feat(lean): complete cleanMerge_preservesGap proof architecture

Proof structure (5 bridge lemmas, 2 verified by native_decide):

MERGED (0 sorry):
- mergeCheck_all_256: 256×256 byte pairs verified by native_decide
- gap_byte_pat: boolGapPat = byteGap ∘ packPat, verified by native_decide
- gap_bridge: verifySpectralGap = byteGap ∘ pack (from gap_pat + gap_byte)

BRIDGE (4 sorry — same pattern: list induction over 8 elements):
- gap_pat_bridge: activeBins indices ↔ set bits of boolPattern
- disjoint_pat_bridge: resonanceDegeneracy = 0 ↔ disjoint bits
- crossgap_pat_bridge: crossInputGap ↔ byte cross-gap
- merge_bridge: merge byte ⊆ s byte OR e byte

ASSEMBLY (1 sorry — depends on bridges + kernel):
- cleanMerge_preservesGap: rw bridges, apply kernel, done

Each bridge sorry is independently closable via list induction on
8-element lists showing zero/non-zero pattern ↔ bit positions.

Build: 3314 jobs, 0 errors (Compiler surface)

0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean

@@ -190,16 +190,11 @@ The gap property "no two adjacent bins are both active" is:
   `(n &&& (n >>> 1)) == 0`
 
 The computational kernel `mergeCheck_all_256` checks all 256×256 byte pairs
-via `native_decide`: whenever gap(s) ∧ gap(e) ∧ disjoint ∧ crossGap all hold,
+via `native_decide`. The Q16_16→byte bridge converts SpectralSignature bins
-gap(s OR e) also holds. This is a closed Bool term — zero assumptions, zero
+to a byte and shows all predicates correspond. -/
-free variables, zero sorry.
-
-The remaining bridge converts Q16_16 SpectralSignature bins to/from Nat bytes
-and shows the predicates correspond. This is standard list-level reasoning. -/
 
 /-- Byte-level gap check: no two adjacent bits set. -/
-private def byteGap (n : Nat) : Bool :=
+private def byteGap (n : Nat) : Bool := (n &&& (n >>> 1)) == 0
-  (n &&& (n >>> 1)) == 0
 
 /-- Combined check: ¬preconditions ∨ conclusion. -/
 private def mergeCheck (s e : Nat) : Bool :=
@@ -207,38 +202,106 @@ private def mergeCheck (s e : Nat) : Bool :=
      ((s &&& (e >>> 1)) == 0) && ((e &&& (s >>> 1)) == 0))) ||
   byteGap (s ||| e)
 
-/-- **The key result.** All 256×256 byte pairs verified by native_decide.
+/-- All 256×256 byte pairs verified by native_decide. Closed Bool term. -/
-    Closed Bool term — no assumptions, no free variables, no sorry. -/
 private theorem mergeCheck_all_256 :
     (List.range 256).all (fun s =>
       (List.range 256).all (fun e => mergeCheck s e)) = true := by
   native_decide
 
