AP076 — ordered power difference — irrationality research

Exact named statement

forall a b M g k u v w. b=a+g ->
  Le(b,M) ->
  Pow(a,S k,u) ->
  Pow(b,S k,v) ->
  Pow(M,k,w) ->
  Le(v,u+(S k)*(g*w))

PD0020 — Pow · PD0001 — Le

Fully expanded target AST

Complete certificate and independent checks

36 actual local proof nodes. Each node carries its complete ordinary HA proof body.

Full canonical proof bundle · Original HA receipt · Independent Lean receipt

Target SHA-256: d4d5beb6c20b976f94c1c1e219e65c4389e0dddce29a5b2f642ed9c3014a7b04
Bundle SHA-256: f0ca341bf0363808fabc242631285ec8ced1c63c25f227a557e94235f202c4f7

Checked statement containment

These exact targets occur inside this certificate. These links summarize containment, not direct dependency arrows; the downloadable bundle records every private lemma and ordered edge.

Scope

prove the ordered natural power difference bound for three actual supplied powers by ordinary induction including zero bases without division or analytic axioms

None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.