From ac700c64606d42ca4d7bdf434b468f2e67196e8f Mon Sep 17 00:00:00 2001 From: allaun Date: Mon, 22 Jun 2026 13:48:39 -0500 Subject: [PATCH] feat(lean): add byte-level gap kernel for cleanMerge_preservesGap MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- .../lean/Semantics/Semantics/GraphRank.lean | 71 +++++++++++-------- 1 file changed, 43 insertions(+), 28 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean b/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean index bb6b3fde..d279641e 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean +++ b/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. - Verified by `native_decide` as a closed ∀-proposition (2^16 cases). -/ -private def boolGap8 (b0 b1 b2 b3 b4 b5 b6 b7 : Bool) : Bool := - !(b0 && b1) && !(b1 && b2) && !(b2 && b3) && !(b3 && b4) && - !(b4 && b5) && !(b5 && b6) && !(b6 && b7) +/-! ## cleanMerge_preservesGap — Bit-level proof + +A boolean is a bit: 0 or 1. Eight bins = 8 bits = one byte. +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, +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: - 1. No bin is active in both (resonanceDegeneracy = 0) - 2. No active bin in one is adjacent to an active bin in the other (crossInputGap) + when the inputs are disjoint (resonanceDegeneracy = 0) and cross-input + separated (crossInputGap). - **Proof sketch** (complete, no mathematical gaps): + **Proof structure:** - 1. **Merge active ⊆ input union**: For each position i, - `min(1, s.bins[i] + e.bins[i]) != 0 → s.bins[i] != 0 ∨ e.bins[i] != 0` - (contrapositive: 0+0 = 0 by `Q16_16.add_zero`). + 1. **Computational kernel** (`mergeCheck_all_256`): all 2^16 byte pairs + verified by `native_decide`. Closed Bool term, zero sorry. - 2. **Union is gap-valid**: The union of s.active and e.active has no - adjacent active positions because: - - Within s: guaranteed by `hs` (verifySpectralGap) - - Within e: guaranteed by `he` - - Across s→e: guaranteed by `hx` (crossInputGap) + 2. **Q16_16 → byte bridge**: `verifySpectralGap s = byteGap (pack s)` where + `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. **Subset inherits gap**: If the union has no adjacent actives, - any subset (the merge) also has no adjacent actives. + 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`. - 4. **Boolean model**: Steps 2-3 are verified by `native_decide` on the - `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. -/ + 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)