feat(lean): add byte-level gap kernel for cleanMerge_preservesGap

A boolean is a bit. Eight bins = eight bits = one byte.

mergeCheck_all_256: closed Bool term verified by native_decide over
all 256×256 byte pairs. Zero assumptions, zero free variables, zero sorry.

The kernel proves: for any two bytes where gap(s) ∧ gap(e) ∧ disjoint ∧
crossGap all hold, gap(s OR e) also holds. This is the complete
computational proof of the spectral gap merge property at the bit level.

The remaining sorry is the Q16_16→byte bridge: converting SpectralSignature
bins to/from Nat bytes and showing the predicates correspond. This is
standard list-level reasoning over 8 elements (unzip, map, filter, all).

Build: 3314 jobs, 0 errors (Compiler surface)

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

@@ -183,41 +183,56 @@ theorem activeBins_empty :
     SpectralSignature.activeBins SpectralSignature.empty = [] := by
   native_decide
 
-/-- Boolean gap check on 8 explicit Bool values: no adjacent trues.
+/-! ## cleanMerge_preservesGap — Bit-level proof
-    Verified by `native_decide` as a closed ∀-proposition (2^16 cases). -/
+
-private def boolGap8 (b0 b1 b2 b3 b4 b5 b6 b7 : Bool) : Bool :=
+A boolean is a bit: 0 or 1. Eight bins = 8 bits = one byte.
-  !(b0 && b1) && !(b1 && b2) && !(b2 && b3) && !(b3 && b4) &&
+The gap property "no two adjacent bins are both active" is:
-  !(b4 && b5) && !(b5 && b6) && !(b6 && b7)
+  `(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,
+gap(s OR e) also holds. This is a closed Bool term — zero assumptions, zero
+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 :=
+  (n &&& (n >>> 1)) == 0
+
+/-- Combined check: ¬preconditions ∨ conclusion. -/
+private def mergeCheck (s e : Nat) : Bool :=
+  (!(byteGap s && byteGap e && ((s &&& e) == 0) &&
+     ((s &&& (e >>> 1)) == 0) && ((e &&& (s >>> 1)) == 0))) ||
+  byteGap (s ||| e)
+
+/-- **The key result.** All 256×256 byte pairs verified by native_decide.
+    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
 
 /-- Key theorem: merging two gap-valid signatures preserves the spectral gap
-    when:
+    when the inputs are disjoint (resonanceDegeneracy = 0) and cross-input
-    1. No bin is active in both (resonanceDegeneracy = 0)
+    separated (crossInputGap).
-    2. No active bin in one is adjacent to an active bin in the other (crossInputGap)
 
-    **Proof sketch** (complete, no mathematical gaps):
+    **Proof structure:**
 
-    1. **Merge active ⊆ input union**: For each position i,
+    1. **Computational kernel** (`mergeCheck_all_256`): all 2^16 byte pairs
-       `min(1, s.bins[i] + e.bins[i]) != 0 → s.bins[i] != 0 ∨ e.bins[i] != 0`
+       verified by `native_decide`. Closed Bool term, zero sorry.
-       (contrapositive: 0+0 = 0 by `Q16_16.add_zero`).
 
-    2. **Union is gap-valid**: The union of s.active and e.active has no
+    2. **Q16_16 → byte bridge**: `verifySpectralGap s = byteGap (pack s)` where
-       adjacent active positions because:
+       `pack` converts each bin to a bit (0 if zero, 1 if non-zero). The bridge
-       - Within s: guaranteed by `hs` (verifySpectralGap)
+       shows `activeBins` indices = bit positions, and `piecewiseMerge` preserves
-       - Within e: guaranteed by `he`
+       the zero/non-zero pattern (`merge_nonzero`: `min(1, 0+0) = 0`).
-       - Across s→e: guaranteed by `hx` (crossInputGap)
 
-    3. **Subset inherits gap**: If the union has no adjacent actives,
+    3. **Extraction**: for specific (s, e) satisfying preconditions,
-       any subset (the merge) also has no adjacent actives.
+       `mergeCheck_all_256` gives `mergeCheck (pack s) (pack e) = true`,
+       which reduces to `byteGap (pack s ||| pack e) = true`.
 
-    4. **Boolean model**: Steps 2-3 are verified by `native_decide` on the
+    Status: kernel verified, bridge is standard list reasoning over 8 elements. -/
-       `Fin 8 → Bool` model (2^16 = 65536 cases). The bridge from Q16_16
-       to Bool preserves all predicates since they only depend on `!= zero`.
-
-    **Status**: The proof is mathematically complete. The remaining gap is
-    the Q16_16↔Bool bridge for 8-element lists, which requires list-level
-    induction on `activeBins`, `verifySpectralGap`, `resonanceDegeneracy`,
-    and `crossInputGap`. This is straightforward but tedious Lean 4 list
-    manipulation — see `boolGap8_merge_thm` above for the Bool kernel. -/
 theorem cleanMerge_preservesGap (s e : SpectralSignature)
     (hs  : s.verifySpectralGap = true)
     (he  : e.verifySpectralGap = true)