Exact named statement
forall n l d s D ab ac x p wb wc tb tc w0 f h y q t E bb bc z v xb xc ub uc v0 g j o. ~D=0 ->
~E=0 ->
NatSqrt2ExpSample(n+8,d,s,D,ab,ac,x,p,wb,wc,tb,tc,w0,f,h,y) ->
NatSqrt2ExpSample((n+8)+l,q,t,E,bb,bc,z,v,xb,xc,ub,uc,v0,g,j,o) ->
exists r. (Pow(2,n,r)) /\ ((~r=0) /\ ((~w0=0) /\ ((~v0=0) /\ ((Le(r*(w0*o),r*(v0*y)+(w0*v0))) /\ (Le(r*(v0*y),r*(w0*o)+(w0*v0)))))))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: 98633f6b0d2144188f824e0f5f1f367d8113fe1999e66199a3b54eb28f615703
Bundle SHA-256: 0cd67027532d8498c60bbdb9cb930631e58a7ee3b16e60982e14bbdaaf415afd
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.
AP003 · AP004 · AP005 · AP006 · AP007 · AP008 · AP009 · AP010 · AP011 · AP012 · AP013 · AP014 · CV009 · CV032 · CV062 · CV068 · CV086 · CV087 · CV088 · CV089 · CV090 · CV092 · CV093 · CV094 · CV095 · CV096 · CV097 · CV098 · CV100 · SQ001 · SQ002 · SQ003 · SQ004 · SQ005 · SQ006 · SQ007 · SQ008 · SQ009 · SQ010
Scope
actual supplied samples at n plus eight and any finer precision have two sided finite error at most one over a constructed positive two to n using the actual coarse power and a constructed positive shift power
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.