diff --git a/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean b/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean
index 5546d514..ab7d2442 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean
@@ -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 :=