SQ006 — dyadic sqrt2 refinement — irrationality research

Exact named statement

forall k l d s q t. DyadicSqrt2(k,d,s) ->
  DyadicSqrt2(k+l,q,t) ->
  exists e. (Pow(2,l,e)) /\ ((~e=0) /\ ((q=d*e) /\ ((Le(s*e,t)) /\ (Lt(t,(S s)*e)))))

PD0001 — Le · PD0002 — Lt · PD0020 — Pow · ND0446 — DyadicSqrt2

Fully expanded target AST

Complete certificate and independent checks

131 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: 4c4a92be36b18b982f9f2f1196e3d2d996ddb4e94fa07479a82bc2eb01d548df
Bundle SHA-256: de94cca849970d3b9ae6794bc012b3ac94b78e32d9475c5069ca02df86f5ba33

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

Scope

preserve supplied dyadic sqrt2 computations at ordered precisions construct actual intervening power prove denominator product and integer nesting without real limit

None of these finite arithmetic statements closes an IR campaign parent. The analytic identification, interpolation and final positive irrationality certificate remain open.