diff --git a/Complexity.lean b/Complexity.lean
index dba79c39b..6a22e6a9b 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2390,6 +2390,7 @@ public import Complexity.Foundations.Analysis.RowCompression
 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.SpecialFunctions.Arccos
 public import Complexity.Foundations.Analysis.SpecialFunctions.PolynomialSwitch
 public import Complexity.Foundations.Analysis.SpecialFunctions.SmoothSwitch
diff --git a/Complexity/Foundations/Analysis/RowCompression/Reference.lean b/Complexity/Foundations/Analysis/RowCompression/Reference.lean
new file mode 100644
index 000000000..e366049ce
--- /dev/null
+++ b/Complexity/Foundations/Analysis/RowCompression/Reference.lean
@@ -0,0 +1,292 @@
+/-
+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.Iteration
+import Mathlib.Tactic.Linarith
+
+/-!
+# Stationary reference rows under compression
+
+This module proves the stationary-output assertion of [OpenAI2026LogSpace, Lemma 8.2].
+The first coordinates of a reference row are at least `-η`, and the absolute values of its
+second coordinates are at most `η`. Compression has floor at most `η` and capacity `n ≥ K`.
+Write `q` for the `K`-th first-coordinate rank padded by the old default. The actual threshold,
+new default and new padded rank are at most `max η q`. If `η < q`, the padded rank is preserved
+exactly; otherwise both old and new ranks remain in `[0,η]`. The row bounds are preserved too.
+
+A row output `H(first, second, rank)` is preserved when it is zero below an entry threshold `e`,
+zero above a gate-closing rank `g`, and independent of rank within `[0,η]`, where
+`η < g` and `3 * g < e`. When the gate is open, entries above `e` are unchanged and entries
+below `e` cannot enter the support. The theorem also iterates the concrete updates with no
+increments, allowing arbitrary floors at most `η` and capacities at least the fixed rank `K`.
+
+This is output preservation, not equality of whole rows: defaults and small entries may move.
+No root-discrepancy bound, comparison with a perturbed reference, or post-overflow error estimate
+is asserted. The arithmetic rank includes zero padding; for the source's nonnegative defaults
+it agrees with padding by arbitrarily many copies of the default.
+
+## Main definitions
+
+* `Cslib.RowCompression.firstRank`: the padded first-coordinate rank.
+
+## Main results
+
+* `Cslib.RowCompression.reference_threshold_le`: the actual threshold is at most `max η q`.
+* `Cslib.RowCompression.reference_firstRank_eq`: ranks above `η` are preserved exactly.
+* `Cslib.RowCompression.reference_update_output_eq`: a gated row output is preserved.
+* `Cslib.RowCompression.reference_iterate_output_eq`: preservation through zero-increment
+  iteration.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 8.3, Lemma 8.2, stationary-reference assertion
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+namespace Cslib.RowCompression
+
+open Finset
+
+variable {ι : Type*}
+
+/-- The first-coordinate rank, padded by the old default as well as zero. For a nonnegative
+default this is the rank obtained by adjoining arbitrarily many copies of `(z,0)`. -/
+@[expose] noncomputable def firstRank (s : Finset ι) (K : ℕ) (z : ℝ)
+    (w : ι → Fin 2 → ℝ) : ℝ := max z (kthLargest K s fun y => w y 0)
+
+variable {s : Finset ι} {n K : ℕ} {ρ z η : ℝ} {w : ι → Fin 2 → ℝ}
+
+theorem firstRank_nonneg : 0 ≤ firstRank s K z w :=
+  kthLargest_nonneg.trans (le_max_right _ _)
+
+theorem default_le_firstRank : z ≤ firstRank s K z w := le_max_left _ _
+
+theorem kthLargest_le_firstRank : kthLargest K s (fun y => w y 0) ≤ firstRank s K z w :=
+  le_max_right _ _
+
+/-- With small negative first coordinates and small second coordinates, size ranks cannot
+exceed the first-coordinate rank or `η`, whichever is larger. -/
+theorem reference_threshold_le (hη : 0 ≤ η) (hρ : ρ ≤ η) (hK : 0 < K) (hKn : K ≤ n)
+    (hfirst : ∀ y ∈ s, -η ≤ w y 0) (hsecond : ∀ y ∈ s, |w y 1| ≤ η) :
+    threshold s n ρ z w ≤ max η (firstRank s K z w) := by
+  let Q := max η (firstRank s K z w)
+  have hηQ : η ≤ Q := le_max_left _ _
+  have hqQ : firstRank s K z w ≤ Q := le_max_right _ _
+  have hQ0 : 0 ≤ Q := hη.trans hηQ
+  have hrank : kthLargest n s (fun y => entrySize (w y)) ≤ Q := by
+    by_contra h
+    have hcard := (lt_kthLargest_iff (hK.trans_le hKn) hQ0).mp (lt_of_not_ge h)
+    have hsub : ({y ∈ s | Q < entrySize (w y)} : Finset ι) ⊆ {y ∈ s | Q < w y 0} := by
+      intro y hy
+      obtain ⟨hys, hy⟩ := mem_filter.mp hy
+      refine mem_filter.mpr ⟨hys, ?_⟩
+      by_contra hfirstQ
+      have hsize : entrySize (w y) ≤ Q :=
+        max_le (abs_le.mpr ⟨by linarith [hfirst y hys], not_lt.mp hfirstQ⟩)
+          ((hsecond y hys).trans hηQ)
+      exact (not_lt_of_ge hsize) hy
+    have hfirstRank : Q < kthLargest K s (fun y => w y 0) :=
+      (lt_kthLargest_iff hK hQ0).mpr (hKn.trans (hcard.trans (card_le_card hsub)))
+    exact (not_lt_of_ge (kthLargest_le_firstRank.trans hqQ)) hfirstRank
+  exact max_le (default_le_firstRank.trans hqQ) (max_le (hρ.trans hηQ) hrank)
+
+/-- The new default is at most the larger of `η` and the old padded rank. -/
+theorem reference_newDefault_le (hη : 0 ≤ η) (hρ : ρ ≤ η) (hK : 0 < K) (hKn : K ≤ n)
+    (hfirst : ∀ y ∈ s, -η ≤ w y 0) (hsecond : ∀ y ∈ s, |w y 1| ≤ η) :
+    newDefault s n K ρ z w ≤ max η (firstRank s K z w) :=
+  max_le (reference_threshold_le hη hρ hK hKn hfirst hsecond)
+    ((min_le_left _ _).trans (le_max_right _ _))
+
+/-- Moving coordinates toward a nonnegative first-coordinate default and zero second
+coordinate preserves the reference row's small negative and second-coordinate bounds. -/
+theorem reference_update_bounds (hη : 0 ≤ η) {y : ι}
+    (hfirst : -η ≤ w y 0) (hsecond : |w y 1| ≤ η) :
+    -η ≤ update s n K ρ z w y 0 ∧ |update s n K ρ z w y 1| ≤ η := by
+  have h0 := update_mem_Icc (s := s) (n := n) (K := K) (ρ := ρ) (z := z) (w := w) y 0
+  have h1 := update_mem_Icc (s := s) (n := n) (K := K) (ρ := ρ) (z := z) (w := w) y 1
+  change min (w y 0) (newDefault s n K ρ z w) ≤ update s n K ρ z w y 0 ∧
+    update s n K ρ z w y 0 ≤ max (w y 0) (newDefault s n K ρ z w) at h0
+  change min (w y 1) 0 ≤ update s n K ρ z w y 1 ∧
+    update s n K ρ z w y 1 ≤ max (w y 1) 0 at h1
+  have hznew : 0 ≤ newDefault s n K ρ z w := newDefault_nonneg
+  refine ⟨(le_min hfirst (by linarith)).trans h0.1, abs_le.mpr ⟨?_, ?_⟩⟩
+  · exact (le_min (abs_le.mp hsecond).1 (by linarith)).trans h1.1
+  · exact h1.2.trans (max_le (abs_le.mp hsecond).2 hη)
+
+/-- The new padded rank is at most the larger of `η` and the old padded rank. -/
+theorem reference_firstRank_le (hη : 0 ≤ η) (hρ : ρ ≤ η) (hK : 0 < K) (hKn : K ≤ n)
+    (hfirst : ∀ y ∈ s, -η ≤ w y 0) (hsecond : ∀ y ∈ s, |w y 1| ≤ η) :
+    firstRank s K (newDefault s n K ρ z w) (update s n K ρ z w) ≤
+      max η (firstRank s K z w) := by
+  let Q := max η (firstRank s K z w)
+  have hQ0 : 0 ≤ Q := hη.trans (le_max_left _ _)
+  have hb : newDefault s n K ρ z w ≤ Q :=
+    reference_newDefault_le hη hρ hK hKn hfirst hsecond
+  refine max_le hb ?_
+  by_contra h
+  have hcard := (lt_kthLargest_iff hK hQ0).mp (lt_of_not_ge h)
+  have hsub : ({y ∈ s | Q < update s n K ρ z w y 0} : Finset ι) ⊆
+      {y ∈ s | Q < w y 0} := by
+    intro y hy
+    obtain ⟨hys, hy⟩ := mem_filter.mp hy
+    refine mem_filter.mpr ⟨hys, ?_⟩
+    by_contra hfirstQ
+    have hu := (update_mem_Icc (s := s) (n := n) (K := K) (ρ := ρ) (z := z) (w := w) y 0).2
+    change update s n K ρ z w y 0 ≤ max (w y 0) (newDefault s n K ρ z w) at hu
+    exact (not_lt_of_ge (hu.trans (max_le (not_lt.mp hfirstQ) hb))) hy
+  have hfirstRank : Q < kthLargest K s (fun y => w y 0) :=
+    (lt_kthLargest_iff hK hQ0).mpr (hcard.trans (card_le_card hsub))
+  exact (not_lt_of_ge (kthLargest_le_firstRank.trans (le_max_right _ _))) hfirstRank
+
+/-- Above the flat rank region, the padded rank is preserved exactly. If the new default
+does not already equal the old rank, all old rank witnesses lie in the identity region. -/
+theorem reference_firstRank_eq (hη : 0 ≤ η) (hρ : ρ ≤ η) (hK : 0 < K) (hKn : K ≤ n)
+    (hfirst : ∀ y ∈ s, -η ≤ w y 0) (hsecond : ∀ y ∈ s, |w y 1| ≤ η)
+    (hq : η < firstRank s K z w) :
+    firstRank s K (newDefault s n K ρ z w) (update s n K ρ z w) = firstRank s K z w := by
+  have hu : threshold s n ρ z w ≤ firstRank s K z w := by
+    simpa only [max_eq_right hq.le] using
+      reference_threshold_le (z := z) hη hρ hK hKn hfirst hsecond
+  refine le_antisymm ?_ ?_
+  · simpa only [max_eq_right hq.le] using
+      reference_firstRank_le (z := z) hη hρ hK hKn hfirst hsecond
+  by_cases hqu : firstRank s K z w ≤ 3 * threshold s n ρ z w
+  · have hb : newDefault s n K ρ z w = firstRank s K z w := by
+      change max (threshold s n ρ z w) (min (firstRank s K z w) (3 * threshold s n ρ z w)) = _
+      rw [min_eq_left hqu, max_eq_right hu]
+    exact hb ▸ (default_le_firstRank (s := s) (K := K) (z := newDefault s n K ρ z w)
+      (w := update s n K ρ z w))
+  have h3u : 3 * threshold s n ρ z w < firstRank s K z w := lt_of_not_ge hqu
+  have hzq : z < firstRank s K z w := by
+    have hz : z ≤ threshold s n ρ z w := le_threshold
+    have hu0 : 0 ≤ threshold s n ρ z w := threshold_nonneg
+    linarith
+  have hqreal : firstRank s K z w ≤ kthLargest K s (fun y => w y 0) := by
+    have hmax := le_max_iff.mp
+      (show firstRank s K z w ≤ max z (kthLargest K s fun y => w y 0) from le_rfl)
+    exact hmax.resolve_left (not_le.mpr hzq)
+  have hq0 : 0 < firstRank s K z w := hη.trans_lt hq
+  have hcard := (le_kthLargest_iff hK hq0).mp hqreal
+  have hsub : ({y ∈ s | firstRank s K z w ≤ w y 0} : Finset ι) ⊆
+      {y ∈ s | firstRank s K z w ≤ update s n K ρ z w y 0} := by
+    intro y hy
+    obtain ⟨hys, hy⟩ := mem_filter.mp hy
+    refine mem_filter.mpr ⟨hys, ?_⟩
+    have hid : update s n K ρ z w y = w y :=
+      update_eq_self_of_three_mul_le
+        (h3u.le.trans ((hy.trans (le_abs_self _)).trans (abs_apply_le_entrySize (w y) 0)))
+    rw [hid]
+    exact hy
+  exact ((le_kthLargest_iff hK hq0).mpr (hcard.trans (card_le_card hsub))).trans
+    kthLargest_le_firstRank
+
+/-- Compression preserves any row output with a separated entry support and rank gate, and
+with no rank sensitivity in `[0,η]`. These are the structural hypotheses used in the
+stationary-reference part of [OpenAI2026LogSpace, Lemma 8.2]. -/
+theorem reference_update_output_eq {H : ℝ → ℝ → ℝ → ℝ} {g e : ℝ}
+    (hη : 0 ≤ η) (hρ : ρ ≤ η) (hK : 0 < K) (hKn : K ≤ n)
+    (hfirst : ∀ y ∈ s, -η ≤ w y 0) (hsecond : ∀ y ∈ s, |w y 1| ≤ η)
+    (hηg : η < g) (hge : 3 * g < e)
+    (hentry : ∀ x v r, x ≤ e → H x v r = 0)
+    (hgate : ∀ x v r, g ≤ r → H x v r = 0)
+    (hflat : ∀ x v q r, q ∈ Set.Icc 0 η → r ∈ Set.Icc 0 η → H x v q = H x v r)
+    (y : ι) (_hy : y ∈ s) :
+    H (update s n K ρ z w y 0) (update s n K ρ z w y 1)
+        (firstRank s K (newDefault s n K ρ z w) (update s n K ρ z w)) =
+      H (w y 0) (w y 1) (firstRank s K z w) := by
+  let q := firstRank s K z w
+  let q' := firstRank s K (newDefault s n K ρ z w) (update s n K ρ z w)
+  change H (update s n K ρ z w y 0) (update s n K ρ z w y 1) q' = H (w y 0) (w y 1) q
+  by_cases hclosed : g ≤ q
+  · have heq : q' = q :=
+      reference_firstRank_eq hη hρ hK hKn hfirst hsecond (hηg.trans_le hclosed)
+    rw [heq, hgate _ _ _ hclosed, hgate _ _ _ hclosed]
+  have hQg : max η q < g := max_lt hηg (lt_of_not_ge hclosed)
+  have hg0 : 0 < g := hη.trans_lt hηg
+  have hu : threshold s n ρ z w ≤ max η q :=
+    reference_threshold_le hη hρ hK hKn hfirst hsecond
+  have hb : newDefault s n K ρ z w ≤ max η q :=
+    reference_newDefault_le hη hρ hK hKn hfirst hsecond
+  have hb_e : newDefault s n K ρ z w ≤ e := by linarith
+  by_cases hsmall : w y 0 ≤ e
+  · have hcoord := (update_mem_Icc (s := s) (n := n) (K := K) (ρ := ρ) (z := z)
+      (w := w) y 0).2
+    change update s n K ρ z w y 0 ≤ max (w y 0) (newDefault s n K ρ z w) at hcoord
+    have hnew : update s n K ρ z w y 0 ≤ e := hcoord.trans (max_le hsmall hb_e)
+    rw [hentry _ _ _ hnew, hentry _ _ _ hsmall]
+  have h3u : 3 * threshold s n ρ z w < e := by linarith
+  have hid : update s n K ρ z w y = w y :=
+    update_eq_self_of_three_mul_le (h3u.le.trans ((lt_of_not_ge hsmall).le.trans
+      ((le_abs_self _).trans (abs_apply_le_entrySize (w y) 0))))
+  rw [hid]
+  by_cases hq : η < q
+  · have heq : q' = q := reference_firstRank_eq hη hρ hK hKn hfirst hsecond hq
+    rw [heq]
+  have hqη : q ≤ η := not_lt.mp hq
+  have hq'η : q' ≤ η := by
+    have h := reference_firstRank_le (z := z) hη hρ hK hKn hfirst hsecond
+    exact h.trans (max_le le_rfl hqη)
+  exact hflat _ _ _ _ ⟨firstRank_nonneg, hq'η⟩ ⟨firstRank_nonneg, hqη⟩
+
+section Iteration
+
+variable {n : ℕ → ℕ} {ρ : ℕ → ℝ} {a : State ι}
+
+/-- Zero-increment compression preserves the reference row's coordinate bounds at every
+stage. This uses only movement toward the nonnegative default, not rank preservation. -/
+theorem reference_iterate_bounds (hη : 0 ≤ η)
+    (hfirst : ∀ y ∈ s, -η ≤ a.row y 0) (hsecond : ∀ y ∈ s, |a.row y 1| ≤ η) (j : ℕ) :
+    (∀ y ∈ s, -η ≤ (iterate s n (fun _ => K) ρ (fun _ => 0) a j).row y 0) ∧
+      ∀ y ∈ s, |(iterate s n (fun _ => K) ρ (fun _ => 0) a j).row y 1| ≤ η := by
+  induction j with
+  | zero => exact ⟨hfirst, hsecond⟩
+  | succ j ih =>
+    have h (y : ι) (hy : y ∈ s) := reference_update_bounds (s := s) (n := n j) (K := K)
+      (ρ := ρ j) (z := (iterate s n (fun _ => K) ρ (fun _ => 0) a j).defaultValue)
+      hη (ih.1 y hy) (ih.2 y hy)
+    constructor
+    · intro y hy
+      simpa only [iterate_succ, advance, add_zero] using (h y hy).1
+    · intro y hy
+      simpa only [iterate_succ, advance, add_zero] using (h y hy).2
+
+/-- Stationary reference outputs survive any finite zero-increment compression schedule
+whose floors are at most `η` and whose capacities are at least the fixed rank `K`.
+Neither the row entries, the defaults, nor the chosen exception lists need remain fixed. -/
+theorem reference_iterate_output_eq {H : ℝ → ℝ → ℝ → ℝ} {g e : ℝ}
+    (hη : 0 ≤ η) (hK : 0 < K)
+    (hfirst : ∀ y ∈ s, -η ≤ a.row y 0) (hsecond : ∀ y ∈ s, |a.row y 1| ≤ η)
+    (hηg : η < g) (hge : 3 * g < e)
+    (hentry : ∀ x v r, x ≤ e → H x v r = 0)
+    (hgate : ∀ x v r, g ≤ r → H x v r = 0)
+    (hflat : ∀ x v q r, q ∈ Set.Icc 0 η → r ∈ Set.Icc 0 η → H x v q = H x v r)
+    (j : ℕ) (hn : ∀ i < j, K ≤ n i) (hρ : ∀ i < j, ρ i ≤ η) (y : ι) (hy : y ∈ s) :
+    H ((iterate s n (fun _ => K) ρ (fun _ => 0) a j).row y 0)
+        ((iterate s n (fun _ => K) ρ (fun _ => 0) a j).row y 1)
+        (firstRank s K (iterate s n (fun _ => K) ρ (fun _ => 0) a j).defaultValue
+          (iterate s n (fun _ => K) ρ (fun _ => 0) a j).row) =
+      H (a.row y 0) (a.row y 1) (firstRank s K a.defaultValue a.row) := by
+  induction j with
+  | zero => rfl
+  | succ j ih =>
+    have hb := reference_iterate_bounds (n := n) (K := K) (ρ := ρ) hη hfirst hsecond j
+    have hstep := reference_update_output_eq (n := n j) (K := K) (ρ := ρ j)
+      (z := (iterate s n (fun _ => K) ρ (fun _ => 0) a j).defaultValue)
+      (H := H) hη (hρ j (Nat.lt_succ_self j)) hK (hn j (Nat.lt_succ_self j))
+      hb.1 hb.2 hηg hge hentry hgate hflat y hy
+    have hprev := ih (fun i hi => hn i (Nat.lt_succ_of_lt hi))
+      (fun i hi => hρ i (Nat.lt_succ_of_lt hi))
+    simpa only [iterate_succ, advance, add_zero] using hstep.trans hprev
+
+end Iteration
+
+end Cslib.RowCompression
diff --git a/ComplexityTests/RowCompressionReference.lean b/ComplexityTests/RowCompressionReference.lean
new file mode 100644
index 000000000..bac8284bf
--- /dev/null
+++ b/ComplexityTests/RowCompressionReference.lean
@@ -0,0 +1,177 @@
+/-
+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.Reference
+import Mathlib.LinearAlgebra.Matrix.Notation
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+
+/-!
+# Stationary reference examples
+
+In the first example the padded rank is above the flat region and stays exactly `1/2`, while a
+zero row entry moves to the new default `3/8`. In the second example the padded rank itself
+moves from zero to `1/8`, inside the flat region. A nonzero gated output is preserved in both.
+-/
+
+namespace ComplexityTests.RowCompressionReference
+
+open Finset Cslib.RowCompression
+
+private theorem univ_three : (univ : Finset (Fin 3)) = {0, 1, 2} := by decide
+
+private noncomputable def highRow : Fin 3 → Fin 2 → ℝ := ![![10, 0], ![1 / 2, 0], ![0, 0]]
+
+private theorem high_rank : firstRank univ 2 0 highRow = 1 / 2 := by
+  have hle : kthLargest 2 univ (fun y => highRow y 0) ≤ 1 / 2 := by
+    refine not_lt.mp fun hlt => ?_
+    have hcard := (lt_kthLargest_iff (by norm_num)
+      (by norm_num : (0 : ℝ) ≤ 1 / 2)).mp hlt
+    have hsupport : ({y | (1 / 2 : ℝ) < highRow y 0} : Finset (Fin 3)) = {0} := by
+      ext y
+      fin_cases y <;> norm_num [highRow]
+    rw [hsupport] at hcard
+    norm_num at hcard
+  have hge : (1 / 2 : ℝ) ≤ kthLargest 2 univ (fun y => highRow y 0) := by
+    apply (le_kthLargest_iff (by norm_num) (by norm_num : (0 : ℝ) < 1 / 2)).mpr
+    have hsupport : ({y | (1 / 2 : ℝ) ≤ highRow y 0} : Finset (Fin 3)) = {0, 1} := by
+      ext y
+      fin_cases y <;> norm_num [highRow]
+    rw [hsupport]
+    norm_num
+  unfold firstRank
+  rw [le_antisymm hle hge]
+  norm_num
+
+private theorem high_threshold : threshold univ 3 (1 / 8) 0 highRow = 1 / 8 := by
+  have hr : kthLargest 3 univ (fun y => entrySize (highRow y)) = 0 := by
+    refine le_antisymm (not_lt.mp fun hlt => ?_) kthLargest_nonneg
+    have hcard := (lt_kthLargest_iff (by norm_num) le_rfl).mp hlt
+    have hsupport : ({y | 0 < entrySize (highRow y)} : Finset (Fin 3)) = {0, 1} := by
+      ext y
+      fin_cases y <;> norm_num [entrySize, highRow]
+    rw [hsupport] at hcard
+    norm_num at hcard
+  norm_num [threshold, hr]
+
+private theorem high_default : newDefault univ 3 2 (1 / 8) 0 highRow = 3 / 8 := by
+  change max (threshold univ 3 (1 / 8) 0 highRow)
+    (min (firstRank univ 2 0 highRow) (3 * threshold univ 3 (1 / 8) 0 highRow)) = _
+  rw [high_threshold, high_rank]
+  norm_num
+
+private theorem high_update : update univ 3 2 (1 / 8) 0 highRow =
+    ![![10, 0], ![1 / 2, 0], ![3 / 8, 0]] := by
+  unfold update
+  rw [high_threshold, high_default]
+  funext y ν
+  fin_cases y <;> fin_cases ν <;>
+    norm_num [updateEntry, radius, entrySize, defaultEntry, highRow]
+
+private theorem high_first (y : Fin 3) (_hy : y ∈ (univ : Finset (Fin 3))) :
+    -(1 / 4 : ℝ) ≤ highRow y 0 := by
+  fin_cases y <;> norm_num [highRow]
+
+private theorem high_second (y : Fin 3) (_hy : y ∈ (univ : Finset (Fin 3))) :
+    |highRow y 1| ≤ (1 / 4 : ℝ) := by
+  fin_cases y <;> norm_num [highRow]
+
+-- The rank theorem applies to a row whose default and some actual entries really move.
+example : firstRank univ 2 (newDefault univ 3 2 (1 / 8) 0 highRow)
+    (update univ 3 2 (1 / 8) 0 highRow) = 1 / 2 := by
+  have h := reference_firstRank_eq (η := 1 / 4) (by norm_num) (by norm_num : (1 / 8 : ℝ) ≤ 1 / 4)
+    (by norm_num : 0 < (2 : ℕ)) (by norm_num : (2 : ℕ) ≤ 3) high_first high_second
+    (by rw [high_rank]; norm_num)
+  exact h.trans high_rank
+
+example : update univ 3 2 (1 / 8) 0 highRow 2 0 ≠ highRow 2 0 := by
+  rw [high_update]
+  norm_num [highRow]
+
+private noncomputable def rowOutput (x v r : ℝ) : ℝ :=
+  if x ≤ 4 then 0 else if 1 ≤ r then 0 else x + v + max (1 / 4) r
+
+private theorem output_entry (x v r : ℝ) (hx : x ≤ 4) : rowOutput x v r = 0 := by
+  simp [rowOutput, hx]
+
+private theorem output_gate (x v r : ℝ) (hr : 1 ≤ r) : rowOutput x v r = 0 := by
+  simp [rowOutput, hr]
+
+private theorem output_flat (x v q r : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4 : ℝ))
+    (hr : r ∈ Set.Icc 0 (1 / 4 : ℝ)) : rowOutput x v q = rowOutput x v r := by
+  have hq' : ¬1 ≤ q := by linarith [hq.2]
+  have hr' : ¬1 ≤ r := by linarith [hr.2]
+  simp only [rowOutput, hq', hr', ↓reduceIte, max_eq_left hq.2, max_eq_left hr.2]
+
+private noncomputable def initial : State (Fin 3) := { defaultValue := 0, row := highRow }
+
+-- An arbitrary number of zero-increment updates preserves the nonzero output 10.5.
+example (j : ℕ) :
+    let a := iterate univ (fun _ => 3) (fun _ => 2) (fun _ => 1 / 8) (fun _ => 0) initial j
+    rowOutput (a.row 0 0) (a.row 0 1) (firstRank univ 2 a.defaultValue a.row) = 21 / 2 := by
+  have h := reference_iterate_output_eq (s := univ) (n := fun _ => 3) (K := 2)
+    (ρ := fun _ => 1 / 8) (a := initial) (η := 1 / 4) (H := rowOutput) (g := 1) (e := 4)
+    (by norm_num) (by norm_num) high_first high_second (by norm_num) (by norm_num)
+    output_entry output_gate output_flat j (by intros; norm_num) (by intros; norm_num) 0
+    (mem_univ 0)
+  refine h.trans ?_
+  change rowOutput 10 0 (firstRank univ 2 0 highRow) = 21 / 2
+  rw [high_rank]
+  norm_num [rowOutput]
+
+private def lowRow : Fin 3 → Fin 2 → ℝ := ![![10, 0], ![0, 0], ![0, 0]]
+
+private theorem low_rank : firstRank univ 2 0 lowRow = 0 := by
+  norm_num [firstRank, kthLargest, lowRow, univ_three, filter_insert, filter_image,
+    filter_singleton]
+
+private theorem low_threshold : threshold univ 3 (1 / 8) 0 lowRow = 1 / 8 := by
+  norm_num [threshold, kthLargest, lowRow, entrySize, univ_three, filter_insert,
+    filter_image, filter_singleton]
+
+private theorem low_default : newDefault univ 3 2 (1 / 8) 0 lowRow = 1 / 8 := by
+  change max (threshold univ 3 (1 / 8) 0 lowRow)
+    (min (firstRank univ 2 0 lowRow) (3 * threshold univ 3 (1 / 8) 0 lowRow)) = _
+  rw [low_threshold, low_rank]
+  norm_num
+
+private theorem low_update : update univ 3 2 (1 / 8) 0 lowRow =
+    ![![10, 0], ![1 / 8, 0], ![1 / 8, 0]] := by
+  unfold update
+  rw [low_threshold, low_default]
+  funext y ν
+  fin_cases y <;> fin_cases ν <;>
+    norm_num [updateEntry, radius, entrySize, defaultEntry, lowRow]
+
+-- A low padded rank may change; the theorem requires only flat output dependence there.
+example : firstRank univ 2 (newDefault univ 3 2 (1 / 8) 0 lowRow)
+    (update univ 3 2 (1 / 8) 0 lowRow) = 1 / 8 ∧ firstRank univ 2 0 lowRow = 0 := by
+  refine ⟨le_antisymm ?_ ?_, low_rank⟩
+  · have h := reference_firstRank_le (s := univ) (n := 3) (K := 2) (ρ := 1 / 8) (z := 0)
+      (w := lowRow) (η := 1 / 8) (by norm_num) le_rfl (by norm_num) (by norm_num)
+      (fun y _ => by fin_cases y <;> norm_num [lowRow])
+      (fun y _ => by fin_cases y <;> norm_num [lowRow])
+    simpa only [low_rank, max_eq_left (by norm_num : (0 : ℝ) ≤ 1 / 8)] using h
+  · have h := default_le_firstRank (s := univ) (K := 2)
+      (z := newDefault univ 3 2 (1 / 8) 0 lowRow) (w := update univ 3 2 (1 / 8) 0 lowRow)
+    simpa only [low_default] using h
+
+example : rowOutput (update univ 3 2 (1 / 8) 0 lowRow 0 0)
+    (update univ 3 2 (1 / 8) 0 lowRow 0 1)
+    (firstRank univ 2 (newDefault univ 3 2 (1 / 8) 0 lowRow)
+      (update univ 3 2 (1 / 8) 0 lowRow)) = 41 / 4 := by
+  have h := reference_update_output_eq (s := univ) (n := 3) (K := 2) (ρ := 1 / 8) (z := 0)
+    (w := lowRow) (η := 1 / 4) (H := rowOutput) (g := 1) (e := 4)
+    (by norm_num) (by norm_num) (by norm_num) (by norm_num)
+    (fun y _ => by fin_cases y <;> norm_num [lowRow])
+    (fun y _ => by fin_cases y <;> norm_num [lowRow])
+    (by norm_num) (by norm_num) output_entry output_gate output_flat 0 (mem_univ 0)
+  refine h.trans ?_
+  rw [low_rank]
+  norm_num [rowOutput, lowRow]
+
+end ComplexityTests.RowCompressionReference