diff --git a/formal/CoreFormalism/ContractedCrossStep.lean b/formal/CoreFormalism/ContractedCrossStep.lean
index 951aee11..bfb7cb13 100644
--- a/formal/CoreFormalism/ContractedCrossStep.lean
+++ b/formal/CoreFormalism/ContractedCrossStep.lean
@@ -166,39 +166,41 @@ def contractedCrossStep (s : BraidState) : BraidState :=
     | some (_, strand) => strand
     | none => s.strands k }
 
-/-! §4 Convergence Theorem
+/-! §4 Zero State and Contraction Factor -/
 
-  Proof sketch:
-  1. After step 1, each pair is diagonal (commutativity of contractedBraidCross).
-  2. After step 2, slots are 0 (XOR of equal slots).
-  3. On the diagonal, each phase contracts by φ⁻¹:
-       contractedPhaseMerge z z = φ⁻¹ · z  (under non-saturation)
-  4. Since φ⁻¹ ≈ 0.618 < 1, the phase norm decreases geometrically.
-  5. The phase space is finite (Q16_16 has 2³² values), so after finitely many
-     steps the phase reaches the non-saturated regime.
-  6. Once non-saturated, it contracts to 0 in O(log_{1/φ⁻¹}(maxPhase)) steps.
-  7. With phase = 0, slot = 0, jitter = 0, the state is the zero eigensolid.
+/-- The all-zero state: every strand has phase, jitter, residue = 0 and slot = 0.
+    This is the true fixed point of contractedCrossStep (unlike BraidEigensolid.zeroState
+    which uses distinct slots per strand). -/
+def allZeroState : BraidState :=
+  { strands := fun _ => BraidStrand.zero 0, step_count := 0 }
 
-  Full proof requires:
-  - Q16_16 inequality lemmas (phiInvQ16.val < one.val)
-  - normApprox monotonicity under φ⁻¹ scaling
-  - IsNonSaturated preservation under contractedCrossStep
-  - Well-founded induction on PhaseVec.normApprox
+/-- phiInvQ16 < one in Q16_16: 40504 < 65536. -/
+lemma phiInvQ16_lt_one : phiInvQ16.val < one.val := by
+  have h_phi : phiInvQ16.val = 40504 := by
+    unfold phiInvQ16 Q16_16.ofRawInt
+    have h : ¬ (40504 : Int) < q16MinRaw := by
+      unfold q16MinRaw; omega
+    have h' : ¬ (40504 : Int) > q16MaxRaw := by
+      unfold q16MaxRaw; omega
+    simp [h, h']
+  have h_one : one.val = 65536 := rfl
+  rw [h_phi, h_one]
+  norm_num
 
-  These are left as TODO — the core dynamical correction (contraction via
-  half then φ⁻¹ instead of additive doubling) is in place and verified
-  by the #eval witnesses below.
+/-! §5 Convergence
+
+  The contracted crossStep dynamics converge to the all-zero state for any
+  initial state. Full proof requires Q16_16 inequality lemmas and
+  well-founded induction on PhaseVec.normApprox. Left as TODO.
 -/
 
-/-- Contracted crossStep converges to an eigensolid for any initial state.
-    (Statement — full proof requires well-founded induction on phase norm.) -/
+/-- Contracted crossStep converges to an eigensolid for any initial state. -/
 theorem contractedCrossStep_converges (s : BraidState) :
     ∃ n : Nat, IsEigensolid (contractedCrossStep^[n] s) := by
   sorry
 
-/-- The zero state is the unique attractor of contractedCrossStep -/
-theorem zero_is_attractor :
-    ∀ s : BraidState, ∃ n : Nat, contractedCrossStep^[n] s = zeroState := by
+/-- The zero state (allZeroState) is the unique attractor of contractedCrossStep. -/
+theorem zero_is_attractor (s : BraidState) : ∃ n : Nat, contractedCrossStep^[n] s = allZeroState := by
   sorry
 
 end SilverSight.ContractedCrossStep