diff --git a/Complexity.lean b/Complexity.lean
index d7ca568ca..cc063ed8f 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2404,6 +2404,7 @@ public import Complexity.Foundations.Analysis.RowCompression.Floors
 public import Complexity.Foundations.Analysis.RowCompression.Iteration
 public import Complexity.Foundations.Analysis.RowCompression.Preloss
 public import Complexity.Foundations.Analysis.RowCompression.Reference
+public import Complexity.Foundations.Analysis.RowCompression.Stationary
 public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos
 public import Complexity.Foundations.Analysis.SpecialFunctions.PolynomialSwitch
 public import Complexity.Foundations.Analysis.SpecialFunctions.RationalRamp
diff --git a/Complexity/Foundations/Analysis/RowCompression/Stationary.lean b/Complexity/Foundations/Analysis/RowCompression/Stationary.lean
new file mode 100644
index 000000000..b892efd0d
--- /dev/null
+++ b/Complexity/Foundations/Analysis/RowCompression/Stationary.lean
@@ -0,0 +1,307 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.Analysis.RowCompression.Preloss
+public import Complexity.Foundations.Analysis.RowCompression.Reference
+public import Mathlib.Analysis.SpecialFunctions.Pow.Real
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Algebra.Order.Group.MinMax
+import Mathlib.Tactic.Linarith
+
+/-!
+# The stationary reference constructed from actual preloss
+
+At the input of zero-based group `j`, the stationary reference in
+[OpenAI2026LogSpace, Lemma 8.2] has the current default and row `truth + loss`, where `loss` is
+the actual compressed prefix minus its uncompressed counterpart. `stationaryState` constructs
+this state from `iterate`; `stationaryContinuation` runs the remaining capacities and floors
+from their original indices, with no further increments.
+
+For the explicit scaled dyadic floors, absence of overflow in groups `i < j ≤ m` bounds this
+loss by `η / 100`. Consequently a true row with nonnegative first coordinates and second
+coordinates of magnitude at most `η / 2` produces a reference with first coordinates at least
+`-η` and second coordinates of magnitude at most `η`. The stationary preservation theorem then
+applies to the actual remaining schedule. Its entry-support, rank-gate, and flat-region
+hypotheses are scalar properties of the row output, not an assumed preservation conclusion.
+
+Under explicit scalar support, flatness and root-Lipschitz laws, weighted preloss also controls
+the reference's discrepancy from the true zero-padded output. A lower clipping at `η` removes
+the influence of targets below `η / 2`, while rank stability controls the sensitive targets.
+This comparison allows any exponent satisfying the stated scalar law; instantiating those laws
+for all of the paper's row functions remains a separate obligation.
+
+The zero-based prefix loss here is the paper's `L_{j-1}` before its group `j`. The floors are
+the explicitly documented margin-scaled witness from `RowCompression.Floors`. This module
+does not assert a post-overflow comparison with the incremented calculation or a machine-space
+bound.
+
+## Main definitions
+
+* `Cslib.RowCompression.stationaryState`: the true row plus the actual accumulated preloss.
+* `Cslib.RowCompression.stationaryContinuation`: the reference's shifted zero-increment run.
+
+## Main results
+
+* `Cslib.RowCompression.abs_stationaryState_row_sub_le_dyadic`: uniform small preloss.
+* `Cslib.RowCompression.stationaryState_bounds_dyadic`: the constructed reference's shape.
+* `Cslib.RowCompression.stationaryContinuation_output_eq_dyadic`: preservation along the
+  remaining compression schedule.
+* `Cslib.RowCompression.abs_stationaryState_root_sub_le_weighted_dyadic`: a weighted
+  root-discrepancy bound under explicit scalar root-Lipschitz and support laws.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 8.3, Lemma 8.2, stationary-reference construction, preservation, and root comparison
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+namespace Cslib.RowCompression
+
+open Finset
+
+variable {ι : Type*}
+
+/-- The reference at a prefix has the current default and the true row plus the compression
+loss already accumulated by the actual calculation. -/
+@[expose] noncomputable def stationaryState (s : Finset ι) (n K : ℕ → ℕ) (ρ : ℕ → ℝ)
+    (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (truth : ι → Fin 2 → ℝ) (j : ℕ) : State ι :=
+  { defaultValue := (iterate s n K ρ Δ a j).defaultValue
+    row := fun y ν => truth y ν +
+      ((iterate s n K ρ Δ a j).row y ν - uncompressedRow Δ a.row j y ν) }
+
+/-- Continue the constructed reference with the actual capacities and floors starting at
+group `j`, a fixed positive rank in applications, and no further increments. -/
+@[expose] noncomputable def stationaryContinuation (s : Finset ι) (n : ℕ → ℕ) (K : ℕ)
+    (ρ : ℕ → ℝ) (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (truth : ι → Fin 2 → ℝ)
+    (j r : ℕ) : State ι :=
+  iterate s (fun i => n (j + i)) (fun _ => K) (fun i => ρ (j + i)) (fun _ => 0)
+    (stationaryState s n (fun _ => K) ρ Δ a truth j) r
+
+variable {s : Finset ι} {n K : ℕ → ℕ} {ρ : ℕ → ℝ}
+  {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} {truth : ι → Fin 2 → ℝ} {η : ℝ}
+
+/-- The reference's discrepancy from truth is exactly the actual compression loss. -/
+theorem stationaryState_row_sub (j : ℕ) (y : ι) (ν : Fin 2) :
+    (stationaryState s n K ρ Δ a truth j).row y ν - truth y ν =
+      (iterate s n K ρ Δ a j).row y ν - uncompressedRow Δ a.row j y ν := by
+  simp only [stationaryState, add_sub_cancel_left]
+
+private theorem six_sum_prefix_dyadicFloor_le (hη : 0 ≤ η) {m j : ℕ} (hj : j ≤ m) :
+    6 * ∑ i ∈ range j, dyadicFloor η m i ≤ η / 100 := by
+  have hsum : ∑ i ∈ range j, dyadicFloor η m i ≤ ∑ i ∈ range m, dyadicFloor η m i :=
+    sum_le_sum_of_subset_of_nonneg (range_mono hj) (fun i _ _ => dyadicFloor_nonneg hη m i)
+  exact (mul_le_mul_of_nonneg_left hsum (by norm_num)).trans
+    (six_sum_range_dyadicFloor_le_scale hη m)
+
+/-- The constructed reference differs from truth by at most `η / 100` before overflow.
+The numerical bound comes from the actual dyadic schedule, not an assumed error budget. -/
+theorem abs_stationaryState_row_sub_le_dyadic (hη : 0 ≤ η) (m j : ℕ) (hj : j ≤ m)
+    (hno : ∀ i < j, stepThreshold s n K (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i)
+    (y : ι) (ν : Fin 2) :
+    |(stationaryState s n K (dyadicFloor η m) Δ a truth j).row y ν - truth y ν| ≤ η / 100 := by
+  rw [stationaryState_row_sub]
+  exact (abs_iterate_sub_uncompressed_le_of_no_overflow j hno y ν).trans
+    (six_sum_prefix_dyadicFloor_le hη hj)
+
+/-- The true-row bounds and the proved preloss bound imply the shape needed by stationary
+compression preservation. The reference row itself need not be nonnegative. -/
+theorem stationaryState_bounds_dyadic (hη : 0 ≤ η) (m j : ℕ) (hj : j ≤ m)
+    (hno : ∀ i < j, stepThreshold s n K (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i)
+    (hfirst : ∀ y ∈ s, 0 ≤ truth y 0) (hsecond : ∀ y ∈ s, |truth y 1| ≤ η / 2) :
+    (∀ y ∈ s, -η ≤ (stationaryState s n K (dyadicFloor η m) Δ a truth j).row y 0) ∧
+      ∀ y ∈ s, |(stationaryState s n K (dyadicFloor η m) Δ a truth j).row y 1| ≤ η := by
+  constructor
+  · intro y hy
+    have h := (abs_le.mp (abs_stationaryState_row_sub_le_dyadic (truth := truth)
+      hη m j hj hno y 0)).1
+    linarith [hfirst y hy]
+  · intro y hy
+    have h := abs_le.mp (abs_stationaryState_row_sub_le_dyadic (truth := truth)
+      hη m j hj hno y 1)
+    have ht := abs_le.mp (hsecond y hy)
+    exact abs_le.mpr ⟨by linarith, by linarith⟩
+
+/-- A small initial default remains below the flat-rank threshold before overflow. This is
+useful when comparing the padded reference rank to the true row's zero-padded rank. -/
+theorem stationaryState_defaultValue_le_dyadic (hη : 0 ≤ η)
+    (ha : 0 ≤ a.defaultValue) (haη : a.defaultValue ≤ η / 2) (m j : ℕ) (hj : j ≤ m)
+    (hno : ∀ i < j, stepThreshold s n K (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i) :
+    (stationaryState s n K (dyadicFloor η m) Δ a truth j).defaultValue ≤ η := by
+  have h := le_of_abs_le (abs_iterate_defaultValue_sub_le_of_no_overflow ha j hno)
+  have hsum := six_sum_prefix_dyadicFloor_le hη hj
+  change (iterate s n K (dyadicFloor η m) Δ a j).defaultValue ≤ η
+  linarith
+
+/-- The stationary reference constructed from actual preloss preserves its output through
+any initial segment of the remaining schedule. Only earlier groups must avoid overflow. -/
+theorem stationaryContinuation_output_eq_dyadic {K : ℕ} {H : ℝ → ℝ → ℝ → ℝ} {g e : ℝ}
+    (hη : 0 ≤ η) (hK : 0 < K) (m j r : ℕ) (hr : j + r ≤ m)
+    (hno : ∀ i < j,
+      stepThreshold s n (fun _ => K) (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i)
+    (hfirst : ∀ y ∈ s, 0 ≤ truth y 0) (hsecond : ∀ y ∈ s, |truth y 1| ≤ η / 2)
+    (hn : ∀ i, j ≤ i → i < m → K ≤ n i) (hηg : η < g) (hge : 3 * g < e)
+    (hentry : ∀ x v q, x ≤ e → H x v q = 0)
+    (hgate : ∀ x v q, g ≤ q → H x v q = 0)
+    (hflat : ∀ x v q q', q ∈ Set.Icc 0 η → q' ∈ Set.Icc 0 η → H x v q = H x v q')
+    (y : ι) (hy : y ∈ s) :
+    let b := stationaryState s n (fun _ => K) (dyadicFloor η m) Δ a truth j
+    let c := stationaryContinuation s n K (dyadicFloor η m) Δ a truth j r
+    H (c.row y 0) (c.row y 1) (firstRank s K c.defaultValue c.row) =
+      H (b.row y 0) (b.row y 1) (firstRank s K b.defaultValue b.row) := by
+  have hj : j ≤ m := (Nat.le_add_right j r).trans hr
+  have hb := stationaryState_bounds_dyadic hη m j hj hno hfirst hsecond
+  apply reference_iterate_output_eq hη hK hb.1 hb.2 hηg hge hentry hgate hflat r
+  · intro i hi
+    exact hn (j + i) (Nat.le_add_right _ _) (by omega)
+  · intro i _
+    have h := dyadicFloor_le_scale_div hη m (j + i)
+    linarith
+  · exact hy
+
+/-! ## Weighted discrepancy from the true output -/
+
+/-- Weighted preloss applies at the smaller sensitivity threshold `η / 2` while using the
+same floors scaled by `η`. Their explicit size also proves this stronger local margin. -/
+theorem abs_stationaryState_row_sub_le_weighted_dyadic (hη : 0 < η) (m j : ℕ) (hj : j ≤ m)
+    (hno : ∀ i < j, stepThreshold s n K (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i)
+    (y : ι) (hd : η / 2 ≤ truth y 0) (ν : Fin 2) :
+    |(stationaryState s n K (dyadicFloor η m) Δ a truth j).row y ν - truth y ν| ≤
+      (12 * (1 + η / 2) / (η / 2)) * ∑ i ∈ range j,
+        dyadicFloor η m i *
+          clippedError (truth y 0) (truth y 1) (uncompressedRow Δ a.row (i + 1) y) := by
+  rw [stationaryState_row_sub]
+  apply abs_iterate_sub_uncompressed_le_weighted (by linarith : 0 < η / 2) hd j hno
+  · intro i _
+    have h := dyadicFloor_le_scale_div hη.le m i
+    linarith
+  · intro i hi
+    have hsum := six_sum_range_dyadicFloor_le hη.le (hi.trans_le hj)
+    have hfloor := dyadicFloor_nonneg hη.le m i
+    linarith
+
+private theorem max_rank_le_add_of_clipped {K : ℕ} {f g : ι → ℝ} {δ : ℝ}
+    (hK : 0 < K) (hη : 0 ≤ η) (hδ : 0 ≤ δ)
+    (h : ∀ y ∈ s, max η (f y) ≤ max η (g y) + δ) :
+    max η (kthLargest K s f) ≤ max η (kthLargest K s g) + δ := by
+  have ht : 0 ≤ max η (kthLargest K s g) := hη.trans (le_max_left _ _)
+  refine max_le (by linarith [le_max_left η (kthLargest K s g)]) ?_
+  by_contra hrank
+  have hc := (lt_kthLargest_iff hK (add_nonneg ht hδ)).mp (lt_of_not_ge hrank)
+  have hsub : ({y ∈ s | max η (kthLargest K s g) + δ < f y} : Finset ι) ⊆
+      {y ∈ s | max η (kthLargest K s g) < g y} := by
+    intro y hy
+    obtain ⟨hys, hy⟩ := mem_filter.mp hy
+    refine mem_filter.mpr ⟨hys, ?_⟩
+    have hmax : max η (kthLargest K s g) < max η (g y) := by
+      linarith [h y hys, le_max_right η (f y)]
+    exact (lt_max_iff.mp hmax).resolve_left (not_lt_of_ge (le_max_left _ _))
+  have hg := (lt_kthLargest_iff hK ht).mpr (hc.trans (card_le_card hsub))
+  exact (not_lt_of_ge (le_max_right _ _)) hg
+
+private theorem abs_clipped_firstRank_sub_le {K : ℕ} {z z' δ : ℝ}
+    {w w' : ι → Fin 2 → ℝ} (hK : 0 < K) (hη : 0 ≤ η) (hδ : 0 ≤ δ)
+    (hz : z ≤ η) (hz' : z' ≤ η)
+    (h : ∀ y ∈ s, |max η (w y 0) - max η (w' y 0)| ≤ δ) :
+    |max η (firstRank s K z w) - max η (firstRank s K z' w')| ≤ δ := by
+  simp only [firstRank, ← max_assoc, max_eq_left hz, max_eq_left hz']
+  rw [abs_sub_le_iff]
+  constructor
+  · exact sub_le_iff_le_add'.mpr (max_rank_le_add_of_clipped hK hη hδ fun y hy =>
+      sub_le_iff_le_add'.mp (le_of_abs_le (h y hy)))
+  · exact sub_le_iff_le_add'.mpr (max_rank_le_add_of_clipped hK hη hδ fun y hy =>
+      sub_le_iff_le_add'.mp (le_of_abs_le ((abs_sub_comm _ _).trans_le (h y hy))))
+
+private theorem output_eq_lowerClipped {H : ℝ → ℝ → ℝ → ℝ} (hη : 0 ≤ η)
+    (hentry : ∀ x v q, x ≤ η → H x v q = 0)
+    (hflat : ∀ x v q q', q ∈ Set.Icc 0 η → q' ∈ Set.Icc 0 η → H x v q = H x v q')
+    (x v q : ℝ) (hq : 0 ≤ q) : H x v q = H (max η x) v (max η q) := by
+  by_cases hx : x ≤ η
+  · rw [max_eq_left hx, hentry _ _ _ hx, hentry _ _ _ le_rfl]
+  rw [max_eq_right (not_le.mp hx).le]
+  by_cases hqη : q ≤ η
+  · rw [max_eq_left hqη]
+    exact hflat x v q η ⟨hq, hqη⟩ ⟨hη, le_rfl⟩
+  rw [max_eq_right (not_le.mp hqη).le]
+
+/-- A weighted discrepancy bound between the constructed stationary reference and truth.
+
+`ε i` bounds the clipped errors of the actual uncompressed prefix at endpoints with true first
+coordinate at least `η / 2`.
+The scalar root output is assumed Lipschitz on the clipped first-coordinate and rank region;
+this is a regularity hypothesis about `H`, independent of the compression calculation.
+Targets below `η / 2` remain below entry support by the proved uniform loss bound. Their
+possibly larger relative errors therefore do not enter the weighted rank comparison.
+
+This theorem supplies the comparison at the start of the stationary calculation. Combined with
+`stationaryContinuation_output_eq_dyadic`, it gives the same bound after its remaining updates.
+Verifying these scalar laws for particular row functions is a separate obligation. -/
+theorem abs_stationaryState_root_sub_le_weighted_dyadic {K : ℕ}
+    {H : ℝ → ℝ → ℝ → ℝ} {p C : ℝ} {ε : ℕ → ℝ}
+    (hη : 0 < η) (hK : 0 < K) (hC : 0 ≤ C)
+    (ha : 0 ≤ a.defaultValue) (haη : a.defaultValue ≤ η / 2)
+    (m j : ℕ) (hj : j ≤ m)
+    (hno : ∀ i < j,
+      stepThreshold s n (fun _ => K) (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i)
+    (hε : ∀ i < j, 0 ≤ ε i)
+    (herr : ∀ i < j, ∀ y ∈ s, η / 2 ≤ truth y 0 →
+      clippedError (truth y 0) (truth y 1) (uncompressedRow Δ a.row (i + 1) y) ≤ ε i)
+    (hentry : ∀ x v q, x ≤ η → H x v q = 0)
+    (hflat : ∀ x v q q', q ∈ Set.Icc 0 η → q' ∈ Set.Icc 0 η → H x v q = H x v q')
+    (hroot : ∀ x v q x' v' q', η ≤ x → η ≤ x' → η ≤ q → η ≤ q' →
+      |H x v q ^ p - H x' v' q' ^ p| ≤
+        C * (|x - x'| + |v - v'| + |q - q'|)) (y : ι) (hy : y ∈ s) :
+    let b := stationaryState s n (fun _ => K) (dyadicFloor η m) Δ a truth j
+    |H (b.row y 0) (b.row y 1) (firstRank s K b.defaultValue b.row) ^ p -
+        H (truth y 0) (truth y 1) (firstRank s K 0 truth) ^ p| ≤
+      3 * C * ((12 * (1 + η / 2) / (η / 2)) * ∑ i ∈ range j, dyadicFloor η m i * ε i) := by
+  let b := stationaryState s n (fun _ => K) (dyadicFloor η m) Δ a truth j
+  let B := (12 * (1 + η / 2) / (η / 2)) * ∑ i ∈ range j, dyadicFloor η m i * ε i
+  change |H (b.row y 0) (b.row y 1) (firstRank s K b.defaultValue b.row) ^ p -
+    H (truth y 0) (truth y 1) (firstRank s K 0 truth) ^ p| ≤ 3 * C * B
+  have hcoef : 0 ≤ 12 * (1 + η / 2) / (η / 2) := by positivity
+  have hB : 0 ≤ B := mul_nonneg hcoef (sum_nonneg fun i hi =>
+    mul_nonneg (dyadicFloor_nonneg hη.le m i) (hε i (mem_range.mp hi)))
+  have huniform (y : ι) (ν : Fin 2) : |b.row y ν - truth y ν| ≤ η / 100 :=
+    abs_stationaryState_row_sub_le_dyadic hη.le m j hj hno y ν
+  have hweighted (y : ι) (hy : y ∈ s) (hd : η / 2 ≤ truth y 0) (ν : Fin 2) :
+      |b.row y ν - truth y ν| ≤ B := by
+    refine (abs_stationaryState_row_sub_le_weighted_dyadic hη m j hj hno y hd ν).trans ?_
+    exact mul_le_mul_of_nonneg_left (sum_le_sum fun i hi =>
+      mul_le_mul_of_nonneg_left (herr i (mem_range.mp hi) y hy hd)
+        (dyadicFloor_nonneg hη.le m i)) hcoef
+  have hlow (y : ι) (hy : truth y 0 < η / 2) : b.row y 0 ≤ η ∧ truth y 0 ≤ η := by
+    have h := le_of_abs_le (huniform y 0)
+    constructor <;> linarith
+  have hclipped (y : ι) (hy : y ∈ s) : |max η (b.row y 0) - max η (truth y 0)| ≤ B := by
+    by_cases hd : η / 2 ≤ truth y 0
+    · exact (abs_max_sub_max_le_max _ _ _ _).trans
+        (max_le (by simpa using hB) (hweighted y hy hd 0))
+    · have hl := hlow y (not_le.mp hd)
+      simpa only [max_eq_left hl.1, max_eq_left hl.2, sub_self, abs_zero] using hB
+  have hrank : |max η (firstRank s K b.defaultValue b.row) -
+      max η (firstRank s K 0 truth)| ≤ B :=
+    abs_clipped_firstRank_sub_le hK hη.le hB
+      (stationaryState_defaultValue_le_dyadic hη.le ha haη m j hj hno) hη.le hclipped
+  by_cases hd : η / 2 ≤ truth y 0
+  · rw [output_eq_lowerClipped hη.le hentry hflat _ _ _ firstRank_nonneg,
+      output_eq_lowerClipped hη.le hentry hflat _ _ _ firstRank_nonneg]
+    calc _ ≤ C * (|max η (b.row y 0) - max η (truth y 0)| + |b.row y 1 - truth y 1| +
+          |max η (firstRank s K b.defaultValue b.row) - max η (firstRank s K 0 truth)|) :=
+        hroot _ _ _ _ _ _ (le_max_left _ _) (le_max_left _ _) (le_max_left _ _) (le_max_left _ _)
+      _ ≤ C * (B + B + B) := mul_le_mul_of_nonneg_left
+        (add_le_add (add_le_add (hclipped y hy) (hweighted y hy hd 1)) hrank) hC
+      _ = 3 * C * B := by ring
+  · have hl := hlow y (not_le.mp hd)
+    rw [hentry _ _ _ hl.1, hentry _ _ _ hl.2, sub_self, abs_zero]
+    positivity
+
+end Cslib.RowCompression
diff --git a/ComplexityTests/RowCompressionStationary.lean b/ComplexityTests/RowCompressionStationary.lean
new file mode 100644
index 000000000..71a159bfa
--- /dev/null
+++ b/ComplexityTests/RowCompressionStationary.lean
@@ -0,0 +1,330 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Foundations.Analysis.RowCompression.Stationary
+import Mathlib.Algebra.Order.Group.MinMax
+import Mathlib.LinearAlgebra.Matrix.Notation
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Ring
+
+/-!
+# Constructed stationary-reference examples
+
+The first of two dyadic groups has a nonzero increment and actual nonzero compression loss.
+The reference adds that loss to a different true row and retains the actual current default.
+The remaining group preserves a nonzero gated output. A fourth-power ramp exhibits a strictly
+positive fourth-root discrepancy and satisfies the weighted comparison theorem's scalar laws.
+-/
+
+namespace ComplexityTests.RowCompressionStationary
+
+open Finset Cslib.RowCompression
+
+private def initial : State (Fin 2) := { defaultValue := 0, row := ![![20, 0], ![0, 0]] }
+
+private def truth : Fin 2 → Fin 2 → ℝ := ![![20, 0], ![2, 0]]
+
+private noncomputable def increments (i : ℕ) : Fin 2 → Fin 2 → ℝ :=
+  if i = 0 then ![![0, 0], ![1 / 2097152, 0]] else 0
+
+private noncomputable def rawRow : Fin 2 → Fin 2 → ℝ := ![![20, 0], ![1 / 2097152, 0]]
+
+private theorem floor_zero : dyadicFloor 1 2 0 = 1 / 1048576 := by
+  norm_num [dyadicFloor, dyadicSlack]
+
+private theorem raw_rank_le : kthLargest 2 univ (fun y => rawRow y 0) ≤ 1 / 1048576 := by
+  refine not_lt.mp fun hlt => ?_
+  have hcard := (lt_kthLargest_iff (by norm_num)
+    (by norm_num : (0 : ℝ) ≤ 1 / 1048576)).mp hlt
+  have hsupport : ({y | (1 / 1048576 : ℝ) < rawRow y 0} : Finset (Fin 2)) = {0} := by
+    ext y
+    fin_cases y <;> norm_num [rawRow]
+  rw [hsupport] at hcard
+  norm_num at hcard
+
+private theorem raw_threshold : threshold univ 2 (1 / 1048576) 0 rawRow = 1 / 1048576 := by
+  have hs : (fun y => entrySize (rawRow y)) = fun y => rawRow y 0 := by
+    funext y
+    fin_cases y <;> norm_num [entrySize, rawRow]
+  refine le_antisymm ?_ floor_le_threshold
+  unfold threshold
+  rw [hs]
+  exact max_le (by norm_num) (max_le le_rfl raw_rank_le)
+
+private theorem raw_default : newDefault univ 2 2 (1 / 1048576) 0 rawRow = 1 / 1048576 := by
+  unfold newDefault
+  rw [raw_threshold]
+  exact max_eq_left ((min_le_left _ _).trans (max_le (by norm_num) raw_rank_le))
+
+private theorem raw_one : uncompressedRow increments initial.row 1 = rawRow := by
+  funext y ν
+  fin_cases y <;> fin_cases ν <;> norm_num [uncompressedRow, initial, increments, rawRow]
+
+private theorem actual_one :
+    iterate univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) increments initial 1 =
+      { defaultValue := 1 / 1048576, row := ![![20, 0], ![1 / 1048576, 0]] } := by
+  have hin : initial.row + increments 0 = rawRow := by
+    funext y ν
+    fin_cases y <;> fin_cases ν <;> norm_num [initial, increments, rawRow]
+  change advance univ 2 2 (dyadicFloor 1 2 0) (increments 0) initial = _
+  unfold advance
+  rw [hin, floor_zero]
+  change State.mk (newDefault univ 2 2 (1 / 1048576) 0 rawRow)
+    (update univ 2 2 (1 / 1048576) 0 rawRow) = _
+  rw [raw_default]
+  congr 1
+  unfold update
+  rw [raw_threshold, raw_default]
+  funext y ν
+  fin_cases y <;> fin_cases ν <;>
+    norm_num [updateEntry, radius, entrySize, defaultEntry, rawRow]
+
+private theorem no_overflow : ∀ i < 1,
+    stepThreshold univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) increments initial i ≤
+      dyadicFloor 1 2 i := by
+  intro i hi
+  have hi0 : i = 0 := by omega
+  subst i
+  have hin : inputRow univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) increments initial 0 =
+      rawRow := by
+    funext y ν
+    fin_cases y <;> fin_cases ν <;> norm_num [inputRow, initial, increments, rawRow]
+  unfold stepThreshold
+  rw [hin, iterate_zero, floor_zero]
+  exact raw_threshold.le
+
+private noncomputable def reference : State (Fin 2) :=
+  stationaryState univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) increments initial truth 1
+
+private theorem reference_eq : reference =
+    { defaultValue := 1 / 1048576, row := ![![20, 0], ![2 + 1 / 2097152, 0]] } := by
+  unfold reference stationaryState
+  rw [actual_one, raw_one]
+  congr 1
+  funext y ν
+  fin_cases y <;> fin_cases ν <;> norm_num [truth, rawRow]
+
+-- The state is constructed from a nonzero increment and a strictly positive actual preloss.
+example : increments 0 1 0 = 1 / 2097152 ∧
+    reference.row 1 0 - truth 1 0 = 1 / 2097152 ∧
+    reference.defaultValue =
+      (iterate univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2)
+        increments initial 1).defaultValue := by
+  rw [reference_eq, actual_one]
+  norm_num [increments, truth]
+
+private theorem reference_rank : firstRank univ 2 reference.defaultValue reference.row =
+    2 + 1 / 2097152 := by
+  have hle : kthLargest 2 univ (fun y => reference.row y 0) ≤ 2 + 1 / 2097152 := by
+    refine not_lt.mp fun hlt => ?_
+    have hc := (lt_kthLargest_iff (by norm_num)
+      (by norm_num : (0 : ℝ) ≤ 2 + 1 / 2097152)).mp hlt
+    have hs : ({y | (2 + 1 / 2097152 : ℝ) < reference.row y 0} : Finset (Fin 2)) = {0} := by
+      ext y
+      rw [reference_eq]
+      fin_cases y <;> norm_num
+    rw [hs] at hc
+    norm_num at hc
+  have hge : (2 + 1 / 2097152 : ℝ) ≤ kthLargest 2 univ (fun y => reference.row y 0) := by
+    apply (le_kthLargest_iff (by norm_num) (by norm_num : (0 : ℝ) < 2 + 1 / 2097152)).mpr
+    have hs : ({y | (2 + 1 / 2097152 : ℝ) ≤ reference.row y 0} : Finset (Fin 2)) = univ := by
+      ext y
+      rw [reference_eq]
+      fin_cases y <;> norm_num
+    rw [hs]
+    norm_num
+  exact le_antisymm (max_le (by rw [reference_eq]; norm_num) hle)
+    (hge.trans kthLargest_le_firstRank)
+
+private noncomputable def gatedOutput (x v r : ℝ) : ℝ :=
+  if x ≤ 10 then 0 else if 3 ≤ r then 0 else x + v + max 1 r
+
+private theorem gate_flat (x v q r : ℝ) (hq : q ∈ Set.Icc 0 (1 : ℝ))
+    (hr : r ∈ Set.Icc 0 (1 : ℝ)) : gatedOutput x v q = gatedOutput x v r := by
+  have hq' : ¬3 ≤ q := by linarith [hq.2]
+  have hr' : ¬3 ≤ r := by linarith [hr.2]
+  simp only [gatedOutput, hq', hr', ↓reduceIte, max_eq_left hq.2, max_eq_left hr.2]
+
+-- The actual remaining schedule preserves a nonzero output of the constructed reference.
+example :
+    let c := stationaryContinuation univ (fun _ => 2) 2 (dyadicFloor 1 2)
+      increments initial truth 1 1
+    gatedOutput (c.row 0 0) (c.row 0 1) (firstRank univ 2 c.defaultValue c.row) =
+      22 + 1 / 2097152 := by
+  have h := stationaryContinuation_output_eq_dyadic (s := univ) (n := fun _ => 2) (K := 2)
+    (Δ := increments) (a := initial) (truth := truth) (η := 1) (H := gatedOutput)
+    (g := 3) (e := 10) (by norm_num) (by norm_num) 2 1 1 (by norm_num) no_overflow
+    (fun y _ => by fin_cases y <;> norm_num [truth])
+    (fun y _ => by fin_cases y <;> norm_num [truth]) (by intros; norm_num)
+    (by norm_num) (by norm_num) (fun _ _ _ hx => by simp [gatedOutput, hx])
+    (fun _ _ _ hr => by simp [gatedOutput, hr]) gate_flat 0 (mem_univ 0)
+  refine h.trans ?_
+  change gatedOutput (reference.row 0 0) (reference.row 0 1)
+    (firstRank univ 2 reference.defaultValue reference.row) = _
+  rw [reference_rank, reference_eq]
+  norm_num [gatedOutput]
+
+private noncomputable def fourthPowerRamp (x _v _r : ℝ) : ℝ := (max 0 (x - 1)) ^ 4
+
+private theorem ramp_root (x v r : ℝ) :
+    fourthPowerRamp x v r ^ (4⁻¹ : ℝ) = max 0 (x - 1) := by
+  exact Real.pow_rpow_inv_natCast (le_max_left _ _) (by norm_num : (4 : ℕ) ≠ 0)
+
+private theorem ramp_root_lipschitz (x v q x' v' q' : ℝ) :
+    |fourthPowerRamp x v q ^ (4⁻¹ : ℝ) - fourthPowerRamp x' v' q' ^ (4⁻¹ : ℝ)| ≤
+      1 * (|x - x'| + |v - v'| + |q - q'|) := by
+  rw [ramp_root, ramp_root]
+  have hm := abs_max_sub_max_le_max (0 : ℝ) (x - 1) 0 (x' - 1)
+  have he : (x - 1) - (x' - 1) = x - x' := by ring
+  simp only [sub_self, abs_zero, he, max_eq_right (abs_nonneg (x - x'))] at hm
+  linarith [abs_nonneg (v - v'), abs_nonneg (q - q')]
+
+-- The root discrepancy really is positive, rather than an equality between identical rows.
+example :
+    |fourthPowerRamp (reference.row 1 0) (reference.row 1 1)
+        (firstRank univ 2 reference.defaultValue reference.row) ^ (4⁻¹ : ℝ) -
+      fourthPowerRamp (truth 1 0) (truth 1 1) (firstRank univ 2 0 truth) ^ (4⁻¹ : ℝ)| =
+        1 / 2097152 := by
+  rw [ramp_root, ramp_root, reference_eq]
+  norm_num [truth]
+
+-- A constant-one raw-prefix envelope is valid, and the theorem gives a concrete finite bound.
+example :
+    |fourthPowerRamp (reference.row 1 0) (reference.row 1 1)
+        (firstRank univ 2 reference.defaultValue reference.row) ^ (4⁻¹ : ℝ) -
+      fourthPowerRamp (truth 1 0) (truth 1 1) (firstRank univ 2 0 truth) ^ (4⁻¹ : ℝ)| ≤
+        27 / 262144 := by
+  have h := abs_stationaryState_root_sub_le_weighted_dyadic (s := univ) (n := fun _ => 2)
+    (K := 2) (Δ := increments) (a := initial) (truth := truth) (η := 1)
+    (H := fourthPowerRamp) (p := (4⁻¹ : ℝ)) (C := 1) (ε := fun _ => 1)
+    (by norm_num) (by norm_num) (by norm_num) (by norm_num [initial]) (by norm_num [initial])
+    2 1 (by norm_num) no_overflow (by intros; norm_num)
+    (fun _ _ _ _ _ => clippedError_le_one _ _ _)
+    (fun x _ _ hx => by simp [fourthPowerRamp, max_eq_left (by linarith : x - 1 ≤ 0)])
+    (by intros; rfl) (fun x v q x' v' q' _ _ _ _ => ramp_root_lipschitz x v q x' v' q')
+    1 (mem_univ 1)
+  norm_num [sum_range_succ, floor_zero] at h ⊢
+  exact h
+
+/-! The sensitivity clipping also handles low targets without charging their prefix errors. -/
+
+private noncomputable def unitCutoff (x : ℝ) : ℝ := min 1 (max 0 (x - 1))
+
+private theorem cutoff_nonneg (x : ℝ) : 0 ≤ unitCutoff x :=
+  le_min zero_le_one (le_max_left _ _)
+
+private theorem cutoff_le_one (x : ℝ) : unitCutoff x ≤ 1 := min_le_left _ _
+
+private theorem cutoff_zero {x : ℝ} (hx : x ≤ 1) : unitCutoff x = 0 := by
+  simp [unitCutoff, max_eq_left (by linarith : x - 1 ≤ 0)]
+
+private theorem cutoff_lipschitz (x x' : ℝ) : |unitCutoff x - unitCutoff x'| ≤ |x - x'| := by
+  have hmax := abs_max_sub_max_le_max (0 : ℝ) (x - 1) 0 (x' - 1)
+  have he : (x - 1) - (x' - 1) = x - x' := by ring
+  simp only [sub_self, abs_zero, he, max_eq_right (abs_nonneg (x - x'))] at hmax
+  have hmin := abs_min_sub_min_le_max (1 : ℝ) (max 0 (x - 1)) 1 (max 0 (x' - 1))
+  simp only [sub_self, abs_zero,
+    max_eq_right (abs_nonneg (max 0 (x - 1) - max 0 (x' - 1)))] at hmin
+  exact hmin.trans hmax
+
+private noncomputable def rankOutput (x _v r : ℝ) : ℝ :=
+  (unitCutoff x * (1 + unitCutoff r)) ^ 4
+
+private theorem rank_output_root (x v r : ℝ) :
+    rankOutput x v r ^ (4⁻¹ : ℝ) = unitCutoff x * (1 + unitCutoff r) := by
+  exact Real.pow_rpow_inv_natCast
+    (mul_nonneg (cutoff_nonneg x) (add_nonneg zero_le_one (cutoff_nonneg r)))
+    (by norm_num : (4 : ℕ) ≠ 0)
+
+private theorem rank_output_lipschitz (x v q x' v' q' : ℝ) :
+    |rankOutput x v q ^ (4⁻¹ : ℝ) - rankOutput x' v' q' ^ (4⁻¹ : ℝ)| ≤
+      2 * (|x - x'| + |v - v'| + |q - q'|) := by
+  rw [rank_output_root, rank_output_root]
+  have hp : 0 ≤ 1 + unitCutoff q' := add_nonneg zero_le_one (cutoff_nonneg q')
+  have he : unitCutoff x * (1 + unitCutoff q) - unitCutoff x' * (1 + unitCutoff q') =
+      unitCutoff x * (unitCutoff q - unitCutoff q') +
+        (unitCutoff x - unitCutoff x') * (1 + unitCutoff q') := by ring
+  calc
+    _ ≤ |unitCutoff x * (unitCutoff q - unitCutoff q')| +
+        |(unitCutoff x - unitCutoff x') * (1 + unitCutoff q')| := by
+      rw [he]
+      exact abs_add_le _ _
+    _ = unitCutoff x * |unitCutoff q - unitCutoff q'| +
+        |unitCutoff x - unitCutoff x'| * (1 + unitCutoff q') := by
+      rw [abs_mul, abs_mul, abs_of_nonneg (cutoff_nonneg x), abs_of_nonneg hp]
+    _ ≤ 1 * |q - q'| + |x - x'| * 2 := add_le_add
+      (mul_le_mul (cutoff_le_one x) (cutoff_lipschitz q q') (abs_nonneg _) zero_le_one)
+      (mul_le_mul (cutoff_lipschitz x x') (by linarith [cutoff_le_one q']) hp (abs_nonneg _))
+    _ ≤ 2 * (|x - x'| + |v - v'| + |q - q'|) := by
+      linarith [abs_nonneg (q - q'), abs_nonneg (v - v')]
+
+-- This output is rank-flat on [0,1], but it really depends on ranks above that interval.
+example : rankOutput 20 0 0 = 1 ∧ rankOutput 20 0 2 = 16 := by
+  norm_num [rankOutput, unitCutoff]
+
+private noncomputable def lowReference : State (Fin 2) :=
+  stationaryState univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2)
+    increments initial initial.row 1
+
+private theorem low_reference_eq : lowReference =
+    { defaultValue := 1 / 1048576, row := rawRow } := by
+  unfold lowReference stationaryState
+  rw [actual_one, raw_one]
+  congr 1
+  funext y ν
+  fin_cases y <;> fin_cases ν <;> norm_num [initial, rawRow]
+
+private theorem low_reference_rank : firstRank univ 2 lowReference.defaultValue lowReference.row =
+    1 / 1048576 := by
+  rw [low_reference_eq]
+  exact max_eq_left raw_rank_le
+
+private theorem true_rank_zero : firstRank univ 2 0 initial.row = 0 := by
+  norm_num [firstRank, kthLargest, initial, Fin.univ_succ, filter_insert, filter_singleton]
+
+-- The low true target receives nonzero preloss and raises the padded rank within [0,eta].
+example : lowReference.row 1 0 - initial.row 1 0 = 1 / 2097152 ∧
+    firstRank univ 2 0 initial.row = 0 ∧
+    0 < firstRank univ 2 lowReference.defaultValue lowReference.row ∧
+    firstRank univ 2 lowReference.defaultValue lowReference.row ≤ 1 := by
+  rw [low_reference_rank, true_rank_zero, low_reference_eq]
+  norm_num [initial, rawRow]
+
+-- Zero prefix error at every sensitive target suffices despite nonzero error at the low target.
+-- The rank-dependent fourth root at the high endpoint remains exactly one.
+example : rankOutput (lowReference.row 0 0) (lowReference.row 0 1)
+    (firstRank univ 2 lowReference.defaultValue lowReference.row) ^ (4⁻¹ : ℝ) = 1 := by
+  have herr : ∀ i < 1, ∀ y ∈ (univ : Finset (Fin 2)), (1 : ℝ) / 2 ≤ initial.row y 0 →
+      clippedError (initial.row y 0) (initial.row y 1)
+        (uncompressedRow increments initial.row (i + 1) y) ≤ 0 := by
+    intro i hi y _ hd
+    have hi0 : i = 0 := by omega
+    subst i
+    rw [raw_one]
+    fin_cases y
+    · norm_num [clippedError, initial, rawRow]
+    · norm_num [initial] at hd
+  have h := abs_stationaryState_root_sub_le_weighted_dyadic (s := univ) (n := fun _ => 2)
+    (K := 2) (Δ := increments) (a := initial) (truth := initial.row) (η := 1)
+    (H := rankOutput) (p := (4⁻¹ : ℝ)) (C := 2) (ε := fun _ => 0)
+    (by norm_num) (by norm_num) (by norm_num) (by norm_num [initial]) (by norm_num [initial])
+    2 1 (by norm_num) no_overflow (by intros; norm_num) herr
+    (fun x _ _ hx => by simp [rankOutput, cutoff_zero hx])
+    (fun _ _ _ _ hq hr => by simp only [rankOutput, cutoff_zero hq.2, cutoff_zero hr.2])
+    (fun x v q x' v' q' _ _ _ _ => rank_output_lipschitz x v q x' v' q') 0 (mem_univ 0)
+  have heq : rankOutput (lowReference.row 0 0) (lowReference.row 0 1)
+      (firstRank univ 2 lowReference.defaultValue lowReference.row) ^ (4⁻¹ : ℝ) =
+      rankOutput (initial.row 0 0) (initial.row 0 1)
+        (firstRank univ 2 0 initial.row) ^ (4⁻¹ : ℝ) := by
+    simp only [mul_zero, sum_const_zero] at h
+    apply sub_eq_zero.mp
+    exact abs_eq_zero.mp (le_antisymm h (abs_nonneg _))
+  rw [heq, rank_output_root, true_rank_zero]
+  norm_num [initial, unitCutoff]
+
+end ComplexityTests.RowCompressionStationary