Exact named statement
forall n l up ud rb rc vp vd sb sc. NatSqrt2ApproxRecord(n,up,ud,rb,rc) ->
NatSqrt2ApproxRecord(n+l,vp,vd,sb,sc) ->
exists r. (Pow(2,n,r)) /\ ((~r=0) /\ ((~ud=0) /\ ((~vd=0) /\ ((Le(r*(ud*vp),r*(vd*up)+(ud*vd))) /\ (Le(r*(vd*up),r*(ud*vp)+(ud*vd)))))))Complete certificate and independent checks
305 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: 237174f38843f6146e5511de3aa4f49bd784a08738da6ca90da7734f1b08a057
Bundle SHA-256: ae901ee94df076839e47c0d5eb3a905c1d0f40061d415fa896dd7f318050657b
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 · AP015 · 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
transport the actual all finer finite dyadic error to two complete records after proving the fixed precision shift alignment preserving the actual power and positive denominators without an analytic limit claim
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.