Exact named statement
forall d x tb tc m N a0. ~d=0 ->
Le(x,d) ->
NatScaledExpRecurrence(d,x,tb,tc,(S m)+N) ->
BetaAt(tb,tc,0,a0) ->
exists p ub uc a s. Pow(2,m,p) /\ (BetaAt(tb,tc,S m,a) /\ (NatAffineSlice(tb,tc,S m,1,ub,uc,S N) /\ (NatRatioBoundPrefix(ub,uc,1,S N) /\ (Sum(ub,uc,S N,s) /\ (Le(p*a,a0) /\ (Le(p*s,2*a0)))))))PD0001 — Le · PD0013 — BetaAt · PD0015 — Sum · ND0411 — NatAffineSlice · PD0020 — Pow · ND0441 — NatRatioBoundPrefix · ND0443 — NatScaledExpRecurrence
Complete certificate and independent checks
136 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: 76d2878ab4276b62e8094e3b25956fc0b58fec9c0d936f9c3af4c253fe8cc5ba
Bundle SHA-256: b69e30c4b5c8f199bb7dc45506f4d3476edf42e8acae440e9ee5c806e00fa303
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
construct actual cutoff power two m first omitted term slice ratio and sum with power times first at most head and power times tail at most twice head uniform in extra finite horizon not analytic limit
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.