mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
0d387902bb
Self-contained document for LLM agents to close the 6 remaining bridge sorries. Covers: - Theorem statement and definitions - Proof architecture (3 verified kernels + 6 bridge sorries) - What each sorry needs and the proof strategy - The key insight (zero/non-zero pattern only) - The blocker (simp can't reduce List operations on 8 elements) - Possible solutions and file context
294 lines
15 KiB
Markdown
294 lines
15 KiB
Markdown
# 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
|
||
```
|