Exact named statement
forall n. exists r. Pow(2,n,r) /\ (~r=0 /\ (forall k d ab ac x p tb tc h y. Le(S(S(18*r)),k) ->
~d=0 ->
NatAtanhPrefix(d,ab,ac,S(2*k)) ->
NatHornerValue(ab,ac,3,S(2*k),x) ->
Pow(3,S(2*k),p) ->
NatScaledExpRecurrence(d*p,3*x,tb,tc,S(S k)) ->
BetaAt(tb,tc,0,h) ->
Sum(tb,tc,S(S(S k)),y) ->
~p=0 /\ (~(d*p)=0 /\ (Le(r*y,(r*2)*h+2*h) /\ Le((r*2)*h,r*y+h)))))PD0001 — Le · PD0013 — BetaAt · ND0425 — NatAtanhPrefix · ND0437 — NatHornerValue · PD0020 — Pow · ND0443 — NatScaledExpRecurrence · PD0015 — Sum
Complete certificate and independent checks
513 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: c49cb9e52773c0bae1157f7b1eedbc0f29391c3163cb80a3c9c28445c69c37b1
Bundle SHA-256: 68e17a66cae013163f697f1a85a48dc2d9a05b8f84a2c621b5a3ca15547cf2a7
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.
AP032 · AP033 · AP034 · AP082 · AP083 · AP084 · CV001 · CV002 · CV004 · CV008 · CV009 · CV011 · CV012 · CV019 · CV020 · CV021 · CV022 · CV024 · CV025 · CV027 · CV028 · CV029 · CV031 · CV032 · CV033 · CV037 · CV038 · CV039 · CV043 · CV044 · CV046 · CV047 · CV048 · CV049 · CV056 · CV057 · CV058 · CV059 · CV060 · CV061 · CV062 · CV063 · CV064 · CV065 · CV068 · CV072 · CV073 · CV075 · CV077 · CV078 · CV079 · CV081 · CV082 · CV083 · CV084 · CV086 · CV087 · CV088 · CV089 · CV090 · CV092 · CV093 · CV094 · CV095 · CV096 · CV097 · CV098 · CV100 · CV101
Scope
prove uniform finite near two bounds for the fixed two k plus one logarithm prefix and k plus two exponential degree by constructing the actual cutoff gap and proving both index alignments without changing the computations
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.