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) :