diff --git a/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean b/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean
index 10c857a2..450555f3 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/GraphRank.lean
@@ -183,39 +183,34 @@ theorem activeBins_empty :
     SpectralSignature.activeBins SpectralSignature.empty = [] := by
   native_decide
 
-/-- Key open theorem: merging two gap-valid signatures with zero resonance
-    degeneracy (no bin active in both) preserves the spectral gap.
-    Interpretation: a clean edge cannot corrupt a clean node.
+/-- Key theorem: merging two gap-valid signatures with zero resonance
+    degeneracy preserves the spectral gap.
 
-    Proof sketch: the gap property depends only on which bins are non-zero.
-    Merged active set ⊆ s.activeBins ∪ e.activeBins. Since both inputs
-    satisfy the gap property with no overlap (resonanceDegeneracy = 0),
-    any two adjacent merged-active bins would require adjacent active bins
-    in one input (contradicting hs/he) or active bins from different inputs
-    at adjacent positions (impossible since the intermediate position is
-    inactive in both inputs, hence inactive in the merge).
+    **Status:** The theorem as stated (with only resonanceDegeneracy = 0) is
+    *false in general*. Counterexample:
 
-    Formalized via boolean abstraction: convert Q16_16 bins to Bool
-    (zero → false, nonzero → true), prove the gap-preservation on the
-    finite 2^8 boolean model, then lift. The boolean version is verified
-    by exhaustive case split (256 × 256 = 65536 cases). -/
+      s = [1,0,1,0,0,0,0,0]  (gap valid, active at {0,2})
+      e = [0,0,0,1,0,1,0,0]  (gap valid, active at {3,5})
+      resonanceDegeneracy = 0 (no overlap)
+      merge = [1,0,1,1,0,1,0,0]  (adjacent active at {2,3} — gap violated!)
+
+    The missing condition is **cross-input gap**: no active bin from s is
+    adjacent to an active bin from e. This holds in the Sidon-basis context
+    (powers-of-2 labels ensure minimum separation ≥ 2).
+
+    **Proof path** (when cross-input gap is available):
+    1. Merged active ⊆ s.active ∪ e.active (merge_active_subset helper below)
+    2. Adjacent merged-active bins come from the same input (contradicts hs/he)
+       or from cross-input adjacency (contradicts cross-gap hypothesis)
+    3. Reduce to boolean model (Fin 8 → Bool) and verify by native_decide
+
+    TODO(lean-port): restate with explicit cross-input gap hypothesis,
+    or prove cross-input gap follows from Sidon-basis constraints. -/
 theorem cleanMerge_preservesGap (s e : SpectralSignature)
     (hs  : s.verifySpectralGap = true)
     (he  : e.verifySpectralGap = true)
     (hne : s.resonanceDegeneracy e = 0) :
     (SpectralSignature.piecewiseMerge s e).verifySpectralGap = true := by
-  -- Boolean abstraction: convert bins to (· != zero) patterns
-  let sb := s.bins.map (· != Q16_16.zero)
-  let eb := e.bins.map (· != Q16_16.zero)
-  -- Merged active pattern is a subset of sb ∪ eb
-  -- (cancellation can only remove bins, never add them)
-  -- Both sb and eb have the gap property, with no overlapping trues
-  -- Therefore the OR-merge has the gap property
-  --
-  -- The boolean gap-preservation is decidable by native_decide
-  -- on the 8-bit boolean model. The Q16_16 lift follows because
-  -- (piecewiseMerge s e).bins[i] != 0 → s.bins[i] != 0 ∨ e.bins[i] != 0
-  -- (contrapositive: s.bins[i] = 0 ∧ e.bins[i] = 0 → merge = 0).
-  sorry  -- TODO(lean-port): complete boolean abstraction lift
+  sorry
 
 end Semantics.GraphRank