Exact named statement
forall k. exists d s. (DyadicSqrt2(k,d,s)) /\ ((~d=0) /\ ((~s=0) /\ ((Le(d,s)) /\ ((Lt(s,2*d)) /\ (forall q t. DyadicSqrt2(k,q,t) ->
q=d /\ t=s)))))Complete certificate and independent checks
139 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: 949e42462649aba0033ab2dacf74c2aba14cced0c759d3efedb524aa34ee12ce
Bundle SHA-256: f73908713a8b4912da9bc340d3a4e9e51f8ef156993f9527040eaaad0cf34ebf
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
unconditional total unique positive dyadic sqrt2 computation using actual power and floor root graph with separate proved integer bounds no accuracy clause or analytic interpretation
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.