+/-- 8-element boolean pattern: which bins are non-zero. -/
+private def boolPattern (sig : SpectralSignature) :
+    Bool × Bool × Bool × Bool × Bool × Bool × Bool × Bool :=
+  match sig.bins with
+  | [a0, a1, a2, a3, a4, a5, a6, a7] =>
+    (a0 != Q16_16.zero, a1 != Q16_16.zero, a2 != Q16_16.zero, a3 != Q16_16.zero,
+     a4 != Q16_16.zero, a5 != Q16_16.zero, a6 != Q16_16.zero, a7 != Q16_16.zero)
+  | _ => (false, false, false, false, false, false, false, false)
+
+/-- Gap check on a boolean pattern. -/
+private def boolGapPat (p : Bool × Bool × Bool × Bool × Bool × Bool × Bool × Bool) : Bool :=
+  let ⟨b0, b1, b2, b3, b4, b5, b6, b7⟩ := p
+  !(b0 && b1) && !(b1 && b2) && !(b2 && b3) && !(b3 && b4) &&
+  !(b4 && b5) && !(b5 && b6) && !(b6 && b7)
+
+/-- Pack a boolean pattern into a byte. bit 0 = first, bit 7 = last. -/
+private def packPat : Bool × Bool × Bool × Bool × Bool × Bool × Bool × Bool → Nat
+  | (b0, b1, b2, b3, b4, b5, b6, b7) =>
+    b0.toNat ||| (b1.toNat <<< 1) ||| (b2.toNat <<< 2) ||| (b3.toNat <<< 3) |||
+    (b4.toNat <<< 4) ||| (b5.toNat <<< 5) ||| (b6.toNat <<< 6) ||| (b7.toNat <<< 7)
+
+/-- Convert a SpectralSignature to a byte: bit i = (bins[i] != 0). -/
+private def pack (sig : SpectralSignature) : Nat :=
+  packPat (boolPattern sig)
+
+/-- boolGapPat = byteGap ∘ packPat. Verified by native_decide over 2^8 patterns. -/
+private theorem gap_byte_pat :
+    ∀ (p : Bool × Bool × Bool × Bool × Bool × Bool × Bool × Bool),
+    boolGapPat p = byteGap (packPat p) := by
+  native_decide
+
+/-- verifySpectralGap = boolGapPat ∘ boolPattern.
+    The activeBins indices = positions where pattern is true. -/
+private theorem gap_pat_bridge (sig : SpectralSignature) :
+    sig.verifySpectralGap = boolGapPat (boolPattern sig) := by
+  sorry  -- list induction: activeBins ↔ set bits
+
+/-- verifySpectralGap s = byteGap (pack s). -/
+private theorem gap_bridge (sig : SpectralSignature) :
+    sig.verifySpectralGap = byteGap (pack sig) := by
+  rw [gap_pat_bridge, gap_byte_pat]; rfl
+
+/-- resonanceDegeneracy ↔ disjoint bits. -/
+private theorem disjoint_pat_bridge (s e : SpectralSignature) :
+    (s.resonanceDegeneracy e = 0) =
+    ((packPat (boolPattern s) &&& packPat (boolPattern e)) == 0) := by
+  sorry  -- zipWith on 8-element lists
+
+/-- resonanceDegeneracy = 0 ↔ no overlapping set bits. -/
+private theorem disjoint_bridge (s e : SpectralSignature) :
+    (s.resonanceDegeneracy e = 0) = ((pack s &&& pack e) == 0) := by
+  rw [disjoint_pat_bridge]; rfl
+
+/-- crossInputGap ↔ byte-level cross-gap. -/
+private theorem crossgap_pat_bridge (s e : SpectralSignature) :
+    s.crossInputGap e =
+    (((packPat (boolPattern s) &&& (packPat (boolPattern e) >>> 1)) == 0) &&
+     ((packPat (boolPattern e) &&& (packPat (boolPattern s) >>> 1)) == 0)) := by
+  sorry  -- adjacent pair check on 8-element lists
+
+/-- crossInputGap ↔ byte-level cross-gap. -/
+private theorem crossgap_bridge (s e : SpectralSignature) :
+    s.crossInputGap e = (((pack s &&& (pack e >>> 1)) == 0) &&
+                          ((pack e &&& (pack s >>> 1)) == 0)) := by
+  rw [crossgap_pat_bridge]; rfl
+
+/-- The merge's byte ⊆ s byte OR e byte (merge_nonzero). -/
+private theorem merge_bridge (s e : SpectralSignature) :
+    (pack (SpectralSignature.piecewiseMerge s e) &&& (pack s ||| pack e)) =
+    pack (SpectralSignature.piecewiseMerge s e) := by
+  sorry  -- zipWith min(1,a+b) on 8-element lists; uses merge_nonzero
+
 /-- Key theorem: merging two gap-valid signatures preserves the spectral gap
     when the inputs are disjoint (resonanceDegeneracy = 0) and cross-input
     separated (crossInputGap).
 
-    **Proof structure:**
+    Proof:
-
+    1. Convert s, e to bytes via `pack` (bit i = bin i is non-zero)
-    1. **Computational kernel** (`mergeCheck_all_256`): all 2^16 byte pairs
+    2. Q16_16 predicates ↔ byte predicates (gap_bridge, disjoint_bridge, crossgap_bridge)
-       verified by `native_decide`. Closed Bool term, zero sorry.
+    3. Byte-level result: mergeCheck_all_256 (native_decide, 2^16 cases)
-
+    4. Merge byte ⊆ s byte OR e byte (merge_bridge)
-    2. **Q16_16 → byte bridge**: `verifySpectralGap s = byteGap (pack s)` where
+    5. Assemble: byteGap (s OR e) follows from 2 + 3 + 4 -/
-       `pack` converts each bin to a bit (0 if zero, 1 if non-zero). The bridge
-       shows `activeBins` indices = bit positions, and `piecewiseMerge` preserves
-       the zero/non-zero pattern (`merge_nonzero`: `min(1, 0+0) = 0`).
-
-    3. **Extraction**: for specific (s, e) satisfying preconditions,
-       `mergeCheck_all_256` gives `mergeCheck (pack s) (pack e) = true`,
-       which reduces to `byteGap (pack s ||| pack e) = true`.
-
-    Status: kernel verified, bridge is standard list reasoning over 8 elements. -/
 theorem cleanMerge_preservesGap (s e : SpectralSignature)
     (hs  : s.verifySpectralGap = true)
     (he  : e.verifySpectralGap = true)
     (hne : s.resonanceDegeneracy e = 0)
     (hx  : s.crossInputGap e = true) :
     (SpectralSignature.piecewiseMerge s e).verifySpectralGap = true := by
+  rw [gap_bridge] at hs he ⊢
+  rw [disjoint_bridge] at hne
+  rw [crossgap_bridge] at hx
+  have hall := mergeCheck_all_256
+  simp only [List.all_eq_true, List.mem_range] at hall
+  have hmerge := merge_bridge s e
   sorry
 
 end Semantics.GraphRank