Exact named statement
forall k l d s q t. DyadicSqrt2(k,d,s) ->
DyadicSqrt2(k+l,q,t) ->
(~d=0) /\ ((~s=0) /\ ((~t=0) /\ ((Le(q*s,d*t)) /\ (Le(d*(d*t),d*(q*s)+s*t)))))Complete certificate and independent checks
149 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: 4e5333c99ca1ed711e3c4059b5352c1b5545b4d3d6ce9e26db04482a0f15cdcd
Bundle SHA-256: 16ba3030487cf8f07c10bd9a3cc909569392a2b677c8bbd6322d8bcd4e403ab4
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.
SQ002 · SQ005 · SQ006 · SQ007 · SQ008 · SQ009
Scope
actual dyadic sqrt2 reciprocal approximants have proved positive denominators reversed order and explicit finite cross multiplied error at most 2 to minus coarse precision no real reciprocal assumption
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.