AP057 — exp normalized truncation — irrationality research

Exact named statement

forall d x L ab ac K m N h s t p B. ~d=0 ->
  Le(x,L*d) ->
  Le(2*L,K) ->
  NatScaledExpRecurrence(d,x,ab,ac,(K+m)+N) ->
  BetaAt(ab,ac,0,h) ->
  Sum(ab,ac,K+m,s) ->
  Sum(ab,ac,S((K+m)+N),t) ->
  Pow(2,m,p) ->
  Pow(L,K,B) ->
  Le(s,t) /\ Le(p*t,p*s+2*(B*h))

PD0001 — Le · PD0013 — BetaAt · PD0015 — Sum · PD0020 — Pow · ND0443 — NatScaledExpRecurrence

Fully expanded target AST

Complete certificate and independent checks

160 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: f74987c7317766d697ca0d5792985ab700e38691f10bd6149d8c1ca141fc33b9
Bundle SHA-256: cc59b8f6360dec4a08b2e261e02420319cf7924020589c9285163adb763d294c

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.

AP051 · AP052 · AP053 · AP054 · AP055 · AP056 · CV009 · CV068

Scope

prove the large argument truncation error relative to the original head while retaining the supplied table sums and two actual powers including zero head and empty prefix without an analytic limit

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