Exact named statement
forall n. exists r d lb lc x q wb wc ab ac h f t z u s. (Pow(2,n,r)) /\ ((~r=0) /\ ((~d=0) /\ ((NatAtanhPrefix(d,lb,lc,S(S(18*r)))) /\ ((NatHornerValue(lb,lc,3,S(S(18*r)),x)) /\ ((Pow(3,S(S(18*r)),q)) /\ ((~q=0) /\ ((~(d*q)=0) /\ ((Le(3*x,d*q)) /\ ((~h=0) /\ ((NatExpWeightTable(2*(d*q),(S(S(S(18*r))))+(S(S(18*r))),wb,wc)) /\ ((NatPowerWeightedPrefix(3*x,wb,wc,ab,ac,S((S(S(S(18*r))))+(S(S(18*r)))))) /\ ((BetaAt(wb,wc,0,h)) /\ ((BetaAt(ab,ac,0,h)) /\ ((Factorial((S(S(S(18*r))))+(S(S(18*r))),f)) /\ ((Pow(2*(d*q),(S(S(S(18*r))))+(S(S(18*r))),t)) /\ ((h=f*t) /\ ((Sum(ab,ac,S((S(S(S(18*r))))+(S(S(18*r)))),z)) /\ ((NatScaledExpRecurrence(2*(d*q),3*x,ab,ac,(S(S(S(18*r))))+(S(S(18*r))))) /\ ((Sum(ab,ac,S(S(S(18*r))),u)) /\ ((Le(r*(u*u),(r*2)*(h*h)+3*(h*h))) /\ ((Le((r*2)*(h*h),r*(u*u)+(h*h))) /\ ((DyadicSqrt2(n,r,s)) /\ ((Le(r*(u*r),r*(s*h)+7*(h*r))) /\ (Le(r*(s*h),r*(u*r)+(h*r))))))))))))))))))))))))))PD0001 — Le · PD0013 — BetaAt · PD0015 — Sum · ND0423 — NatExpWeightTable · PD0020 — Pow · PD0023 — Factorial · ND0437 — NatHornerValue · ND0425 — NatAtanhPrefix · ND0442 — NatPowerWeightedPrefix · ND0443 — NatScaledExpRecurrence · ND0446 — DyadicSqrt2
Complete certificate and independent checks
560 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: 4110740f69dfccac4fd2f8dfa027de161e05948d42f010fe33bdf3b03c1bcbca
Bundle SHA-256: 7c36ebfc20bc30b67500cb3c89192873f059af2f30b2cf4f26baeb80c3d822b6
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 · AP037 · AP038 · AP040 · AP041 · AP042 · AP043 · AP044 · AP045 · AP046 · AP047 · AP048 · AP049 · CV001 · CV002 · CV004 · CV008 · CV009 · CV011 · CV012 · CV019 · CV020 · CV021 · CV022 · CV024 · CV025 · CV027 · CV028 · CV029 · CV030 · CV031 · CV032 · CV033 · CV037 · CV038 · CV039 · CV043 · CV044 · CV046 · CV047 · CV048 · CV049 · CV056 · CV057 · CV058 · CV059 · CV060 · CV061 · CV062 · CV063 · CV064 · CV065 · CV068 · CV069 · CV070 · CV072 · CV073 · CV075 · CV077 · CV078 · CV079 · CV081 · CV082 · CV083 · CV084 · CV086 · CV087 · CV088 · CV094 · CV095 · CV096 · CV097 · CV098 · CV100 · SQ002 · SQ009
Scope
construct at every precision the actual half log exponential and same denominator dyadic floor root preserving all computations and square bounds and proving both finite cross product errors without an infinite identity
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.