diff --git a/6-Documentation/docs/lean/cleanMerge_preservesGap_proof_guide.md b/6-Documentation/docs/lean/cleanMerge_preservesGap_proof_guide.md new file mode 100644 index 00000000..b40eddcb --- /dev/null +++ b/6-Documentation/docs/lean/cleanMerge_preservesGap_proof_guide.md @@ -0,0 +1,294 @@ +# cleanMerge_preservesGap — Proof Guide for LLM Agents + +**File:** `0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean` +**Module:** `Semantics.GraphRank` +**Build:** `lake build Semantics.GraphRank` (3302 jobs) / `lake build Compiler` (3314 jobs) +**Status:** 6 bridge sorries remaining. All computational kernels verified. + +--- + +## 1. What the Theorem Says + +```lean +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 +``` + +**In words:** If two spectral signatures each have no adjacent active bins, share no active bins (resonanceDegeneracy = 0), and have no cross-input adjacency (crossInputGap), then their piecewise merge also has no adjacent active bins. + +**Why it matters:** This is the "clean edge cannot corrupt a clean node" theorem for spectral-gap-gated social graph ranking. + +--- + +## 2. Key Definitions (from `Semantics.Spectrum`) + +```lean +structure SpectralSignature where + bins : List Q16_16 -- 8 fixed-point amplitude values + +def activeBins (sig : SpectralSignature) : List (Nat × Q16_16) := + (List.zip (List.range sig.bins.length) sig.bins).filter (·.2 != Q16_16.zero) + +def verifySpectralGap (sig : SpectralSignature) : Bool := + let active := sig.activeBins.map (·.1) -- indices of non-zero bins + active.all (fun i => active.all (fun j => + i == j || peakDistance i j > 1)) -- no two active bins are adjacent + +def resonanceDegeneracy (left right : SpectralSignature) : Nat := + List.zipWith (fun a b => if a != 0 && b != 0 then 1 else 0) left.bins right.bins + |>.foldl Nat.add 0 -- count of positions where both are non-zero + +def crossInputGap (left right : SpectralSignature) : Bool := + -- for each adjacent pair (i, i+1): not (left[i] && right[i+1]) and not (right[i] && left[i+1]) + +def piecewiseMerge (left right : SpectralSignature) : SpectralSignature := + ⟨List.zipWith (fun a b => Q16_16.min Q16_16.one (Q16_16.add a b)) left.bins right.bins⟩ +``` + +**Critical observation:** ALL of these predicates depend only on which bins are **zero vs non-zero** (`!= Q16_16.zero`). The actual Q16_16 magnitudes are irrelevant. + +--- + +## 3. Proof Architecture + +``` + ┌─────────────────────────────┐ + │ mergeCheck_all_256 │ ← native_decide (256×256 bytes) + │ "gap(s)∧gap(e)∧disjoint │ 0 sorry ✓ + │ ∧crossGap → gap(s∨e)" │ + └──────────────┬──────────────┘ + │ + ┌──────────────┴──────────────┐ + │ gap_byte_pat │ ← native_decide (256 patterns) + │ "boolGapPat = byteGap∘pack" │ 0 sorry ✓ + └──────────────┬──────────────┘ + │ + ┌─────────────────────────┼─────────────────────────┐ + │ │ │ + ┌──────┴──────┐ ┌──────┴──────┐ ┌──────┴──────┐ + │ gap_bridge │ │disjoint_ │ │crossgap_ │ + │ │ │bridge │ │bridge │ + │ sorry ←─────│──┐ │ sorry ←─────│──┐ │ sorry ←─────│──┐ + └─────────────┘ │ └─────────────┘ │ └─────────────┘ │ + │ │ │ + ┌─────────┴────────────────────────┴────────────────────────┘ + │ + ┌──────┴──────┐ ┌─────────────────┐ + │gap_preserved│ │canonicalize_ │ + │ │ │ne_zero │ + │ sorry ←─────│──┐ │ PROVEN ✓ │ + └─────────────┘ │ └─────────────────┘ + │ ┌─────────────────┐ + │ │canonicalize_ │ + │ │pattern │ + │ │ PROVEN ✓ │ + │ └─────────────────┘ + ┌─────────┘ + ┌──────┴──────┐ + │ merge_bridge│ + │ │ + │ sorry │ + └─────────────┘ +``` + +--- + +## 4. What's Already Proven (0 sorry) + +### 4.1 `mergeCheck_all_256` — The Byte Kernel +```lean +theorem mergeCheck_all_256 : + (List.range 256).all (fun s => + (List.range 256).all (fun e => mergeCheck s e)) = true := by + native_decide +``` +Verified all 65,536 byte-pair combinations. `mergeCheck` is `¬preconditions ∨ conclusion` encoded as a Bool. + +### 4.2 `gap_byte_pat` — Bool Pattern = Byte Gap +```lean +theorem gap_byte_pat : + ∀ (p : Bool × Bool × Bool × Bool × Bool × Bool × Bool × Bool), + boolGapPat p = byteGap (packPat p) := by + native_decide +``` +Verified all 256 boolean patterns. The `boolGapPat` (adjacent-pair check on 8 Bools) equals `byteGap` (AND-shift-zero check on packed byte). + +### 4.3 `canonicalize_ne_zero` — Canonicalization Preserves Zero Pattern +```lean +theorem canonicalize_ne_zero (q : Q16_16) : + (canonicalize q != Q16_16.zero) = (q != Q16_16.zero) := by + unfold canonicalize + split + · next h => rw [h]; rfl -- isTrue: (one != zero) = true by rfl + · next h => simp [Bool.not_eq_true] at h; simp [h] -- isFalse +``` +`canonicalize q = if q != 0 then one else zero`. The proof: case-split on `(q != 0)`. If true, canonicalize = one, and `one != zero = true` (definitional). If false, canonicalize = zero, and `zero != zero = false`. + +### 4.4 `canonicalize_pattern` — Pattern Preserved by Canonicalization +```lean +theorem canonicalize_pattern (sig : SpectralSignature) : + boolPattern (canonicalizeSignature sig) = boolPattern sig := by + unfold canonicalizeSignature boolPattern + match sig.bins with + | [a0, a1, a2, a3, a4, a5, a6, a7] => + simp only [List.map, canonicalize_ne_zero] + | [] => simp [List.map] + | [_] => simp [List.map] + -- ... (one case per list length 0-9+) +``` +The key: `simp [List.map]` reduces `List.map canonicalize [a0,...,a7]` to `[canonicalize a0, ..., canonicalize a7]`. Then `canonicalize_ne_zero` rewrites each `(canonicalize ai != 0)` to `(ai != 0)`. The exhaustive match handles all list lengths (non-8-length lists return `(false,...,false)` for both sides). + +--- + +## 5. What Needs Proving (6 sorries) + +### 5.1 `gap_preserved` — verifySpectralGap Preserved by Canonicalization + +**Statement:** +```lean +theorem gap_preserved (sig : SpectralSignature) : + (canonicalizeSignature sig).verifySpectralGap = sig.verifySpectralGap +``` + +**What it means:** Replacing all bins with their canonical form (zero or one) doesn't change `verifySpectralGap`. + +**Proof strategy:** `verifySpectralGap` uses `activeBins` which filters on `!= 0`. After canonicalization, `canonicalize ai != 0 = ai != 0` (by `canonicalize_ne_zero`). So `activeBins` returns the same indices. And `verifySpectralGap` only uses the indices. + +**How to prove:** +```lean +theorem gap_preserved (sig : SpectralSignature) : + (canonicalizeSignature sig).verifySpectralGap = sig.verifySpectralGap := by + -- Strategy: unfold verifySpectralGap and activeBins on both sides. + -- The only difference is that LHS has (canonicalize ai) and RHS has (ai). + -- Since (canonicalize ai != 0) = (ai != 0) by canonicalize_ne_zero, + -- the filter produces the same indices, and the rest is identical. + -- + -- Problem: simp with List.zip, List.filter, List.map, List.all on + -- 8-element lists produces terms too large for simp to handle. + -- + -- Solution: define a helper that mirrors verifySpectralGap but on + -- explicit Bool values, prove it equals verifySpectralGap by rfl, + -- then rewrite using canonicalize_ne_zero. + sorry +``` + +**Alternative approach that might work:** +1. Define `gapFromBools (b0 ... b7 : Bool) : Bool` that does the same computation as `verifySpectralGap` but on explicit Bool inputs +2. Prove `verifySpectralGap ⟨[a0,...,a7]⟩ = gapFromBools (a0!=0) ... (a7!=0)` — this requires showing the list operations reduce to the Bool operations +3. Prove `gapFromBools (canonicalize a0 != 0) ... = gapFromBools (a0 != 0) ...` — trivially by `canonicalize_ne_zero` +4. Chain: `verifySpectralGap (canonicalize sig) = gapFromBools (canonical ...) = gapFromBools (original) = verifySpectralGap sig` + +The hard part is step 2 — showing `List.zip (List.range 8) [a0,...,a7] |>.filter (·.2 != 0) |>.map (·.1) |>.all ...` reduces to the same thing as checking adjacent Bool pairs. For 8 elements, this is a finite computation but `simp` can't handle the intermediate term size. + +### 5.2 `gap_bridge` — verifySpectralGap = byteGap ∘ pack + +**Statement:** +```lean +theorem gap_bridge (sig : SpectralSignature) : + sig.verifySpectralGap = byteGap (pack sig) +``` + +**Proof chain:** `verifySpectralGap = verifySpectralGap ∘ canonicalize` (gap_preserved) `= boolGapPat ∘ boolPattern` (gapQ16Bool_eq_boolGapPat + canonicalize_pattern) `= byteGap ∘ packPat ∘ boolPattern` (gap_byte_pat) `= byteGap ∘ pack` (definition of pack). + +### 5.3 `disjoint_pat_bridge` — resonanceDegeneracy ↔ Disjoint Bits + +**Statement:** +```lean +theorem disjoint_pat_bridge (s e : SpectralSignature) : + (s.resonanceDegeneracy e = 0) = + ((packPat (boolPattern s) &&& packPat (boolPattern e)) == 0) +``` + +**What it means:** `resonanceDegeneracy = 0` (no position where both are non-zero) ↔ the AND of packed bytes is zero (no overlapping set bits). + +**Proof strategy:** `resonanceDegeneracy` counts positions where `a != 0 && b != 0`. The AND of packed bytes has bit i set iff both s and e have bit i set. These are the same condition. + +**How to prove:** Same pattern as `gap_preserved` — unfold on 8-element lists, use `canonicalize_ne_zero` to reduce to Bool operations. + +### 5.4 `crossgap_pat_bridge` — crossInputGap ↔ Byte Cross-Gap + +**Statement:** +```lean +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)) +``` + +**What it means:** The cross-input adjacency check (no active bin in s adjacent to active bin in e) ↔ the byte-level cross-gap check (s AND (e>>>1) = 0 AND e AND (s>>>1) = 0). + +**Proof strategy:** Same pattern. `crossInputGap` checks adjacent pairs `(i, i+1)` for cross-input activation. The byte version checks the same thing with bitwise shift-AND. + +### 5.5 `merge_bridge` — Merge Byte ⊆ Input Bytes OR + +**Statement:** +```lean +theorem merge_bridge (s e : SpectralSignature) : + (pack (piecewiseMerge s e) &&& (pack s ||| pack e)) = + pack (piecewiseMerge s e) +``` + +**What it means:** Every set bit in the merge's byte is also set in `(pack s ||| pack e)`. Equivalently: if `min(1, a+b) != 0` then `a != 0 || b != 0`. + +**Proof strategy:** For each position, `piecewiseMerge` computes `min(1, a+b)`. If this is non-zero, then `a+b != 0` (since `min(1,x) != 0 ↔ x != 0`), which means `a != 0 || b != 0`. This is `merge_nonzero` (a Q16_16 arithmetic lemma). + +### 5.6 `cleanMerge_preservesGap` — Final Assembly + +**Proof:** +```lean +rw [gap_bridge] at hs he ⊢ -- convert Q16_16 predicates to byte level +rw [disjoint_bridge] at hne +rw [crossgap_bridge] at hx +have hall := mergeCheck_all_256 -- the verified kernel +simp only [List.all_eq_true, List.mem_range] at hall +have hmerge := merge_bridge s e +-- Now: hall gives gap(s∨e) from the preconditions +-- hmerge shows merge byte ⊆ s∨e byte +-- Assemble: byteGap (pack (piecewiseMerge s e)) = true +sorry -- trivial once bridges are done +``` + +--- + +## 6. The Key Insight + +**Everything depends only on zero vs non-zero.** The Q16_16 magnitudes are irrelevant. The proof should: + +1. Convert Q16_16 to Bool (`!= 0`) — already done via `boolPattern` and `canonicalize_ne_zero` +2. Prove the Bool version — already done via `native_decide` on 256×256 cases +3. Show the conversion preserves the predicates — the 6 bridge lemmas + +The bridge lemmas all have the same structure: unfold the Q16_16 list operations on 8-element lists, use `canonicalize_ne_zero` to rewrite each `(canonicalize ai != 0)` to `(ai != 0)`, and show the result equals the Bool version. + +**The blocker:** `simp` can't reduce `List.zip (List.range 8) [a0,...,a7] |>.filter (·.2 != 0) |>.map (·.1) |>.all (fun i => .all (fun j => ...))` to the equivalent `!(b0 && b1) && !(b1 && b2) && ... && !(b6 && b7)`. The intermediate terms from `List.zip`, `List.filter`, `List.map`, `List.all` on 8 elements are too large for the simplifier. + +**Possible solutions:** +1. Write explicit `@[simp]` equation lemmas for `List.zip`, `List.filter`, `List.map`, `List.all` on concrete 8-element lists +2. Use `native_decide` after `revert`-ing the Q16_16 variables (fails because Q16_16 = Subtype Int, infinite) +3. Define a `@[reducible]` version of `verifySpectralGap` that unfolds to a concrete Bool expression on 8 elements, then `rfl` or `decide` +4. Write a custom tactic that canonicalizes Q16_16 values and calls `native_decide` + +--- + +## 7. File Context + +- **Q16_16** is defined in `Semantics.FixedPoint` as `{ x : Int // q16MinRaw ≤ x ∧ x ≤ q16MaxRaw }`. It has `BEq`, `DecidableEq`, `Repr`. +- **Q16_16.zero** = `⟨0, ...⟩`, **Q16_16.one** = `⟨65536, ...⟩` (1.0 in Q16.16 fixed-point). +- **SpectralSignature** is `structure where bins : List Q16_16`. No length constraint. +- The `!=` operator on Q16_16 uses `BEq` which compares `.val` (the underlying Int). +- `List.range 8 = [0,1,2,3,4,5,6,7]`. +- `peakDistance i j = if i > j then i - j else j - i`. + +--- + +## 8. Build Commands + +```bash +cd 0-Core-Formalism/lean/Semantics +lake build Semantics.GraphRank # 3302 jobs, should have 6 sorries +lake build Compiler # 3314 jobs, must stay green +```