Exact named statement
forall k d s. DyadicSqrt2(k,d,s) ->
(~d=0) /\ ((~s=0) /\ ((Le(d,s)) /\ ((Lt(s,2*d)) /\ ((Le(s*s,2*(d*d))) /\ (Le(2*(d*d),s*s+2*(2*d)))))))Complete certificate and independent checks
53 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: c5d6445cccb9460719eff249437f8849968eaa22bcc68dc2d5615589e7873a0c
Bundle SHA-256: 1189e78e28fb6697459f8f7ff4696adaa4d8f739643e53c11fa82c491066e274
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
supplied actual dyadic sqrt2 computation has positive denominator and root root range and explicit square residual at most four times denominator no limit or square root identity assumption
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.