diff --git a/Complexity.lean b/Complexity.lean
index 4ec2d31ed..48f916e1e 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2454,6 +2454,7 @@ public import Complexity.Foundations.Analysis.RowCompression.OverflowNoise
 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.Stationary
 public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos
 public import Complexity.Foundations.Analysis.SpecialFunctions.PolynomialSwitch
diff --git a/Complexity/Foundations/Analysis/RowCompression/SentinelIteration.lean b/Complexity/Foundations/Analysis/RowCompression/SentinelIteration.lean
new file mode 100644
index 000000000..5a1558e23
--- /dev/null
+++ b/Complexity/Foundations/Analysis/RowCompression/SentinelIteration.lean
@@ -0,0 +1,247 @@
+/-
+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.Sentinel
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Tactic.Linarith
+
+/-!
+# Removing sentinels through an actual compression schedule
+
+The modified calculation starts from `sentinelState marked L a` and uses increments
+`sentinelFirst marked 0 (Δ i)`. Thus only marked first-channel increments are removed; second
+increments are unchanged. If the actual modified input ranks and thresholds are bounded by
+`R ≥ 0`, and `3R` plus the total absolute first-channel variation is below every marked initial
+first coordinate, the two actual calculations remain coupled at every prefix.
+
+Their defaults agree, the modified full row is the sentinel replacement of the original row,
+and both original marked coordinates follow their actual uncompressed prefixes. The latter
+fact derives the large-input condition needed at the next step. After every positive prefix,
+the padded first ranks also agree and are at most `R`.
+
+This supplies the removal induction in [OpenAI2026LogSpace, Lemma 8.3]. It assumes explicit
+ceilings only for the modified calculation; no bound on original compressed inputs or desired
+final output is assumed. Deriving the ceilings and variation hypothesis from clipped errors,
+upper saturation of row functions, the heavy-count case, and full post-overflow stability remain
+separate. No implementation for finding or storing the analytical sentinels is asserted.
+
+## Main definitions
+
+* `Cslib.RowCompression.sentinelState`: preserve the default and replace marked first entries.
+
+## Main results
+
+* `Cslib.RowCompression.firstRank_update_le_of_le`: explicit input rank and threshold ceilings
+  bound the updated padded rank, without reference-row shape hypotheses.
+* `Cslib.RowCompression.iterate_sentinelState_of_sum_abs_lt`: actual multi-step removal with
+  raw-prefix preservation at marked endpoints and exact rank equality after positive prefixes.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 8.3, proof of Lemma 8.3, induction removing the sentinel modification
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+namespace Cslib.RowCompression
+
+open Finset
+
+variable {ι : Type*}
+
+/-- Replace marked first entries in a state, retaining its actual common default. -/
+@[expose] noncomputable def sentinelState (marked : Finset ι) (L : ℝ) (a : State ι) : State ι :=
+  { defaultValue := a.defaultValue, row := sentinelFirst marked L a.row }
+
+/-- Clearing marked first increments makes addition commute exactly with sentinel replacement. -/
+theorem sentinelFirst_add (marked : Finset ι) (L : ℝ) (w Δ : ι → Fin 2 → ℝ) :
+    sentinelFirst marked L (w + Δ) = sentinelFirst marked L w + sentinelFirst marked 0 Δ := by
+  classical
+  funext y ν
+  by_cases h : y ∈ marked ∧ ν = 0 <;> simp [sentinelFirst, h]
+
+section Update
+
+variable {s marked : Finset ι} {n K : ℕ} {ρ z R L : ℝ} {w : ι → Fin 2 → ℝ}
+
+/-- The updated padded first rank remains below a common input rank and threshold ceiling.
+No lower bound on raw first entries or upper bound on second entries is needed. -/
+theorem firstRank_update_le_of_le (hK : 0 < K) (hR : 0 ≤ R)
+    (hq : firstRank s K z w ≤ R) (hu : threshold s n ρ z w ≤ R) :
+    firstRank s K (newDefault s n K ρ z w) (update s n K ρ z w) ≤ R := by
+  have hb : newDefault s n K ρ z w ≤ R :=
+    max_le hu ((min_le_left _ _).trans hq)
+  refine max_le hb ?_
+  by_contra h
+  have hcard := (lt_kthLargest_iff hK hR).mp (lt_of_not_ge h)
+  have hsub : ({y ∈ s | R < update s n K ρ z w y 0} : Finset ι) ⊆
+      {y ∈ s | R < w y 0} := by
+    intro y hy
+    obtain ⟨hys, hy⟩ := mem_filter.mp hy
+    refine mem_filter.mpr ⟨hys, ?_⟩
+    by_contra hfirst
+    have hout := (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 hout
+    exact (not_lt_of_ge (hout.trans (max_le (not_lt.mp hfirst) hb))) hy
+  have hlt := (lt_kthLargest_iff hK hR).mpr (hcard.trans (card_le_card hsub))
+  exact (not_lt_of_ge (kthLargest_le_firstRank.trans hq)) hlt
+
+private theorem sentinelFirst_update_all (hmarked : marked ⊆ s)
+    (hK : 0 < K) (hKn : K ≤ n) (hR : 0 ≤ R) (hL : 3 * R < L)
+    (hw : ∀ y ∈ s, y ∈ marked → 3 * R < w y 0)
+    (hq : firstRank s K z (sentinelFirst marked L w) ≤ R)
+    (hu : threshold s n ρ z (sentinelFirst marked L w) ≤ R) :
+    sentinelFirst marked L (update s n K ρ z w) =
+      update s n K ρ z (sentinelFirst marked L w) := by
+  funext y
+  by_cases hm : y ∈ marked
+  · exact sentinelFirst_update hK hKn hR hL hw hq hu (hmarked hm)
+  · have hL' : R < L := by linarith
+    have hw' : ∀ y ∈ s, y ∈ marked → R < w y 0 := by
+      intro y hy hm
+      linarith [hw y hy hm]
+    rw [sentinelFirst_of_not_mem hm]
+    unfold update
+    rw [threshold_eq_sentinelFirst (hK.trans_le hKn) hR hL' hw' hu,
+      newDefault_eq_sentinelFirst (hK.trans_le hKn) hK hR hL' hw' hq hu,
+      sentinelFirst_of_not_mem hm]
+
+private theorem advance_sentinelState {a : State ι} {Δ : ι → Fin 2 → ℝ}
+    (hmarked : marked ⊆ s) (hK : 0 < K) (hKn : K ≤ n) (hR : 0 ≤ R) (hL : 3 * R < L)
+    (hw : ∀ y ∈ s, y ∈ marked → 3 * R < (a.row + Δ) y 0)
+    (hq : firstRank s K a.defaultValue (sentinelFirst marked L (a.row + Δ)) ≤ R)
+    (hu : threshold s n ρ a.defaultValue (sentinelFirst marked L (a.row + Δ)) ≤ R) :
+    advance s n K ρ (sentinelFirst marked 0 Δ) (sentinelState marked L a) =
+      sentinelState marked L (advance s n K ρ Δ a) := by
+  have hL' : R < L := by linarith
+  have hw' : ∀ y ∈ s, y ∈ marked → R < (a.row + Δ) y 0 := by
+    intro y hy hm
+    linarith [hw y hy hm]
+  unfold advance sentinelState
+  rw [← sentinelFirst_add]
+  congr 1
+  · exact (newDefault_eq_sentinelFirst (hK.trans_le hKn) hK hR hL' hw' hq hu).symm
+  · exact (sentinelFirst_update_all hmarked hK hKn hR hL hw hq hu).symm
+
+end Update
+
+section Iteration
+
+variable {s marked : Finset ι} {n : ℕ → ℕ} {K : ℕ} {ρ : ℕ → ℝ} {R L : ℝ}
+  {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι}
+
+private theorem raw_first_gt_of_sum_abs_lt {m j : ℕ} {y : ι} (hj : j ≤ m)
+    (hvar : 3 * R + ∑ i ∈ range m, |Δ i y 0| < a.row y 0) :
+    3 * R < uncompressedRow Δ a.row j y 0 := by
+  have hsum : ∑ i ∈ range j, |Δ i y 0| ≤ ∑ i ∈ range m, |Δ i y 0| :=
+    sum_le_sum_of_subset_of_nonneg (range_mono hj) (fun _ _ _ => abs_nonneg _)
+  have habs : |∑ i ∈ range j, Δ i y 0| ≤ ∑ i ∈ range m, |Δ i y 0| :=
+    (abs_sum_le_sum_abs _ _).trans hsum
+  have hlo := (abs_le.mp habs).1
+  change 3 * R < a.row y 0 + ∑ i ∈ range j, Δ i y 0
+  linarith
+
+/-- **Actual multi-step sentinel removal**. Only the modified run's input ranks and thresholds
+are assumed bounded. Total raw first-channel variation proves that original marked inputs stay
+in the compression identity region. Both original marked channels follow their raw prefixes.
+
+The result also identifies the actual padded ranks after every positive prefix and bounds them
+by `R`. No equality or regularity law for final row outputs is assumed. -/
+theorem iterate_sentinelState_of_sum_abs_lt (m : ℕ) (hmarked : marked ⊆ s)
+    (hK : 0 < K) (hKn : ∀ i < m, K ≤ n i) (hR : 0 ≤ R) (hL : 3 * R < L)
+    (hvar : ∀ y ∈ marked, 3 * R + ∑ i ∈ range m, |Δ i y 0| < a.row y 0) :
+    let Δ' := fun i => sentinelFirst marked 0 (Δ i)
+    let b := sentinelState marked L a
+    (∀ i < m, firstRank s K (iterate s n (fun _ => K) ρ Δ' b i).defaultValue
+      (inputRow s n (fun _ => K) ρ Δ' b i) ≤ R) →
+    (∀ i < m, stepThreshold s n (fun _ => K) ρ Δ' b i ≤ R) →
+    ∀ j ≤ m,
+      let original := iterate s n (fun _ => K) ρ Δ a j
+      let modified := iterate s n (fun _ => K) ρ Δ' b j
+      modified = sentinelState marked L original ∧
+        (∀ y ∈ marked, original.row y = uncompressedRow Δ a.row j y) ∧
+        (0 < j → firstRank s K original.defaultValue original.row =
+          firstRank s K modified.defaultValue modified.row ∧
+            firstRank s K modified.defaultValue modified.row ≤ R) := by
+  let Δ' := fun i => sentinelFirst marked 0 (Δ i)
+  let b := sentinelState marked L a
+  let A := iterate s n (fun _ => K) ρ Δ a
+  let B := iterate s n (fun _ => K) ρ Δ' b
+  change (∀ i < m, firstRank s K (B i).defaultValue
+      (inputRow s n (fun _ => K) ρ Δ' b i) ≤ R) →
+    (∀ i < m, stepThreshold s n (fun _ => K) ρ Δ' b i ≤ R) →
+    ∀ j ≤ m, B j = sentinelState marked L (A j) ∧
+      (∀ y ∈ marked, (A j).row y = uncompressedRow Δ a.row j y) ∧
+      (0 < j → firstRank s K (A j).defaultValue (A j).row =
+        firstRank s K (B j).defaultValue (B j).row ∧
+          firstRank s K (B j).defaultValue (B j).row ≤ R)
+  intro hq hu j
+  induction j with
+  | zero =>
+    intro _
+    refine ⟨rfl, ?_, fun h => (Nat.not_lt_zero _ h).elim⟩
+    intro y _
+    simp only [uncompressedRow_zero, A, iterate_zero]
+  | succ j ih =>
+    intro hj
+    have hjm : j < m := (Nat.lt_succ_self j).trans_le hj
+    obtain ⟨heq, hraw, _⟩ := ih ((Nat.le_succ j).trans hj)
+    have hinput : inputRow s n (fun _ => K) ρ Δ' b j =
+        sentinelFirst marked L (inputRow s n (fun _ => K) ρ Δ a j) := by
+      change (B j).row + Δ' j = sentinelFirst marked L ((A j).row + Δ j)
+      rw [heq]
+      exact (sentinelFirst_add marked L (A j).row (Δ j)).symm
+    have hq' : firstRank s K (A j).defaultValue
+        (sentinelFirst marked L (inputRow s n (fun _ => K) ρ Δ a j)) ≤ R := by
+      have h := hq j hjm
+      rw [hinput, heq] at h
+      exact h
+    have hu' : threshold s (n j) (ρ j) (A j).defaultValue
+        (sentinelFirst marked L (inputRow s n (fun _ => K) ρ Δ a j)) ≤ R := by
+      have h := hu j hjm
+      change threshold s (n j) (ρ j) (B j).defaultValue
+        (inputRow s n (fun _ => K) ρ Δ' b j) ≤ R at h
+      rw [hinput, heq] at h
+      exact h
+    have hrawInput (y : ι) (hy : y ∈ marked) :
+        inputRow s n (fun _ => K) ρ Δ a j y = uncompressedRow Δ a.row (j + 1) y := by
+      funext ν
+      change (A j).row y ν + Δ j y ν = _
+      rw [hraw y hy, uncompressedRow_succ]
+    have hhigh : ∀ y ∈ s, y ∈ marked →
+        3 * R < inputRow s n (fun _ => K) ρ Δ a j y 0 := by
+      intro y _ hy
+      rw [hrawInput y hy]
+      exact raw_first_gt_of_sum_abs_lt hj (hvar y hy)
+    have hnext : B (j + 1) = sentinelState marked L (A (j + 1)) := by
+      change advance s (n j) K (ρ j) (Δ' j) (B j) =
+        sentinelState marked L (advance s (n j) K (ρ j) (Δ j) (A j))
+      rw [heq]
+      exact advance_sentinelState hmarked hK (hKn j hjm) hR hL hhigh hq' hu'
+    have hrawNext (y : ι) (hy : y ∈ marked) :
+        (A (j + 1)).row y = uncompressedRow Δ a.row (j + 1) y := by
+      exact (update_eq_self_of_mem_sentinelFirst (hK.trans_le (hKn j hjm)) hR hL
+        hhigh hu' (hmarked hy) hy).1.trans (hrawInput y hy)
+    have hbound : firstRank s K (B (j + 1)).defaultValue (B (j + 1)).row ≤ R :=
+      firstRank_update_le_of_le hK hR (hq j hjm) (hu j hjm)
+    have hfinal : firstRank s K (A (j + 1)).defaultValue (A (j + 1)).row =
+        firstRank s K (B (j + 1)).defaultValue (B (j + 1)).row := by
+      rw [hnext] at hbound ⊢
+      apply firstRank_eq_sentinelFirst hK hR (by linarith) _ hbound
+      intro y _ hy
+      rw [hrawNext y hy]
+      have h := raw_first_gt_of_sum_abs_lt hj (hvar y hy)
+      linarith
+    exact ⟨hnext, hrawNext, fun _ => ⟨hfinal, hbound⟩⟩
+
+end Iteration
+
+end Cslib.RowCompression
diff --git a/ComplexityTests/RowCompressionSentinelIteration.lean b/ComplexityTests/RowCompressionSentinelIteration.lean
new file mode 100644
index 000000000..90ce23a6c
--- /dev/null
+++ b/ComplexityTests/RowCompressionSentinelIteration.lean
@@ -0,0 +1,182 @@
+/-
+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.SentinelIteration
+import Mathlib.LinearAlgebra.Matrix.Notation
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum
+
+/-!
+# Two actual sentinel compression steps
+
+The marked first coordinate receives increments `-5,+7`; its second coordinate receives
+`+2,-3`. The modified calculation clears only those first increments. Its two input rank and
+threshold ceilings are proved by evaluating its actual intermediate states. The coupling theorem
+then recovers the original marked raw prefix, common defaults, and exact final rank equality.
+An unmarked endpoint has raw first prefix `-2` but compressed value `2`, so the calculation is
+not globally identical to its uncompressed prefixes.
+-/
+
+namespace ComplexityTests.RowCompressionSentinelIteration
+
+open Finset Cslib.RowCompression
+
+private noncomputable def initial : State (Fin 4) :=
+  { defaultValue := 1 / 2, row := ![![1000000, -17], ![4, 0], ![2, -1], ![-1, 1]] }
+
+private def increments (i : ℕ) : Fin 4 → Fin 2 → ℝ :=
+  if i = 0 then ![![-5, 2], ![0, 0], ![0, 0], ![0, 0]]
+  else if i = 1 then ![![7, -3], ![0, 0], ![0, 0], ![-1, 1]] else 0
+
+private noncomputable def cleared (i : ℕ) : Fin 4 → Fin 2 → ℝ :=
+  sentinelFirst {0} 0 (increments i)
+
+private noncomputable def modifiedStart : State (Fin 4) := sentinelState {0} 100 initial
+
+private noncomputable def originalRun : ℕ → State (Fin 4) :=
+  iterate univ (fun _ => 3) (fun _ => 3) (fun _ => 1) increments initial
+
+private noncomputable def modifiedRun : ℕ → State (Fin 4) :=
+  iterate univ (fun _ => 3) (fun _ => 3) (fun _ => 1) cleared modifiedStart
+
+private noncomputable def modifiedInput : ℕ → Fin 4 → Fin 2 → ℝ :=
+  inputRow univ (fun _ => 3) (fun _ => 3) (fun _ => 1) cleared modifiedStart
+
+private def inputZero : Fin 4 → Fin 2 → ℝ := ![![100, -15], ![4, 0], ![2, -1], ![-1, 1]]
+
+private def inputOne : Fin 4 → Fin 2 → ℝ := ![![100, -18], ![2, 0], ![2, 0], ![1, 1]]
+
+private theorem modified_input_zero : modifiedInput 0 = inputZero := by
+  funext y ν
+  fin_cases y <;> fin_cases ν <;>
+    norm_num [modifiedInput, inputRow, modifiedStart, sentinelState, initial, cleared,
+      sentinelFirst, increments, inputZero]
+
+private theorem rank_zero : firstRank univ 3 (1 / 2) inputZero = 2 := by
+  norm_num [firstRank, kthLargest, inputZero, Fin.univ_succ, filter_insert, filter_singleton]
+
+private theorem threshold_zero : threshold univ 3 1 (1 / 2) inputZero = 2 := by
+  norm_num [threshold, entrySize, kthLargest, inputZero, Fin.univ_succ,
+    filter_insert, filter_singleton]
+
+private theorem default_zero : newDefault univ 3 3 1 (1 / 2) inputZero = 2 := by
+  change max (threshold univ 3 1 (1 / 2) inputZero)
+    (min (firstRank univ 3 (1 / 2) inputZero) (3 * threshold univ 3 1 (1 / 2) inputZero)) = 2
+  rw [threshold_zero, rank_zero]
+  norm_num
+
+private theorem modified_one : modifiedRun 1 =
+    { defaultValue := 2, row := ![![100, -15], ![2, 0], ![2, 0], ![2, 0]] } := by
+  have hin : modifiedStart.row + cleared 0 = inputZero := modified_input_zero
+  change advance univ 3 3 1 (cleared 0) modifiedStart = _
+  unfold advance
+  rw [hin]
+  change State.mk (newDefault univ 3 3 1 (1 / 2) inputZero)
+    (update univ 3 3 1 (1 / 2) inputZero) = _
+  rw [default_zero]
+  congr 1
+  unfold update
+  rw [threshold_zero, default_zero]
+  funext y ν
+  fin_cases y <;> fin_cases ν <;>
+    norm_num [updateEntry, radius, entrySize, defaultEntry, inputZero]
+
+private theorem modified_input_one : modifiedInput 1 = inputOne := by
+  change (modifiedRun 1).row + cleared 1 = inputOne
+  rw [modified_one]
+  funext y ν
+  fin_cases y <;> fin_cases ν <;> norm_num [cleared, sentinelFirst, increments, inputOne]
+
+private theorem rank_one : firstRank univ 3 2 inputOne = 2 := by
+  norm_num [firstRank, kthLargest, inputOne, Fin.univ_succ, filter_insert, filter_singleton]
+
+private theorem threshold_one : threshold univ 3 1 2 inputOne = 2 := by
+  norm_num [threshold, entrySize, kthLargest, inputOne, Fin.univ_succ,
+    filter_insert, filter_singleton]
+
+private theorem default_one : newDefault univ 3 3 1 2 inputOne = 2 := by
+  change max (threshold univ 3 1 2 inputOne)
+    (min (firstRank univ 3 2 inputOne) (3 * threshold univ 3 1 2 inputOne)) = 2
+  rw [threshold_one, rank_one]
+  norm_num
+
+private theorem modified_two : modifiedRun 2 =
+    { defaultValue := 2, row := ![![100, -18], ![2, 0], ![2, 0], ![2, 0]] } := by
+  have hin : (modifiedRun 1).row + cleared 1 = inputOne := modified_input_one
+  change advance univ 3 3 1 (cleared 1) (modifiedRun 1) = _
+  unfold advance
+  rw [hin, modified_one]
+  rw [default_one]
+  congr 1
+  unfold update
+  rw [threshold_one, default_one]
+  funext y ν
+  fin_cases y <;> fin_cases ν <;>
+    norm_num [updateEntry, radius, entrySize, defaultEntry, inputOne]
+
+private theorem modified_ceilings (i : ℕ) (hi : i < 2) :
+    firstRank univ 3 (modifiedRun i).defaultValue (modifiedInput i) ≤ 2 ∧
+      threshold univ 3 1 (modifiedRun i).defaultValue (modifiedInput i) ≤ 2 := by
+  have hi' : i = 0 ∨ i = 1 := by omega
+  rcases hi' with rfl | rfl
+  · change firstRank univ 3 (1 / 2) (modifiedInput 0) ≤ 2 ∧
+      threshold univ 3 1 (1 / 2) (modifiedInput 0) ≤ 2
+    rw [modified_input_zero]
+    exact ⟨rank_zero.le, threshold_zero.le⟩
+  · rw [modified_input_one, modified_one]
+    exact ⟨rank_one.le, threshold_one.le⟩
+
+private theorem coupling (j : ℕ) (hj : j ≤ 2) :
+    modifiedRun j = sentinelState {0} 100 (originalRun j) ∧
+      (∀ y ∈ ({0} : Finset (Fin 4)),
+        (originalRun j).row y = uncompressedRow increments initial.row j y) ∧
+      (0 < j → firstRank univ 3 (originalRun j).defaultValue (originalRun j).row =
+        firstRank univ 3 (modifiedRun j).defaultValue (modifiedRun j).row ∧
+          firstRank univ 3 (modifiedRun j).defaultValue (modifiedRun j).row ≤ 2) := by
+  apply iterate_sentinelState_of_sum_abs_lt (s := univ) (marked := {0}) (n := fun _ => 3)
+    (K := 3) (ρ := fun _ => 1) (Δ := increments) (a := initial) (R := 2) (L := 100)
+    2 (subset_univ _) (by norm_num) (by intros; norm_num) (by norm_num) (by norm_num)
+    _ (fun i hi => (modified_ceilings i hi).1) (fun i hi => (modified_ceilings i hi).2) j hj
+  intro y hy
+  have hy0 : y = 0 := mem_singleton.mp hy
+  subst y
+  norm_num [sum_range_succ, increments, initial]
+
+-- Only the marked first increments are removed; nonzero signed second increments survive.
+example : increments 0 0 0 = -5 ∧ increments 1 0 0 = 7 ∧
+    cleared 0 0 0 = 0 ∧ cleared 1 0 0 = 0 ∧ cleared 0 0 1 = 2 ∧ cleared 1 0 1 = -3 := by
+  norm_num [increments, cleared, sentinelFirst]
+
+-- The original marked entry follows both raw prefixes, derived from the actual coupling theorem.
+example : (originalRun 2).row 0 = ![1000002, -18] := by
+  rw [(coupling 2 (by norm_num)).2.1 0 (mem_singleton_self 0)]
+  funext ν
+  fin_cases ν <;> norm_num [uncompressedRow, initial, increments, sum_range_succ]
+
+-- The defaults genuinely rise from 1/2 to 2 and agree in the two actual calculations.
+example : initial.defaultValue = 1 / 2 ∧
+    (originalRun 2).defaultValue = 2 ∧ (modifiedRun 2).defaultValue = 2 := by
+  have heq := congrArg State.defaultValue (coupling 2 (by norm_num)).1
+  rw [modified_two] at heq ⊢
+  exact ⟨rfl, heq.symm, rfl⟩
+
+-- Unmarked first values need not follow raw prefixes; actual compression still takes place.
+example : (originalRun 2).row 3 0 = 2 ∧
+    uncompressedRow increments initial.row 2 3 0 = -2 := by
+  have h := congrArg (fun a : State (Fin 4) => a.row 3 0) (coupling 2 (by norm_num)).1
+  rw [modified_two] at h
+  have hfirst : (originalRun 2).row 3 0 = 2 := by
+    norm_num [sentinelState, sentinelFirst] at h
+    exact h.symm
+  exact ⟨hfirst, by norm_num [uncompressedRow, initial, increments, sum_range_succ]⟩
+
+-- The post-update rank helper is consumed by the actual final-rank conclusion.
+example : firstRank univ 3 (originalRun 2).defaultValue (originalRun 2).row =
+    firstRank univ 3 (modifiedRun 2).defaultValue (modifiedRun 2).row ∧
+      firstRank univ 3 (modifiedRun 2).defaultValue (modifiedRun 2).row ≤ 2 :=
+  (coupling 2 (by norm_num)).2.2 (by norm_num)
+
+end ComplexityTests.RowCompressionSentinelIteration