Research-Stack/6-Documentation/docs/lean/cleanMerge_preservesGap_proof_guide.md

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

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)

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

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

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

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

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:

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:

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:

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:

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:

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:

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:

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

cd 0-Core-Formalism/lean/Semantics
lake build Semantics.GraphRank     # 3302 jobs, should have 6 sorries
lake build Compiler                # 3314 jobs, must stay green