allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-08-17 16:00:35 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(lean): clean up cleanMerge_preservesGap proof structure

Browse source 
Build: 3314 jobs, 0 errors (Compiler surface)
5 bridge sorries remain — each is list induction over 8-element Q16_16
lists showing zero/non-zero pattern ↔ byte bit positions.
This commit is contained in:
allaun 2026-06-22 13:57:06 -05:00
parent 158f10aa04
commit 67c9e72d00
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -239,11 +239,10 @@ private theorem gap_byte_pat :
boolGapPat p = byteGap (packPat p) := by boolGapPat p = byteGap (packPat p) := by
native_decide native_decide
/-- verifySpectralGap = boolGapPat ∘ boolPattern. /-- verifySpectralGap = boolGapPat ∘ boolPattern. -/
The activeBins indices = positions where pattern is true. -/
private theorem gap_pat_bridge (sig : SpectralSignature) : private theorem gap_pat_bridge (sig : SpectralSignature) :
sig.verifySpectralGap = boolGapPat (boolPattern sig) := by sig.verifySpectralGap = boolGapPat (boolPattern sig) := by
sorry -- list induction: activeBins ↔ set bits sorry
/-- verifySpectralGap s = byteGap (pack s). -/ /-- verifySpectralGap s = byteGap (pack s). -/
private theorem gap_bridge (sig : SpectralSignature) : private theorem gap_bridge (sig : SpectralSignature) :