Exact named statement
forall k d s D ab ac x p wb wc tb tc w0 f h y. ~D=0 ->
NatSqrt2ExpSample(k,d,s,D,ab,ac,x,p,wb,wc,tb,tc,w0,f,h,y) ->
(~w0=0) /\ ((~((D*p)*s)=0) /\ ((Sum(tb,tc,S (k+2),y)) /\ ((forall j t. Le(j,(k+2)) ->
BetaAt(tb,tc,j,t) ->
exists f0 p0 q0. (Factorial(j,f0)) /\ ((Pow(((D*p)*s),j,p0)) /\ ((Pow(((3*x)*d),j,q0)) /\ ((~f0=0) /\ ((~p0=0) /\ (IRatEq(t,0,w0,q0,0,f0*p0))))))))))PD0013 — BetaAt · PD0020 — Pow · PD0001 — Le · PD0023 — Factorial · PD0015 — Sum · ND0448 — NatSqrt2ExpSample · ND0383 — IRatEq
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: 8c30669eb1c317280a38fcade33d35967d3427cb940f0753752a02da1460daee
Bundle SHA-256: 54f2e7c6dafc48993d063b9a2d83baf25bd914591746ff2119806debafd152dd
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
preserve the actual supplied exponential sample table and sum and identify each normalized term with its factorial series value using constructed factorials and both powers with positive denominators without infinite exponential identification
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.