Exact named statement
forall n. exists up ud rb rc. NatSqrt2ApproxRecord(n,up,ud,rb,rc)Complete certificate and independent checks
206 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: 6ff27609504236182a615ce1dd07fddf1b3d1c7d0161d869bb756ac824c4ef8e
Bundle SHA-256: 118016ea5a5b20b9116df0cdd125fcd0aff8a5d906b152f62b680d9b44db4199
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.
AP022 · AP023 · CV022 · CV030 · CV032 · CV069 · CV070 · CV086 · SQ001 · SQ002 · SQ003 · SQ004
Scope
construct an actual fifteen field beta record of the positive fixed factorial finite sample at precision n plus eight with both code components explicit and all decoded fields consumed without accuracy or analytic clauses
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.