diff --git a/Complexity.lean b/Complexity.lean
index f06264477..ec90a008b 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2462,10 +2462,12 @@ public import Complexity.Foundations.Analysis.RowCompression.Floors
 public import Complexity.Foundations.Analysis.RowCompression.Iteration
 public import Complexity.Foundations.Analysis.RowCompression.OverflowBudget
 public import Complexity.Foundations.Analysis.RowCompression.OverflowNoise
+public import Complexity.Foundations.Analysis.RowCompression.Perturbation
 public import Complexity.Foundations.Analysis.RowCompression.Preloss
 public import Complexity.Foundations.Analysis.RowCompression.Reference
 public import Complexity.Foundations.Analysis.RowCompression.Sentinel
 public import Complexity.Foundations.Analysis.RowCompression.SentinelIteration
+public import Complexity.Foundations.Analysis.RowCompression.SentinelRelative
 public import Complexity.Foundations.Analysis.RowCompression.Stationary
 public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos
 public import Complexity.Foundations.Analysis.SpecialFunctions.PolynomialSwitch
diff --git a/Complexity/Foundations/Analysis/RowCompression/Perturbation.lean b/Complexity/Foundations/Analysis/RowCompression/Perturbation.lean
new file mode 100644
index 000000000..7536d0b75
--- /dev/null
+++ b/Complexity/Foundations/Analysis/RowCompression/Perturbation.lean
@@ -0,0 +1,168 @@
+/-
+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.Reference
+import Mathlib.Algebra.BigOperators.Ring.Finset
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
+
+/-!
+# Perturbations of compression schedules
+
+The concrete compression update has Lipschitz constant `28`. Comparing schedules with different
+increments gives an initial-error term `28 ^ m * δ` and a sum of increment-error terms
+`28 ^ (m - i) * ε i`. Both defaults and all retained coordinates satisfy the same bound.
+
+A zero-increment reference with the usual small negative and second-coordinate bounds preserves
+an initial padded-rank ceiling above the floor scale. Its actual thresholds satisfy that ceiling
+as well. These estimates are the absolute-error ingredients of the sentinel comparison in
+[OpenAI2026LogSpace, Section 8.3, Lemma 8.3]. They do not by themselves convert relative errors
+at unbounded first coordinates to absolute errors or prove the final row-output comparison.
+
+## Main results
+
+* `Cslib.RowCompression.iterate_stability_of_increment_error`: weighted stability for two actual
+  schedules with different increments.
+* `Cslib.RowCompression.reference_iterate_firstRank_le`: a uniform padded-rank ceiling for
+  zero-increment references.
+* `Cslib.RowCompression.reference_stepThreshold_le`: the corresponding actual threshold bound.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 8.3, proof of Lemma 8.3, the absolute comparison after sentinel replacement
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+namespace Cslib.RowCompression
+
+open Finset
+
+variable {ι : Type*} {s : Finset ι} {a b : State ι}
+
+/-- One update with an increment discrepancy adds that discrepancy before the factor `28`.
+The initial defaults and both full rows may already differ. -/
+theorem advance_stability_of_increment_error {n K : ℕ} {ρ δ ε : ℝ}
+    {Δ Δ' : ι → Fin 2 → ℝ} (hn : 0 < n) (hK : 0 < K) (hδ : 0 ≤ δ) (hε : 0 ≤ ε)
+    (hz : |a.defaultValue - b.defaultValue| ≤ δ)
+    (hw : ∀ y ∈ s, ∀ ν, |a.row y ν - b.row y ν| ≤ δ)
+    (hΔ : ∀ y ∈ s, ∀ ν, |Δ y ν - Δ' y ν| ≤ ε) :
+    |(advance s n K ρ Δ a).defaultValue - (advance s n K ρ Δ' b).defaultValue| ≤
+        28 * (δ + ε) ∧
+      ∀ y ∈ s, ∀ ν,
+        |(advance s n K ρ Δ a).row y ν - (advance s n K ρ Δ' b).row y ν| ≤
+          28 * (δ + ε) := by
+  have hinput (y : ι) (hy : y ∈ s) (ν : Fin 2) :
+      |(a.row + Δ) y ν - (b.row + Δ') y ν| ≤ δ + ε := by
+    calc
+      _ = |(a.row y ν - b.row y ν) + (Δ y ν - Δ' y ν)| := by
+        congr 1
+        simp only [Pi.add_apply]
+        ring
+      _ ≤ |a.row y ν - b.row y ν| + |Δ y ν - Δ' y ν| := abs_add_le _ _
+      _ ≤ δ + ε := add_le_add (hw y hy ν) (hΔ y hy ν)
+  have hz' : |a.defaultValue - b.defaultValue| ≤ δ + ε := hz.trans (le_add_of_nonneg_right hε)
+  constructor
+  · exact (abs_newDefault_sub_newDefault_le hn hK (add_nonneg hδ hε) hz' hinput).trans
+      (by nlinarith)
+  · intro y hy ν
+    exact abs_update_sub_update_le hn hK (add_nonneg hδ hε) hz' hinput hy ν
+
+private theorem propagation_succ (δ : ℝ) (ε : ℕ → ℝ) (j : ℕ) :
+    28 * (28 ^ j * δ + ∑ i ∈ range j, 28 ^ (j - i) * ε i + ε j) =
+      28 ^ (j + 1) * δ + ∑ i ∈ range (j + 1), 28 ^ (j + 1 - i) * ε i := by
+  have hsum : (∑ i ∈ range j, (28 : ℝ) ^ (j + 1 - i) * ε i) =
+      28 * ∑ i ∈ range j, (28 : ℝ) ^ (j - i) * ε i := by
+    rw [mul_sum]
+    apply sum_congr rfl
+    intro i hi
+    have hexp : j + 1 - i = (j - i) + 1 := by
+      have hi' := mem_range.mp hi
+      omega
+    rw [hexp, pow_succ]
+    ring
+  rw [sum_range_succ, hsum]
+  simp only [Nat.add_sub_cancel_left, pow_succ]
+  ring
+
+/-- Different increments contribute at the group where they are actually added, with one
+factor `28` for that update and for each subsequent update. No threshold ceiling is assumed. -/
+theorem iterate_stability_of_increment_error {n K : ℕ → ℕ} {ρ : ℕ → ℝ}
+    {Δ Δ' : ℕ → ι → Fin 2 → ℝ} {δ : ℝ} {ε : ℕ → ℝ}
+    (hδ : 0 ≤ δ) (hz : |a.defaultValue - b.defaultValue| ≤ δ)
+    (hw : ∀ y ∈ s, ∀ ν, |a.row y ν - b.row y ν| ≤ δ) (m : ℕ)
+    (hn : ∀ i < m, 0 < n i) (hK : ∀ i < m, 0 < K i)
+    (hε : ∀ i < m, 0 ≤ ε i)
+    (hΔ : ∀ i < m, ∀ y ∈ s, ∀ ν, |Δ i y ν - Δ' i y ν| ≤ ε i) :
+    |(iterate s n K ρ Δ a m).defaultValue - (iterate s n K ρ Δ' b m).defaultValue| ≤
+        28 ^ m * δ + ∑ i ∈ range m, 28 ^ (m - i) * ε i ∧
+      ∀ y ∈ s, ∀ ν,
+        |(iterate s n K ρ Δ a m).row y ν - (iterate s n K ρ Δ' b m).row y ν| ≤
+          28 ^ m * δ + ∑ i ∈ range m, 28 ^ (m - i) * ε i := by
+  induction m with
+  | zero => simpa using And.intro hz hw
+  | succ m ih =>
+    have ih' := ih (fun i hi => hn i (Nat.lt_succ_of_lt hi))
+      (fun i hi => hK i (Nat.lt_succ_of_lt hi))
+      (fun i hi => hε i (Nat.lt_succ_of_lt hi))
+      (fun i hi => hΔ i (Nat.lt_succ_of_lt hi))
+    have hbudget : 0 ≤ 28 ^ m * δ + ∑ i ∈ range m, 28 ^ (m - i) * ε i := by
+      exact add_nonneg (mul_nonneg (by positivity) hδ)
+        (sum_nonneg fun i hi => mul_nonneg (by positivity)
+          (hε i (Nat.lt_succ_of_lt (mem_range.mp hi))))
+    have h := advance_stability_of_increment_error (ρ := ρ m)
+      (hn m (Nat.lt_succ_self m)) (hK m (Nat.lt_succ_self m)) hbudget
+      (hε m (Nat.lt_succ_self m)) ih'.1 ih'.2 (hΔ m (Nat.lt_succ_self m))
+    simpa only [iterate_succ, propagation_succ] using h
+
+section Reference
+
+variable {n : ℕ → ℕ} {K : ℕ} {ρ : ℕ → ℝ} {η Q : ℝ}
+
+/-- A stationary reference's padded first rank stays below any initial ceiling above the
+reference scale. The hypotheses are only on its initial row and the finite schedule. -/
+theorem reference_iterate_firstRank_le (hη : 0 ≤ η) (hηQ : η ≤ Q) (hK : 0 < K)
+    (hfirst : ∀ y ∈ s, -η ≤ a.row y 0) (hsecond : ∀ y ∈ s, |a.row y 1| ≤ η)
+    (hq : firstRank s K a.defaultValue a.row ≤ Q) (m : ℕ)
+    (hn : ∀ i < m, K ≤ n i) (hρ : ∀ i < m, ρ i ≤ η) :
+    firstRank s K (iterate s n (fun _ => K) ρ (fun _ => 0) a m).defaultValue
+      (iterate s n (fun _ => K) ρ (fun _ => 0) a m).row ≤ Q := by
+  induction m with
+  | zero => exact hq
+  | succ m ih =>
+    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))
+    have hb := reference_iterate_bounds (n := n) (K := K) (ρ := ρ) hη hfirst hsecond m
+    have hnext := reference_firstRank_le
+      (z := (iterate s n (fun _ => K) ρ (fun _ => 0) a m).defaultValue)
+      hη (hρ m (Nat.lt_succ_self m)) hK
+      (hn m (Nat.lt_succ_self m)) hb.1 hb.2
+    simpa only [iterate_succ, advance, add_zero] using hnext.trans (max_le hηQ hprev)
+
+/-- The same initial reference ceiling controls every actual input threshold. -/
+theorem reference_stepThreshold_le (hη : 0 ≤ η) (hηQ : η ≤ Q) (hK : 0 < K)
+    (hfirst : ∀ y ∈ s, -η ≤ a.row y 0) (hsecond : ∀ y ∈ s, |a.row y 1| ≤ η)
+    (hq : firstRank s K a.defaultValue a.row ≤ Q) (m : ℕ)
+    (hn : ∀ i ≤ m, K ≤ n i) (hρ : ∀ i ≤ m, ρ i ≤ η) :
+    stepThreshold s n (fun _ => K) ρ (fun _ => 0) a m ≤ Q := by
+  have hb := reference_iterate_bounds (n := n) (K := K) (ρ := ρ) hη hfirst hsecond m
+  have hr := reference_iterate_firstRank_le hη hηQ hK hfirst hsecond hq m
+    (fun i hi => hn i hi.le) (fun i hi => hρ i hi.le)
+  have ht := reference_threshold_le
+    (z := (iterate s n (fun _ => K) ρ (fun _ => 0) a m).defaultValue)
+    hη (hρ m le_rfl) hK (hn m le_rfl) hb.1 hb.2
+  simpa only [stepThreshold, inputRow, add_zero] using ht.trans (max_le hηQ hr)
+
+end Reference
+
+end Cslib.RowCompression
diff --git a/Complexity/Foundations/Analysis/RowCompression/SentinelRelative.lean b/Complexity/Foundations/Analysis/RowCompression/SentinelRelative.lean
new file mode 100644
index 000000000..e7d429322
--- /dev/null
+++ b/Complexity/Foundations/Analysis/RowCompression/SentinelRelative.lean
@@ -0,0 +1,409 @@
+/-
+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.Perturbation
+public import Complexity.Foundations.Analysis.RowCompression.Preloss
+public import Complexity.Foundations.Analysis.RowCompression.SentinelIteration
+import Mathlib.Algebra.BigOperators.Ring.Finset
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Algebra.Order.Group.MinMax
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
+
+/-!
+# Deriving sentinel comparison bounds from clipped prefix errors
+
+Suppose fewer than `K` true first entries exceed `L₀`, and the actual raw prefixes have small
+clipped errors. Replace first entries above `16 * (L₀ + 1)` by that common sentinel and clear
+only their later first increments. The modified calculation has bounded actual input ranks and
+thresholds, and the original marked entries remain in the compression identity region.
+
+The ceilings and the total-variation hypothesis of
+`Cslib.RowCompression.iterate_sentinelState_of_sum_abs_lt` are derived here, rather than assumed.
+The comparison reference has the true row plus the same small initial loss and no increments.
+The finite error budget is the exact `28`-weighted sum supplied by absolute update stability.
+No upper bound on the largest true entry, original compressed input, or final output error is
+assumed.
+
+For a first-overflow application, start the local calculation from the already-added input of
+that group, use a zero first local increment, and then use the subsequent actual increments.
+Both the initial and first local prefix errors then concern the overflow group's raw input.
+This does not require an error estimate for the preceding global prefix.
+
+This supplies the small-heavy-set sentinel comparison in the proof of
+[OpenAI2026LogSpace, Section 8.3, Lemma 8.3]. Upper saturation and the row-output comparison,
+the case of at least `K` large true entries, and the full relative-stability estimate remain
+separate. Sentinels are analytical devices, not objects stored by the compression algorithm.
+
+## Main results
+
+* `Cslib.RowCompression.abs_sub_le_of_clippedError_le`: small clipped errors give the actual
+  relative first-channel and absolute second-channel bounds.
+* `Cslib.RowCompression.iterate_sentinelState_of_clippedError_le`: actual sentinel coupling
+  from clipped prefix budgets and a strict true-heavy-count bound.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 8.3, proof of Lemma 8.3, the branch with fewer than `K` entries above `L₀`
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+namespace Cslib.RowCompression
+
+open Finset
+
+/-- Below one, clipping discards no information. The first target may be arbitrarily large. -/
+theorem abs_sub_le_of_clippedError_le {d v ε : ℝ} {w : Fin 2 → ℝ}
+    (hd : 0 ≤ d) (hε : ε < 1) (he : clippedError d v w ≤ ε) :
+    |w 0 - d| ≤ (1 + d) * ε ∧ |w 1 - v| ≤ ε := by
+  have hfirst : |w 0 - d| / (1 + d) ≤ ε :=
+    (min_le_iff.mp ((le_max_left _ _).trans he)).resolve_left (not_le.mpr hε)
+  have hsecond : |w 1 - v| ≤ ε :=
+    (min_le_iff.mp ((le_max_right _ _).trans he)).resolve_left (not_le.mpr hε)
+  refine ⟨?_, hsecond⟩
+  simpa only [mul_comm] using (div_le_iff₀ (by linarith : 0 < 1 + d)).mp hfirst
+
+private def budget (ε : ℕ → ℝ) (m : ℕ) : ℝ :=
+  28 ^ m * ε 0 + ∑ i ∈ range m, 28 ^ (m - i) * (ε i + ε (i + 1))
+
+private theorem budget_nonneg {ε : ℕ → ℝ} {m : ℕ} (hε : ∀ i ≤ m, 0 ≤ ε i) :
+    0 ≤ budget ε m := by
+  apply add_nonneg (mul_nonneg (by positivity) (hε 0 (Nat.zero_le m)))
+  refine sum_nonneg fun i hi => mul_nonneg (by positivity) (add_nonneg ?_ ?_)
+  · exact hε i (mem_range.mp hi).le
+  · exact hε (i + 1) (mem_range.mp hi)
+
+private theorem budget_mono {ε : ℕ → ℝ} {j m : ℕ}
+    (hε : ∀ i ≤ m, 0 ≤ ε i) (hj : j ≤ m) : budget ε j ≤ budget ε m := by
+  apply add_le_add
+  · exact mul_le_mul_of_nonneg_right (pow_le_pow_right₀ (by norm_num) hj)
+      (hε 0 (Nat.zero_le m))
+  calc
+    _ ≤ ∑ i ∈ range j, (28 : ℝ) ^ (m - i) * (ε i + ε (i + 1)) := by
+      refine sum_le_sum fun i hi => mul_le_mul_of_nonneg_right
+        (pow_le_pow_right₀ (by norm_num) (Nat.sub_le_sub_right hj i)) ?_
+      exact add_nonneg (hε i ((mem_range.mp hi).le.trans hj))
+        (hε (i + 1) ((mem_range.mp hi).trans_le hj))
+    _ ≤ _ := sum_le_sum_of_subset_of_nonneg (range_mono hj) fun i hi _ =>
+      mul_nonneg (by positivity)
+        (add_nonneg (hε i (mem_range.mp hi).le) (hε (i + 1) (mem_range.mp hi)))
+
+private theorem sum_errors_le_budget {ε : ℕ → ℝ} {m : ℕ}
+    (hε : ∀ i ≤ m, 0 ≤ ε i) :
+    ε 0 + ∑ i ∈ range m, (ε i + ε (i + 1)) ≤ budget ε m := by
+  apply add_le_add
+  · exact le_mul_of_one_le_left (hε 0 (Nat.zero_le m)) (one_le_pow₀ (by norm_num))
+  · exact sum_le_sum fun i hi => le_mul_of_one_le_left
+      (add_nonneg (hε i (mem_range.mp hi).le) (hε (i + 1) (mem_range.mp hi)))
+      (one_le_pow₀ (by norm_num))
+
+private theorem error_le_budget {ε : ℕ → ℝ} {m i : ℕ}
+    (hε : ∀ i ≤ m, 0 ≤ ε i) (hi : i ≤ m) : ε i ≤ budget ε m := by
+  have hsum := sum_errors_le_budget hε
+  have hs0 : 0 ≤ ∑ k ∈ range m, (ε k + ε (k + 1)) :=
+    sum_nonneg fun k hk => add_nonneg (hε k (mem_range.mp hk).le)
+      (hε (k + 1) (mem_range.mp hk))
+  cases i with
+  | zero => exact (le_add_of_nonneg_right hs0).trans hsum
+  | succ i =>
+    have hsingle := single_le_sum (s := range m) (f := fun k => ε k + ε (k + 1))
+      (fun k hk => add_nonneg (hε k (mem_range.mp hk).le) (hε (k + 1) (mem_range.mp hk)))
+      (mem_range.mpr hi)
+    have hi0 := hε i (Nat.le_of_lt hi)
+    have h00 := hε 0 (Nat.zero_le m)
+    linarith
+
+private theorem input_budget_le {ε : ℕ → ℝ} {m i : ℕ}
+    (hε : ∀ k ≤ m, 0 ≤ ε k) (hi : i < m) :
+    budget ε i + (ε i + ε (i + 1)) ≤ budget ε m := by
+  apply le_trans (b := budget ε (i + 1)) _ (budget_mono hε hi)
+  unfold budget
+  rw [sum_range_succ]
+  simp only [Nat.add_sub_cancel_left, pow_one]
+  conv_rhs => rw [← add_assoc]
+  apply add_le_add
+  · apply add_le_add
+    · exact mul_le_mul_of_nonneg_right
+        (pow_le_pow_right₀ (by norm_num) (Nat.le_succ i)) (hε 0 (Nat.zero_le m))
+    · refine sum_le_sum fun k hk => mul_le_mul_of_nonneg_right
+        (pow_le_pow_right₀ (by norm_num) (Nat.sub_le_sub_right (Nat.le_succ i) k)) ?_
+      exact add_nonneg (hε k ((mem_range.mp hk).le.trans hi.le))
+        (hε (k + 1) ((mem_range.mp hk).trans_le hi.le))
+  · exact le_mul_of_one_le_left (add_nonneg (hε i hi.le) (hε (i + 1) hi)) (by norm_num)
+
+variable {ι : Type*}
+
+private theorem sentinel_reference_bounds {s : Finset ι} {K : ℕ} {η L₀ z : ℝ}
+    {truth loss : ι → Fin 2 → ℝ} (hη : 0 ≤ η) (hL₀ : η ≤ L₀) (hK : 0 < K) (hz : z ≤ η)
+    (hfirst : ∀ y ∈ s, 0 ≤ truth y 0) (hsecond : ∀ y ∈ s, |truth y 1| ≤ η / 2)
+    (hloss : ∀ y ∈ s, ∀ ν, |loss y ν| ≤ η / 2)
+    (hcount : #{y ∈ s | L₀ < truth y 0} < K) :
+    let marked := {y ∈ s | 16 * (L₀ + 1) < truth y 0}
+    let b := sentinelState marked (16 * (L₀ + 1)) ⟨z, truth + loss⟩
+    (∀ y ∈ s, -η ≤ b.row y 0) ∧ (∀ y ∈ s, |b.row y 1| ≤ η) ∧
+      firstRank s K b.defaultValue b.row ≤ 2 * L₀ := by
+  classical
+  let marked := {y ∈ s | 16 * (L₀ + 1) < truth y 0}
+  let b := sentinelState marked (16 * (L₀ + 1)) ⟨z, truth + loss⟩
+  change (∀ y ∈ s, -η ≤ b.row y 0) ∧ (∀ y ∈ s, |b.row y 1| ≤ η) ∧
+    firstRank s K b.defaultValue b.row ≤ 2 * L₀
+  have hL₀0 : 0 ≤ L₀ := hη.trans hL₀
+  have hshape : (∀ y ∈ s, -η ≤ b.row y 0) ∧ (∀ y ∈ s, |b.row y 1| ≤ η) := by
+    constructor
+    · intro y hy
+      by_cases hm : y ∈ marked
+      · change -η ≤ sentinelFirst marked (16 * (L₀ + 1)) (truth + loss) y 0
+        rw [sentinelFirst_zero_of_mem hm]
+        linarith
+      · change -η ≤ sentinelFirst marked (16 * (L₀ + 1)) (truth + loss) y 0
+        rw [sentinelFirst_of_not_mem hm]
+        have hl := (abs_le.mp (hloss y hy 0)).1
+        change -η ≤ truth y 0 + loss y 0
+        linarith [hfirst y hy]
+    · intro y hy
+      change |sentinelFirst marked (16 * (L₀ + 1)) (truth + loss) y 1| ≤ η
+      rw [sentinelFirst_one]
+      exact (abs_add_le _ _).trans (by linarith [hsecond y hy, hloss y hy 1])
+  refine ⟨hshape.1, hshape.2, max_le (by change z ≤ 2 * L₀; linarith) ?_⟩
+  by_contra hq
+  have hcard := (lt_kthLargest_iff hK (by positivity : 0 ≤ 2 * L₀)).mp (lt_of_not_ge hq)
+  have hsub : ({y ∈ s | 2 * L₀ < b.row y 0} : Finset ι) ⊆
+      {y ∈ s | L₀ < truth y 0} := by
+    intro y hy
+    obtain ⟨hys, hy⟩ := mem_filter.mp hy
+    refine mem_filter.mpr ⟨hys, ?_⟩
+    by_cases hm : y ∈ marked
+    · have hlarge := (mem_filter.mp hm).2
+      linarith
+    · change 2 * L₀ < sentinelFirst marked (16 * (L₀ + 1)) (truth + loss) y 0 at hy
+      rw [sentinelFirst_of_not_mem hm] at hy
+      have hl := (abs_le.mp (hloss y hys 0)).2
+      change 2 * L₀ < truth y 0 + loss y 0 at hy
+      linarith
+  exact (not_le.mpr hcount) (hcard.trans (card_le_card hsub))
+
+open Classical in
+/-- **Sentinel coupling from actual clipped-prefix budgets.** The threshold and variation
+conditions of the removal induction follow from the true heavy-count branch and the weighted
+prefix budget. `loss` is the common initial preloss; it is not a final-error hypothesis.
+
+Only marked first increments are cleared. Both original marked channels follow their actual
+raw prefixes, and all positive-prefix padded ranks agree exactly. -/
+theorem iterate_sentinelState_of_clippedError_le {s : Finset ι} {n : ℕ → ℕ} {K : ℕ}
+    {ρ : ℕ → ℝ} {η L₀ z : ℝ} {truth raw₀ loss : ι → Fin 2 → ℝ}
+    {Δ : ℕ → ι → Fin 2 → ℝ} {ε : ℕ → ℝ} (m : ℕ)
+    (hη : 0 ≤ η) (hL₀ : η ≤ L₀) (hzη : z ≤ η) (hK : 0 < K)
+    (hKn : ∀ i < m, K ≤ n i) (hρ : ∀ i < m, ρ i ≤ η)
+    (hfirst : ∀ y ∈ s, 0 ≤ truth y 0) (hsecond : ∀ y ∈ s, |truth y 1| ≤ η / 2)
+    (hloss : ∀ y ∈ s, ∀ ν, |loss y ν| ≤ η / 2)
+    (hcount : #{y ∈ s | L₀ < truth y 0} < K)
+    (hε : ∀ i ≤ m, 0 ≤ ε i)
+    (herr : ∀ i ≤ m, ∀ y ∈ s,
+      clippedError (truth y 0) (truth y 1) (uncompressedRow Δ raw₀ i y) ≤ ε i)
+    (hsmall : (1 + 16 * (L₀ + 1)) *
+      (28 ^ m * ε 0 + ∑ i ∈ range m, 28 ^ (m - i) * (ε i + ε (i + 1))) ≤ 1 / 8) :
+    let L := 16 * (L₀ + 1)
+    let R := 2 * L₀ + 1
+    let marked := {y ∈ s | L < truth y 0}
+    let a : State ι := ⟨z, raw₀ + loss⟩
+    let original := iterate s n (fun _ => K) ρ Δ a
+    let modified := iterate s n (fun _ => K) ρ
+      (fun i => sentinelFirst marked 0 (Δ i)) (sentinelState marked L a)
+    ∀ j ≤ m, modified j = sentinelState marked L (original j) ∧
+      (∀ y ∈ marked, (original j).row y = uncompressedRow Δ a.row j y) ∧
+      (0 < j → firstRank s K (original j).defaultValue (original j).row =
+        firstRank s K (modified j).defaultValue (modified j).row ∧
+          firstRank s K (modified j).defaultValue (modified j).row ≤ R) := by
+  classical
+  let L := 16 * (L₀ + 1)
+  let R := 2 * L₀ + 1
+  let c := 1 + L
+  let marked := {y ∈ s | L < truth y 0}
+  let a : State ι := ⟨z, raw₀ + loss⟩
+  let b : State ι := ⟨z, truth + loss⟩
+  let a' := sentinelState marked L a
+  let b' := sentinelState marked L b
+  let Δ' := fun i => sentinelFirst marked 0 (Δ i)
+  let A := iterate s n (fun _ => K) ρ Δ' a'
+  let B := iterate s n (fun _ => K) ρ (fun _ => 0) b'
+  have hL₀0 : 0 ≤ L₀ := hη.trans hL₀
+  have hc1 : 1 ≤ c := by dsimp only [c, L]; linarith
+  have hc0 : 0 ≤ c := (by norm_num : (0 : ℝ) ≤ 1).trans hc1
+  have hR : 0 ≤ R := by dsimp only [R]; positivity
+  have hL : 3 * R < L := by dsimp only [R, L]; linarith
+  have hmarked : marked ⊆ s := filter_subset _ _
+  have hsmall' : c * budget ε m ≤ 1 / 8 := hsmall
+  have hE : budget ε m ≤ 1 / 8 :=
+    (le_mul_of_one_le_left (budget_nonneg hε) hc1).trans hsmall'
+  have hεlt (i : ℕ) (hi : i ≤ m) : ε i < 1 := by
+    have h := (error_le_budget hε hi).trans hE
+    linarith
+  have hraw (i : ℕ) (hi : i ≤ m) (y : ι) (hy : y ∈ s) :
+      |uncompressedRow Δ raw₀ i y 0 - truth y 0| ≤ (1 + truth y 0) * ε i ∧
+        |uncompressedRow Δ raw₀ i y 1 - truth y 1| ≤ ε i :=
+    abs_sub_le_of_clippedError_le (hfirst y hy) (hεlt i hi) (herr i hi y hy)
+  have hincr (i : ℕ) (hi : i < m) (y : ι) (hy : y ∈ s) :
+      |Δ i y 0| ≤ (1 + truth y 0) * (ε i + ε (i + 1)) ∧
+        |Δ i y 1| ≤ ε i + ε (i + 1) := by
+    have hbefore := hraw i hi.le y hy
+    have hafter := hraw (i + 1) hi y hy
+    have heq (ν : Fin 2) : Δ i y ν =
+        (uncompressedRow Δ raw₀ (i + 1) y ν - truth y ν) -
+          (uncompressedRow Δ raw₀ i y ν - truth y ν) := by
+      rw [uncompressedRow_succ]
+      ring
+    constructor
+    · rw [heq 0]
+      exact (abs_sub _ _).trans (by linarith [hbefore.1, hafter.1])
+    · rw [heq 1]
+      exact (abs_sub _ _).trans (by linarith [hbefore.2, hafter.2])
+  have hoff (y : ι) (hy : y ∈ s) (hm : y ∉ marked) : truth y 0 ≤ L := by
+    exact not_lt.mp fun h => hm (mem_filter.mpr ⟨hy, h⟩)
+  have hinit (y : ι) (hy : y ∈ s) (ν : Fin 2) : |a'.row y ν - b'.row y ν| ≤ c * ε 0 := by
+    have hr := hraw 0 (Nat.zero_le m) y hy
+    simp only [uncompressedRow_zero] at hr
+    fin_cases ν
+    · by_cases hm : y ∈ marked
+      · change |sentinelFirst marked L a.row y 0 - sentinelFirst marked L b.row y 0| ≤ _
+        rw [sentinelFirst_zero_of_mem hm, sentinelFirst_zero_of_mem hm, sub_self, abs_zero]
+        exact mul_nonneg hc0 (hε 0 (Nat.zero_le m))
+      · change |sentinelFirst marked L a.row y 0 - sentinelFirst marked L b.row y 0| ≤ _
+        rw [sentinelFirst_of_not_mem hm, sentinelFirst_of_not_mem hm]
+        change |raw₀ y 0 + loss y 0 - (truth y 0 + loss y 0)| ≤ _
+        rw [add_sub_add_right_eq_sub]
+        exact hr.1.trans (mul_le_mul_of_nonneg_right (by dsimp only [c]; linarith [hoff y hy hm])
+          (hε 0 (Nat.zero_le m)))
+    · change |sentinelFirst marked L a.row y 1 - sentinelFirst marked L b.row y 1| ≤ _
+      rw [sentinelFirst_one, sentinelFirst_one]
+      change |raw₀ y 1 + loss y 1 - (truth y 1 + loss y 1)| ≤ _
+      rw [add_sub_add_right_eq_sub]
+      exact hr.2.trans (le_mul_of_one_le_left (hε 0 (Nat.zero_le m)) hc1)
+  have hΔ' (i : ℕ) (hi : i < m) (y : ι) (hy : y ∈ s) (ν : Fin 2) :
+      |Δ' i y ν - (0 : ι → Fin 2 → ℝ) y ν| ≤ c * (ε i + ε (i + 1)) := by
+    have hsum0 := add_nonneg (hε i hi.le) (hε (i + 1) hi)
+    simp only [Pi.zero_apply, sub_zero]
+    fin_cases ν
+    · by_cases hm : y ∈ marked
+      · change |sentinelFirst marked 0 (Δ i) y 0| ≤ _
+        rw [sentinelFirst_zero_of_mem hm, abs_zero]
+        exact mul_nonneg hc0 hsum0
+      · change |sentinelFirst marked 0 (Δ i) y 0| ≤ _
+        rw [sentinelFirst_of_not_mem hm]
+        exact (hincr i hi y hy).1.trans (mul_le_mul_of_nonneg_right
+          (by dsimp only [c]; linarith [hoff y hy hm]) hsum0)
+    · change |sentinelFirst marked 0 (Δ i) y 1| ≤ _
+      rw [sentinelFirst_one]
+      exact (hincr i hi y hy).2.trans (le_mul_of_one_le_left hsum0 hc1)
+  have hreference := sentinel_reference_bounds hη hL₀ hK hzη hfirst hsecond hloss hcount
+  change (∀ y ∈ s, -η ≤ b'.row y 0) ∧ (∀ y ∈ s, |b'.row y 1| ≤ η) ∧
+    firstRank s K b'.defaultValue b'.row ≤ 2 * L₀ at hreference
+  have hstates (i : ℕ) (hi : i ≤ m) :
+      |(A i).defaultValue - (B i).defaultValue| ≤ c * budget ε i ∧
+        ∀ y ∈ s, ∀ ν, |(A i).row y ν - (B i).row y ν| ≤ c * budget ε i := by
+    have hz' : |a'.defaultValue - b'.defaultValue| ≤ c * ε 0 := by
+      change |z - z| ≤ _
+      simpa only [sub_self, abs_zero] using mul_nonneg hc0 (hε 0 (Nat.zero_le m))
+    have hs := iterate_stability_of_increment_error (ρ := ρ)
+      (mul_nonneg hc0 (hε 0 (Nat.zero_le m))) hz' hinit i
+      (fun k hk => hK.trans_le (hKn k (hk.trans_le hi))) (fun _ _ => hK)
+      (fun k hk => mul_nonneg hc0
+        (add_nonneg (hε k (hk.le.trans hi)) (hε (k + 1) (hk.trans_le hi))))
+      (fun k hk => hΔ' k (hk.trans_le hi))
+    have heq : (28 : ℝ) ^ i * (c * ε 0) +
+        ∑ k ∈ range i, 28 ^ (i - k) * (c * (ε k + ε (k + 1))) = c * budget ε i := by
+      simp only [budget, mul_add, mul_sum]
+      congr 1
+      · ring
+      · apply sum_congr rfl
+        intro k _
+        ring
+    rw [heq] at hs
+    exact hs
+  have hceil (i : ℕ) (hi : i < m) :
+      firstRank s K (A i).defaultValue (inputRow s n (fun _ => K) ρ Δ' a' i) ≤ R ∧
+        stepThreshold s n (fun _ => K) ρ Δ' a' i ≤ R := by
+    let D := c * (budget ε i + (ε i + ε (i + 1)))
+    have hD0 : 0 ≤ D := mul_nonneg hc0 (add_nonneg
+      (budget_nonneg fun k hk => hε k (hk.trans hi.le))
+      (add_nonneg (hε i hi.le) (hε (i + 1) hi)))
+    have hD : D ≤ 1 / 8 :=
+      (mul_le_mul_of_nonneg_left (input_budget_le hε hi) hc0).trans hsmall'
+    have hs := hstates i hi.le
+    have hzD : |(A i).defaultValue - (B i).defaultValue| ≤ D :=
+      hs.1.trans (mul_le_mul_of_nonneg_left (le_add_of_nonneg_right
+        (add_nonneg (hε i hi.le) (hε (i + 1) hi))) hc0)
+    have hwD (y : ι) (hy : y ∈ s) (ν : Fin 2) :
+        |inputRow s n (fun _ => K) ρ Δ' a' i y ν - (B i).row y ν| ≤ D := by
+      have hd := hΔ' i hi y hy ν
+      simp only [Pi.zero_apply, sub_zero] at hd
+      change |(A i).row y ν + Δ' i y ν - (B i).row y ν| ≤ _
+      calc
+        _ = |((A i).row y ν - (B i).row y ν) + Δ' i y ν| := by congr 1; ring
+        _ ≤ |(A i).row y ν - (B i).row y ν| + |Δ' i y ν| := abs_add_le _ _
+        _ ≤ c * budget ε i + c * (ε i + ε (i + 1)) := add_le_add (hs.2 y hy ν) hd
+        _ = D := by dsimp only [D]; ring
+    have hqref : firstRank s K (B i).defaultValue (B i).row ≤ 2 * L₀ :=
+      reference_iterate_firstRank_le hη (by linarith) hK hreference.1 hreference.2.1
+        hreference.2.2 i (fun k hk => hKn k (hk.trans hi)) (fun k hk => hρ k (hk.trans hi))
+    have huref : threshold s (n i) (ρ i) (B i).defaultValue (B i).row ≤ 2 * L₀ := by
+      have h := reference_stepThreshold_le hη (by linarith) hK hreference.1 hreference.2.1
+        hreference.2.2 i (fun k hk => hKn k (hk.trans_lt hi))
+        (fun k hk => hρ k (hk.trans_lt hi))
+      simpa only [stepThreshold, inputRow, add_zero] using h
+    have hqdiff : |firstRank s K (A i).defaultValue
+        (inputRow s n (fun _ => K) ρ Δ' a' i) -
+          firstRank s K (B i).defaultValue (B i).row| ≤ D :=
+      (abs_max_sub_max_le_max _ _ _ _).trans
+        (max_le hzD (abs_kthLargest_sub_kthLargest_le hK hD0 (fun y hy => hwD y hy 0)))
+    have hudiff := abs_threshold_sub_threshold_le (ρ := ρ i) (hK.trans_le (hKn i hi))
+      hD0 hzD hwD
+    constructor
+    · have h := (le_abs_self _).trans hqdiff
+      change firstRank s K (A i).defaultValue (inputRow s n (fun _ => K) ρ Δ' a' i) -
+        firstRank s K (B i).defaultValue (B i).row ≤ D at h
+      dsimp only [R]
+      linarith
+    · have h := (le_abs_self _).trans hudiff
+      change threshold s (n i) (ρ i) (A i).defaultValue
+        (inputRow s n (fun _ => K) ρ Δ' a' i) -
+          threshold s (n i) (ρ i) (B i).defaultValue (B i).row ≤ D at h
+      change threshold s (n i) (ρ i) (A i).defaultValue
+        (inputRow s n (fun _ => K) ρ Δ' a' i) ≤ R
+      dsimp only [R]
+      linarith
+  have hvar (y : ι) (hy : y ∈ marked) :
+      3 * R + ∑ i ∈ range m, |Δ i y 0| < a.row y 0 := by
+    have hys := hmarked hy
+    have hd := (mem_filter.mp hy).2
+    have hraw₀ := (hraw 0 (Nat.zero_le m) y hys).1
+    simp only [uncompressedRow_zero] at hraw₀
+    have hlo := (abs_le.mp hraw₀).1
+    have hlosslo := (abs_le.mp (hloss y hys 0)).1
+    have hs : ∑ i ∈ range m, |Δ i y 0| ≤
+        (1 + truth y 0) * ∑ i ∈ range m, (ε i + ε (i + 1)) := by
+      rw [mul_sum]
+      exact sum_le_sum fun i hi => (hincr i (mem_range.mp hi) y hys).1
+    have he : (1 + truth y 0) * (ε 0 + ∑ i ∈ range m, (ε i + ε (i + 1))) ≤
+        (1 + truth y 0) / 8 := by
+      have h := mul_le_mul_of_nonneg_left ((sum_errors_le_budget hε).trans hE)
+        (by linarith [hfirst y hys] : 0 ≤ 1 + truth y 0)
+      linarith
+    change 3 * R + ∑ i ∈ range m, |Δ i y 0| < raw₀ y 0 + loss y 0
+    dsimp only [L] at hd
+    dsimp only [R]
+    nlinarith
+  exact iterate_sentinelState_of_sum_abs_lt m hmarked hK hKn hR hL hvar
+    (fun i hi => (hceil i hi).1) (fun i hi => (hceil i hi).2)
+
+end Cslib.RowCompression
diff --git a/ComplexityTests/RowCompressionSentinelRelative.lean b/ComplexityTests/RowCompressionSentinelRelative.lean
new file mode 100644
index 000000000..9f3217201
--- /dev/null
+++ b/ComplexityTests/RowCompressionSentinelRelative.lean
@@ -0,0 +1,203 @@
+/-
+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.SentinelRelative
+import Complexity.Foundations.Analysis.RowCompression.FalseOverflow
+import Mathlib.LinearAlgebra.Matrix.Notation
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.IntervalCases
+import Mathlib.Tactic.NormNum
+
+/-!
+# Clipped-prefix budgets for an actual sentinel comparison
+
+The true first row is `(1000, 0)`, with one entry above the fixed threshold `1`. A local
+two-group calculation starts from the already-added input of its first group. Its first
+increment is zero; its second increment changes a large first entry and signed second entries.
+The first actual threshold is `10⁻⁷`, strictly above the floor `10⁻⁹`. Compression raises the
+default and erases the low entry's negative second channel. Every raw prefix nevertheless has
+clipped error at most `10⁻⁶`.
+
+The theorem derives coupling to the common sentinel `32`, including exact defaults and padded
+ranks and the original marked channels' nonconstant raw evolution. A zero-initial global run
+has the same two-group result, while its preceding raw prefix has large error. This checks why
+the local comparison starts after adding the first overflow group's input.
+-/
+
+namespace ComplexityTests.RowCompressionSentinelRelative
+
+open Finset Cslib.RowCompression
+open scoped BigOperators
+
+private noncomputable def truth : Fin 2 → Fin 2 → ℝ := ![![1000, 0], ![0, 0]]
+
+private noncomputable def raw₀ : Fin 2 → Fin 2 → ℝ :=
+  ![![1000, -1 / 4000000], ![1 / 10000000, -1 / 20000000]]
+
+private noncomputable def later : Fin 2 → Fin 2 → ℝ :=
+  ![![1 / 10000, 1 / 8000000], ![-1 / 20000000, 1 / 40000000]]
+
+private noncomputable def increments (i : ℕ) : Fin 2 → Fin 2 → ℝ :=
+  if i = 1 then later else 0
+
+private noncomputable def initial : State (Fin 2) := ⟨0, raw₀⟩
+
+private noncomputable def original : ℕ → State (Fin 2) :=
+  iterate univ (fun _ => 2) (fun _ => 2) (fun _ => 1 / 1000000000) increments initial
+
+private noncomputable def modified : ℕ → State (Fin 2) :=
+  iterate univ (fun _ => 2) (fun _ => 2) (fun _ => 1 / 1000000000)
+    (fun i => sentinelFirst {0} 0 (increments i)) (sentinelState {0} 32 initial)
+
+private theorem heavy_set : ({y | (1 : ℝ) < truth y 0} : Finset (Fin 2)) = {0} := by
+  ext y
+  fin_cases y <;> norm_num [truth]
+
+private theorem marked_set : ({y | (32 : ℝ) < truth y 0} : Finset (Fin 2)) = {0} := by
+  ext y
+  fin_cases y <;> norm_num [truth]
+
+private theorem prefix_error (i : ℕ) (hi : i ≤ 2) (y : Fin 2) :
+    clippedError (truth y 0) (truth y 1) (uncompressedRow increments raw₀ i y) ≤
+      1 / 1000000 := by
+  interval_cases i <;> fin_cases y <;>
+    norm_num [clippedError, uncompressedRow, increments, raw₀, later, truth, sum_range_succ]
+
+-- This is the exact finite weighted budget used by the theorem, including the initial error.
+example : (1 + 16 * ((1 : ℝ) + 1)) *
+    (28 ^ 2 * (1 / 1000000) + ∑ i ∈ range 2,
+      28 ^ (2 - i) * (1 / 1000000 + 1 / 1000000)) = 9933 / 125000 := by
+  norm_num [sum_range_succ]
+
+private theorem coupling (j : ℕ) (hj : j ≤ 2) :
+    modified j = sentinelState {0} 32 (original j) ∧
+      (∀ y ∈ ({0} : Finset (Fin 2)), (original j).row y =
+        uncompressedRow increments initial.row j y) ∧
+      (0 < j → firstRank univ 2 (original j).defaultValue (original j).row =
+        firstRank univ 2 (modified j).defaultValue (modified j).row ∧
+          firstRank univ 2 (modified j).defaultValue (modified j).row ≤ 3) := by
+  have h := iterate_sentinelState_of_clippedError_le (s := (univ : Finset (Fin 2)))
+    (n := fun _ => 2) (K := 2) (ρ := fun _ => 1 / 1000000000)
+    (η := 1) (L₀ := 1) (z := 0) (truth := truth) (raw₀ := raw₀)
+    (loss := 0) (Δ := increments) (ε := fun _ => 1 / 1000000) 2
+    (by norm_num) le_rfl (by norm_num) (by norm_num)
+    (by intros; exact le_rfl) (by intros; norm_num)
+    (by intro y _; fin_cases y <;> norm_num [truth])
+    (by intro y _; fin_cases y <;> norm_num [truth])
+    (by intros; norm_num)
+    (by rw [heavy_set]; norm_num)
+    (by intros; norm_num) (by intro i hi y _; exact prefix_error i hi y)
+    (by norm_num [sum_range_succ]) j hj
+  norm_num only [show (16 : ℝ) * (1 + 1) = 32 by norm_num,
+    show (2 : ℝ) * 1 + 1 = 3 by norm_num, marked_set, add_zero] at h
+  exact h
+
+private theorem rank_two (v : Fin 2 → ℝ)
+    (h0 : v 0 = 1000) (h1 : v 1 = 1 / 10000000) :
+    kthLargest 2 univ v = 1 / 10000000 := by
+  apply le_antisymm
+  · refine not_lt.mp fun hlt => ?_
+    have hc := (lt_kthLargest_iff (by norm_num)
+      (by norm_num : (0 : ℝ) ≤ 1 / 10000000)).mp hlt
+    have hs : ({y | (1 / 10000000 : ℝ) < v y} : Finset (Fin 2)) = {0} := by
+      ext y
+      fin_cases y <;> norm_num [h0, h1]
+    rw [hs] at hc
+    norm_num at hc
+  · apply (le_kthLargest_iff (by norm_num) (by norm_num : (0 : ℝ) < 1 / 10000000)).mpr
+    have hs : ({y | (1 / 10000000 : ℝ) ≤ v y} : Finset (Fin 2)) = univ := by
+      ext y
+      fin_cases y <;> norm_num [h0, h1]
+    rw [hs]
+    norm_num
+
+private theorem first_threshold :
+    threshold univ 2 (1 / 1000000000) 0 raw₀ = 1 / 10000000 := by
+  unfold threshold
+  rw [rank_two (fun y => entrySize (raw₀ y)) (by norm_num [raw₀, entrySize])
+    (by norm_num [raw₀, entrySize])]
+  norm_num
+
+private theorem first_default :
+    newDefault univ 2 2 (1 / 1000000000) 0 raw₀ = 1 / 10000000 := by
+  unfold newDefault
+  rw [first_threshold, rank_two (fun y => raw₀ y 0) (by norm_num [raw₀])
+    (by norm_num [raw₀])]
+  norm_num
+
+private theorem first_state : original 1 =
+    ⟨1 / 10000000, ![![1000, -1 / 4000000], ![1 / 10000000, 0]]⟩ := by
+  change advance univ 2 2 (1 / 1000000000) (increments 0) initial = _
+  simp only [advance, initial, increments, show (0 : ℕ) ≠ 1 by decide, ↓reduceIte, add_zero]
+  rw [first_default]
+  congr 1
+  unfold update
+  rw [first_threshold, first_default]
+  funext y ν
+  fin_cases y <;> fin_cases ν <;>
+    norm_num [updateEntry, radius, entrySize, defaultEntry, raw₀]
+
+-- There is a genuine first overflow, nonzero default, and erased negative second channel.
+example : IsFirstOverflow univ (fun _ => 2) (fun _ => 2) (fun _ => 1 / 1000000000)
+      increments initial 0 ∧
+    (original 1).defaultValue = 1 / 10000000 ∧
+    uncompressedRow increments initial.row 1 1 1 = -1 / 20000000 ∧
+    (original 1).row 1 1 = 0 := by
+  refine ⟨⟨by simp, ?_⟩, ?_⟩
+  · simpa only [stepThreshold, inputRow, iterate_zero, initial, increments,
+      show (0 : ℕ) ≠ 1 by decide, ↓reduceIte, add_zero, first_threshold] using
+      (show (1 / 1000000000 : ℝ) < 1 / 10000000 by norm_num)
+  · rw [first_state]
+    norm_num [uncompressedRow, initial, increments, raw₀]
+
+-- Original marked first and signed second channels evolve; only the modified first is fixed.
+example : (original 2).row 0 0 = 10000001 / 10000 ∧
+    (original 2).row 0 1 = -1 / 8000000 ∧
+    (modified 2).row 0 0 = 32 ∧ (modified 2).row 0 1 = -1 / 8000000 ∧
+    (modified 2).defaultValue = (original 2).defaultValue ∧
+    firstRank univ 2 (original 2).defaultValue (original 2).row =
+      firstRank univ 2 (modified 2).defaultValue (modified 2).row := by
+  obtain ⟨heq, hraw, hq⟩ := coupling 2 le_rfl
+  have hraw0 := hraw 0 (by simp)
+  rw [heq]
+  simp only [sentinelState, sentinelFirst_zero_of_mem (by simp : (0 : Fin 2) ∈ ({0} : Finset _)),
+    sentinelFirst_one, hraw0]
+  norm_num [uncompressedRow, initial, increments, raw₀, later, sum_range_succ]
+  simpa only [heq, sentinelState] using (hq (by norm_num)).1
+
+private noncomputable def globalIncrements (i : ℕ) : Fin 2 → Fin 2 → ℝ :=
+  if i = 0 then raw₀ else increments i
+
+private noncomputable def globalRun : ℕ → State (Fin 2) :=
+  iterate univ (fun _ => 2) (fun _ => 2) (fun _ => 1 / 1000000000)
+    globalIncrements ⟨0, 0⟩
+
+-- Start the comparison after adding the overflow input: the local first increment is zero.
+example : globalRun 2 = original 2 ∧ increments 0 = 0 ∧
+    uncompressedRow globalIncrements 0 1 = raw₀ ∧
+    1 / 1000000 < clippedError (truth 0 0) (truth 0 1)
+      (uncompressedRow globalIncrements 0 0 0) := by
+  have hfirst : globalRun 1 = original 1 := by
+    simp only [globalRun, original, iterate_succ, iterate_zero, advance, initial,
+      globalIncrements, increments, show (0 : ℕ) ≠ 1 by decide, ↓reduceIte, zero_add, add_zero]
+  refine ⟨?_, ?_, ?_, ?_⟩
+  · change advance univ 2 2 (1 / 1000000000) (globalIncrements 1) (globalRun 1) =
+      advance univ 2 2 (1 / 1000000000) (increments 1) (original 1)
+    rw [hfirst]
+    rfl
+  · simp [increments]
+  · funext y ν
+    simp [uncompressedRow, globalIncrements]
+  · norm_num [uncompressedRow, clippedError, truth]
+
+-- The small-heavy-set branch is a real restriction, and unclipping needs a strict bound below one.
+example : ¬ #{y : Fin 2 | (1 : ℝ) < (![1000, 1000] : Fin 2 → ℝ) y} < 2 := by
+  norm_num [Fin.univ_succ, filter_insert, filter_singleton]
+
+example : clippedError 0 0 ![2, 0] = 1 ∧ ¬ |(2 : ℝ) - 0| ≤ (1 + 0) * 1 := by
+  norm_num [clippedError]
+
+end ComplexityTests.RowCompressionSentinelRelative