From 67c9e72d00273e5350cab973ce6dede774fe770c Mon Sep 17 00:00:00 2001 From: allaun Date: Mon, 22 Jun 2026 13:57:06 -0500 Subject: [PATCH] fix(lean): clean up cleanMerge_preservesGap proof structure MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- 0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean b/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean index af84d9d0..785517a6 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean @@ -239,11 +239,10 @@ private theorem gap_byte_pat : boolGapPat p = byteGap (packPat p) := by native_decide -/-- verifySpectralGap = boolGapPat ∘ boolPattern. - The activeBins indices = positions where pattern is true. -/ +/-- verifySpectralGap = boolGapPat ∘ boolPattern. -/ private theorem gap_pat_bridge (sig : SpectralSignature) : sig.verifySpectralGap = boolGapPat (boolPattern sig) := by - sorry -- list induction: activeBins ↔ set bits + sorry /-- verifySpectralGap s = byteGap (pack s). -/ private theorem gap_bridge (sig : SpectralSignature) :