# 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
```