Exact named statement
forall d x bb bc n b0 v p. ~d=0 ->
Le(x,d) ->
NatScaledExpRecurrence(d,x,bb,bc,n) ->
BetaAt(bb,bc,0,b0) ->
Sum(bb,bc,S n,v) ->
Pow(2,n,p) ->
exists wb wc ab ac h f q z u. (~h=0) /\ ((NatExpWeightTable(2*d,(S n)+n,wb,wc)) /\ ((NatPowerWeightedPrefix(x,wb,wc,ab,ac,S((S n)+n))) /\ ((BetaAt(wb,wc,0,h)) /\ ((BetaAt(ab,ac,0,h)) /\ ((Factorial((S n)+n,f)) /\ ((Pow(2*d,(S n)+n,q)) /\ ((h=f*q) /\ ((Sum(ab,ac,S((S n)+n),z)) /\ ((NatScaledExpRecurrence(2*d,x,ab,ac,(S n)+n)) /\ ((Sum(ab,ac,S n,u)) /\ (Le((h*h)*v,b0*(u*u)) /\ Le(p*(b0*(u*u)),p*((h*h)*v)+2*(b0*(h*h))))))))))))))PD0001 — Le · PD0013 — BetaAt · PD0015 — Sum · ND0423 — NatExpWeightTable · PD0020 — Pow · PD0023 — Factorial · ND0442 — NatPowerWeightedPrefix · ND0443 — NatScaledExpRecurrence
Complete certificate and independent checks
303 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: a0ae3b4a0d82774e120a7703228bf12483ea7f606b04303d09fac179c58075e7
Bundle SHA-256: f65fd8094f9b078f62b6ee80b550b4bb62cff1c7a7728edc179d6215ae3fb413
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.
AP037 · AP038 · AP040 · AP041 · AP042 · AP043 · CV008 · CV009 · CV011 · CV022 · CV030 · CV043 · CV044 · CV046 · CV047 · CV048 · CV068 · CV069 · CV070 · CV087 · CV088 · CV094 · CV095 · CV096 · CV097 · CV098 · CV100
Scope
construct positive factorial weighted half argument exponential terms and both actual sums and bound the short sum square against the supplied whole argument sum without logarithm or square root identification
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.