allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(lean): close canonicalize_ne_zero and canonicalize_pattern sorries

Browse source 
canonicalize_ne_zero: (canonicalize q != 0) = (q != 0)
  Proof: unfold canonicalize, split on if-condition,
  rw h in isTrue branch (Q16_16.one != zero = true by rfl),
  simp in isFalse branch.

canonicalize_pattern: boolPattern ∘ canonicalizeSignature = boolPattern
  Proof: unfold definitions, exhaustive match on list length (0-9+ elements),
  simp with canonicalize_ne_zero rewrites each component.

6 bridge sorries remain (down from 8). Each requires list-level reasoning
over 8-element Q16_16 lists — the simp terms from List.zip/filter/all are
too large for automatic simplification.

Build: 3314 jobs, 0 errors (Compiler surface)
This commit is contained in:
allaun 2026-06-22 14:34:37 -05:00
parent 70bdfb5c2a
commit 56679941ed
1 changed files with 36 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean
View file

@ -246,15 +246,47 @@ private def canonicalize (q : Q16_16) : Q16_16 :=
private def canonicalizeSignature (sig : SpectralSignature) : SpectralSignature :=
⟨sig.bins.map canonicalize⟩
/-- The canonicalized pattern matches the boolean pattern. -/
/-- canonicalize preserves != 0. Key building block. -/
private theorem canonicalize_ne_zero (q : Q16_16) :
(canonicalize q != Q16_16.zero) = (q != Q16_16.zero) := by
unfold canonicalize
split
· next h =>
-- h : (q != Q16_16.zero) = true
-- Goal: (Q16_16.one != Q16_16.zero) = (q != Q16_16.zero)
rw [h]
-- Goal: (Q16_16.one != Q16_16.zero) = true
rfl
· next h =>
-- h : ¬(q != Q16_16.zero) = true
-- i.e., (q != Q16_16.zero) = false
simp [Bool.not_eq_true] at h
simp [h]
/-- boolPattern ∘ canonicalizeSignature = boolPattern. -/
private theorem canonicalize_pattern (sig : SpectralSignature) :
boolPattern (canonicalizeSignature sig) = boolPattern sig := by
sorry -- (canonicalize ai != zero) = (ai != zero)
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]
| [_, _] => simp [List.map]
| [_, _, _] => simp [List.map]
| [_, _, _, _] => simp [List.map]
| [_, _, _, _, _] => simp [List.map]
| [_, _, _, _, _, _] => simp [List.map]
| [_, _, _, _, _, _, _] => simp [List.map]
| _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ => simp [List.map]
/-- verifySpectralGap preserved by canonicalization. -/
/-- verifySpectralGap preserved by canonicalization.
Follows from activeBins filtering on != 0 (canonicalize_ne_zero).
Proof: unfold activeBins, match on 8-element list, simp with canonicalize_ne_zero
rewrites (canonicalize ai != 0) to (ai != 0) at each position. -/
private theorem gap_preserved (sig : SpectralSignature) :
(canonicalizeSignature sig).verifySpectralGap = sig.verifySpectralGap := by
sorry -- activeBins depends only on != zero
sorry
/-- The boolean gap check on 8 concrete Q16_16 values (zero or one). -/
private def gapQ16 (a0 a1 a2 a3 a4 a5 a6 a7 : Q16_16) : Bool :=