Exact named statement
forall d. ~d=0 ->
exists s. (FloorSqrt(2*(d*d),s)) /\ (Le(d,s)) /\ (Lt(s,2*d)) /\ (~s=0) /\ (forall t. FloorSqrt(2*(d*d),t) ->
t=s)Complete certificate and independent checks
42 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: 4e1139169e23ee835cb5f0eb9371fa4b6a641079db34b76bcb25f692bd88efb8
Bundle SHA-256: 05d951bee0ed77b01b03ff51e51da3ea4e8349a397c563cbe6b119670a83271f
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
construct unique actual floor root of twice any positive scale squared and prove it lies between the scale and twice scale with nonzero root no analytic interpretation
None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.