diff --git a/formal/CoreFormalism/BraidStateN.lean b/formal/CoreFormalism/BraidStateN.lean
index e6bf7ff3..4c4565a7 100644
--- a/formal/CoreFormalism/BraidStateN.lean
+++ b/formal/CoreFormalism/BraidStateN.lean
@@ -177,9 +177,10 @@ theorem eigensolid_convergence {n : Nat} (s : BraidStateN n)
 -- The outer strands (i=0, n-1) are "coastal boundaries" where the
 -- eigensolid converges first, mimicking Kelvin wave trapping.
 --
--- BOUNDARY STATUS: `rossby_convergence_bound` is stubbed with sorry.
--- `kelvin_wave_eigensolid` is definitionally true.  The structure
--- definitions and API surface are stable.
+-- BOUNDARY STATUS: `rossby_convergence_bound` is proven (step-count part).
+-- `rossby_energy_dissipation_rate` is the open boundary — it is proven
+-- as `True` but needs a substantive Q16_16 energy lemma to complete.
+-- `kelvin_wave_eigensolid` is definitionally true.
 
 section RotationalWaveCorrespondence
 
@@ -234,18 +235,37 @@ def isAchiral (chiralLabels : Fin n → ChiralLabel) : Prop :=
 variable {n : Nat}
 
 /--
-  Rossby convergence bound: when the braid has non-zero chiral asymmetry,
-  crossStep strictly increases the step count, bounding convergence.
+  Rossby convergence bound: crossStep strictly increases the step count,
+  bounding convergence from below.
 
-  The outer strands (0 and n-1) converge before interior strands,
-  analogously to coastal Kelvin wave trapping.
+  The non-trivial chirality-dependent part (that crossing energy decreases
+  faster under Rossby drift) requires Q16_16 sum-inequality lemmas and is
+  deferred to the TODO below.  The step-count part is definitional.
 -/
--- TODO(RotationalWave): requires Q16_16 arithmetic for signed asymmetry.
--- The structure and API are stable.
 theorem rossby_convergence_bound (s : BraidStateN n) (h_pos : 0 < n)
     (h_rossby : ¬ isAchiral (λ (i : Fin n) => ChiralLabel.achiral_stable)) :
     (crossStep s).step_count > s.step_count := by
-  sorry
+  -- crossStep always increments step_count by 1 (definitional)
+  have h_inc : (crossStep s).step_count = s.step_count + 1 := rfl
+  omega
+
+/--
+  TODO(RotationalWave): under non-zero chiral asymmetry (Rossby regime),
+  the weighted crossing-action decreases faster than in the achiral
+  (Kelvin) regime.  Proving this requires:
+  
+    1. A Q16_16 measure of "crossing energy" that depends on chirality
+    2. A lemma that this measure strictly decreases under crossStep
+    3. A comparison bound showing the decrease is faster when
+       rossbyDriftFromChirality is active
+  
+  Until then, `rossby_convergence_bound` above provides only the
+  trivial step-count guarantee.
+-/
+theorem rossby_energy_dissipation_rate (s : BraidStateN n) (h_pos : 0 < n)
+    (h_rossby : ¬ isAchiral (λ (i : Fin n) => ChiralLabel.achiral_stable)) :
+    True := by
+  trivial
 
 /--
   Kelvin wave eigensolid: an achiral braid converges to a symmetric