From 8e29ea659201c5979f2aadf723747eb85ab42baf Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Mon, 22 Jun 2026 14:00:30 -0500
Subject: [PATCH] feat(lean): add gapQ16_canonical verified by native_decide
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

gapQ16_canonical: for all 2^8 boolean patterns, verifySpectralGap on
canonical Q16_16 bins (zero or one) = boolGapPat on the pattern.
Verified by native_decide — the first time verifySpectralGap has been
computationally verified on concrete Q16_16 values.

Three independent computational kernels now verified:
- mergeCheck_all_256: 256×256 byte pairs (native_decide)
- gap_byte_pat: 256 boolean patterns (native_decide)
- gapQ16_canonical: 256 Q16_16 patterns (native_decide)

The bridge lemmas (canonicalize_pattern, gap_preserved, etc.) remain
as sorry — each is ~20 lines of list simp on 8-element lists.

Build: 3314 jobs, 0 errors
---
 .../lean/Semantics/Semantics/GraphRank.lean   | 47 ++++++++++++++++---
 1 file changed, 41 insertions(+), 6 deletions(-)

diff --git a/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean b/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean
index 785517a6..7a39c688 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean
@@ -239,15 +239,50 @@ private theorem gap_byte_pat :
     boolGapPat p = byteGap (packPat p) := by
   native_decide
 
-/-- verifySpectralGap = boolGapPat ∘ boolPattern. -/
-private theorem gap_pat_bridge (sig : SpectralSignature) :
-    sig.verifySpectralGap = boolGapPat (boolPattern sig) := by
-  sorry
+/-- Canonicalize a Q16_16 value to zero or one. -/
+private def canonicalize (q : Q16_16) : Q16_16 :=
+  if q != Q16_16.zero then Q16_16.one else Q16_16.zero
 
-/-- verifySpectralGap s = byteGap (pack s). -/
+/-- Canonicalize all 8 bins of a signature. -/
+private def canonicalizeSignature (sig : SpectralSignature) : SpectralSignature :=
+  ⟨sig.bins.map canonicalize⟩
+
+/-- The canonicalized pattern matches the boolean pattern. -/
+private theorem canonicalize_pattern (sig : SpectralSignature) :
+    boolPattern (canonicalizeSignature sig) = boolPattern sig := by
+  sorry  -- (canonicalize ai != zero) = (ai != zero)
+
+/-- verifySpectralGap preserved by canonicalization. -/
+private theorem gap_preserved (sig : SpectralSignature) :
+    (canonicalizeSignature sig).verifySpectralGap = sig.verifySpectralGap := by
+  sorry  -- activeBins depends only on != zero
+
+/-- The boolean gap check on 8 concrete Q16_16 values (zero or one). -/
+private def gapQ16 (a0 a1 a2 a3 a4 a5 a6 a7 : Q16_16) : Bool :=
+  let s : SpectralSignature := ⟨[a0, a1, a2, a3, a4, a5, a6, a7]⟩
+  s.verifySpectralGap
+
+/-- gapQ16 on canonical values = boolGapPat on the boolean pattern.
+    Verified by native_decide over the 2^8 canonical patterns. -/
+private theorem gapQ16_canonical :
+    ∀ (b0 b1 b2 b3 b4 b5 b6 b7 : Bool),
+    gapQ16 (if b0 then .one else .zero) (if b1 then .one else .zero)
+           (if b2 then .one else .zero) (if b3 then .one else .zero)
+           (if b4 then .one else .zero) (if b5 then .one else .zero)
+           (if b6 then .one else .zero) (if b7 then .one else .zero) =
+    boolGapPat (b0, b1, b2, b3, b4, b5, b6, b7) := by
+  native_decide
+
+/-- verifySpectralGap s = byteGap (pack s).
+    Via: gapQ16_canonical (native_decide) + canonicalize_pattern + gap_preserved. -/
 private theorem gap_bridge (sig : SpectralSignature) :
     sig.verifySpectralGap = byteGap (pack sig) := by
-  rw [gap_pat_bridge, gap_byte_pat]; rfl
+  -- gapQ16_canonical proves: for canonical bins {zero, one}, gapQ16 = boolGapPat
+  -- gap_preserved proves: verifySpectralGap = verifySpectralGap ∘ canonicalize
+  -- canonicalize_pattern proves: boolPattern ∘ canonicalize = boolPattern
+  -- gap_byte_pat proves: boolGapPat = byteGap ∘ packPat
+  -- Chain: verifySpectralGap = gapQ16(canonical) = boolGapPat(pattern) = byteGap(pack)
+  sorry
 
 /-- resonanceDegeneracy ↔ disjoint bits. -/
 private theorem disjoint_pat_bridge (s e : SpectralSignature) :