diff --git a/Complexity.lean b/Complexity.lean
index fd26b807e..e0277879f 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2828,6 +2828,7 @@ public import Complexity.Foundations.Probability.HeavyCount
 public import Complexity.Foundations.Probability.HeavyCountRarity
 public import Complexity.Foundations.Probability.HierarchyParams
 public import Complexity.Foundations.Probability.PolynomialAtomCutoffs
+public import Complexity.Foundations.Probability.PolynomialAtomRows
 public import Complexity.Foundations.Probability.ProductError
 public import Complexity.Foundations.Probability.RootMetric
 public import Complexity.Foundations.Probability.SecondMoment
diff --git a/Complexity/Foundations/Probability/PolynomialAtomRows.lean b/Complexity/Foundations/Probability/PolynomialAtomRows.lean
new file mode 100644
index 000000000..97f83fd5b
--- /dev/null
+++ b/Complexity/Foundations/Probability/PolynomialAtomRows.lean
@@ -0,0 +1,271 @@
+/-
+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.Probability.PolynomialAtomCutoffs
+public import Complexity.Foundations.Probability.CorrectionAtom
+public import Complexity.Foundations.Analysis.RowCompression.Stationary
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+
+/-!
+# Polynomial atom rows under stationary compression
+
+The preparation, auxiliary score, and broad witness are concrete two-variable polynomial
+functions from `Complexity.Foundations.Probability.PolynomialAtomCutoffs`. This file proves
+their strict retained-support bound, zero default output, preservation along the constructed
+stationary reference, and a weighted fourth-root comparison with truth. `PolynomialAtomRow`
+is a closed choice of those three functions; no scalar regularity or support law is assumed.
+
+The common sufficient margin is `0 < η ≤ θ / 10000`, where `θ` is the atom's support scale
+and `η` is the compression scale. The comparison constant depends only on the chosen function,
+`θ`, and `η`; it is independent of the row, finite retained set, rank, schedule, and error
+envelope. The rank includes the actual compressed default. Only the true row uses zero padding.
+The bridges to `Matrix.atomPrep` and `Matrix.auxScore` use their existing zero-padded ranks.
+
+These results instantiate the scalar laws in the stationary-reference portion of
+[OpenAI2026LogSpace, Lemma 8.2] for the three pre-incoming row functions of Section 5.5.
+They belong to the fourth-moment adaptation in complexitylib issue #1721; the pinned paper
+uses eighth roots. Normalized main atoms, incoming-gate assembly, enumeration, post-overflow
+stability, and a machine-space certificate remain separate.
+
+## Main results
+
+* `Cslib.PolynomialAtomRow.card_filter_eval_ne_zero_lt`: actual support has fewer than `K` entries.
+* `Cslib.PolynomialAtomRow.stationaryContinuation_eval_eq`: preservation through the remaining
+  real compression schedule after a prefix without overflow.
+* `Cslib.PolynomialAtomRow.exists_stationaryContinuation_root_bound`: a uniform weighted
+  fourth-root discrepancy bound with all scalar hypotheses discharged.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 5.5, support-margin lemma and compression-threshold table; Section 8.3, Lemma 8.2
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+namespace Cslib
+
+/-- The three concrete pre-incoming row functions with polynomial fourth-root regularity. -/
+inductive PolynomialAtomRow
+  | preparation
+  | auxiliary
+  | witness
+  deriving DecidableEq
+
+namespace PolynomialAtomRow
+
+open Finset RowCompression
+
+/-- Evaluate the chosen concrete function, using rational arithmetic for rational arguments. -/
+@[expose] def eval {R : Type*} [Field R] [LinearOrder R] (kind : PolynomialAtomRow)
+    (θ v r : R) : R :=
+  match kind with
+  | preparation => polynomialPrepRow4 θ v r
+  | auxiliary => polynomialAuxCutoff4 θ v r
+  | witness => polynomialWitnessCutoff4 θ v r
+
+/-- The closed entry-zero threshold of the chosen function. -/
+@[expose] def entryThreshold {R : Type*} [Field R] (kind : PolynomialAtomRow) (θ : R) : R :=
+  match kind with
+  | preparation => θ / 2
+  | auxiliary => θ / 8
+  | witness => 82 * θ / 1000
+
+/-- The closed rank-zero threshold of the chosen function. -/
+@[expose] def gateThreshold {R : Type*} [Field R] (kind : PolynomialAtomRow) (θ : R) : R :=
+  match kind with
+  | preparation => θ / 500
+  | auxiliary => θ / 50
+  | witness => 27 * θ / 1000
+
+variable (kind : PolynomialAtomRow) {θ η v r r' : ℝ}
+
+theorem eval_nonneg (θ v r : ℝ) : 0 ≤ kind.eval θ v r := by
+  cases kind
+  · exact polynomialPrepRow4_nonneg _ _ _
+  · exact polynomialAuxCutoff4_nonneg _ _ _
+  · exact polynomialWitnessCutoff4_nonneg _ _ _
+
+theorem eval_le_one (θ v r : ℝ) : kind.eval θ v r ≤ 1 := by
+  cases kind
+  · exact polynomialPrepRow4_le_one _ _ _
+  · exact polynomialAuxCutoff4_le_one _ _ _
+  · exact polynomialWitnessCutoff4_le_one _ _ _
+
+theorem entryThreshold_pos (hθ : 0 < θ) : 0 < kind.entryThreshold θ := by
+  cases kind <;> dsimp only [entryThreshold] <;> positivity
+
+theorem gateThreshold_pos (hθ : 0 < θ) : 0 < kind.gateThreshold θ := by
+  cases kind <;> dsimp only [gateThreshold] <;> positivity
+
+theorem three_mul_gateThreshold_lt_entryThreshold (hθ : 0 < θ) :
+    3 * kind.gateThreshold θ < kind.entryThreshold θ := by
+  cases kind <;> dsimp only [gateThreshold, entryThreshold] <;> linarith
+
+theorem gateThreshold_lt_entryThreshold (hθ : 0 < θ) :
+    kind.gateThreshold θ < kind.entryThreshold θ := by
+  linarith [kind.gateThreshold_pos hθ, kind.three_mul_gateThreshold_lt_entryThreshold hθ]
+
+theorem scale_lt_gateThreshold (hθ : 0 < θ) (hη : η ≤ θ / 10000) :
+    η < kind.gateThreshold θ := by
+  cases kind <;> dsimp only [gateThreshold] <;> linarith
+
+theorem eval_eq_zero_of_entry_le (hθ : 0 < θ) (hv : v ≤ kind.entryThreshold θ) :
+    kind.eval θ v r = 0 := by
+  cases kind
+  · exact polynomialPrepRow4_eq_zero_of_entry_le hθ hv
+  · exact polynomialAuxCutoff4_eq_zero_of_entry_le hθ hv
+  · exact polynomialWitnessCutoff4_eq_zero_of_entry_le hθ hv
+
+theorem eval_eq_zero_of_rank_ge (hθ : 0 < θ) (hr : kind.gateThreshold θ ≤ r) :
+    kind.eval θ v r = 0 := by
+  cases kind
+  · exact polynomialPrepRow4_eq_zero_of_rank_ge hθ hr
+  · exact polynomialAuxCutoff4_eq_zero_of_rank_ge hθ hr
+  · exact polynomialWitnessCutoff4_eq_zero_of_rank_ge hθ hr
+
+/-- All three actual rank factors are constant throughout the common flat region. -/
+theorem eval_eq_of_rank_le (hθ : 0 < θ) (hη : η ≤ θ / 10000) (hr : r ≤ η) (hr' : r' ≤ η) :
+    kind.eval θ v r = kind.eval θ v r' := by
+  cases kind
+  · exact (polynomialPrepRow4_of_rank_le hθ (by linarith)).trans
+      (polynomialPrepRow4_of_rank_le hθ (by linarith)).symm
+  · exact (polynomialAuxCutoff4_of_rank_le hθ (by linarith)).trans
+      (polynomialAuxCutoff4_of_rank_le hθ (by linarith)).symm
+  · exact (polynomialWitnessCutoff4_of_rank_le hθ (by linarith)).trans
+      (polynomialWitnessCutoff4_of_rank_le hθ (by linarith)).symm
+
+theorem exists_abs_eval_root_sub_le (θ : ℝ) :
+    ∃ C : ℝ, 0 ≤ C ∧ ∀ v r v' r',
+      |kind.eval θ v r ^ (4⁻¹ : ℝ) - kind.eval θ v' r' ^ (4⁻¹ : ℝ)| ≤
+        C * (|v - v'| + |r - r'|) := by
+  cases kind
+  · exact exists_abs_polynomialPrepRow4_root_sub_le θ
+  · exact exists_abs_polynomialAuxCutoff4_root_sub_le θ
+  · exact exists_abs_polynomialWitnessCutoff4_root_sub_le θ
+
+variable {ι : Type*} {s : Finset ι} {K : ℕ} {z : ℝ} {w : ι → Fin 2 → ℝ}
+
+/-- Zero padding in the compression rank agrees with the existing atom rank, including when
+`K` exceeds the retained cardinality or the raw first coordinates are negative. -/
+theorem eval_firstRank_zero (θ v : ℝ) :
+    kind.eval θ v (firstRank s K 0 w) = kind.eval θ v (kthLargest K s fun y => w y 0) := by
+  rw [firstRank, max_eq_right kthLargest_nonneg]
+
+/-- The actual default entry always has zero output, with no sign restriction on the default. -/
+theorem eval_default_eq_zero (hθ : 0 < θ) :
+    kind.eval θ z (firstRank s K z w) = 0 := by
+  by_cases hz : z ≤ kind.entryThreshold θ
+  · exact kind.eval_eq_zero_of_entry_le hθ hz
+  exact kind.eval_eq_zero_of_rank_ge hθ
+    ((kind.gateThreshold_lt_entryThreshold hθ).le.trans
+      ((not_le.mp hz).le.trans default_le_firstRank))
+
+/-- Fewer than `K` retained endpoints have nonzero output for the actual padded rank. -/
+theorem card_filter_eval_ne_zero_lt (hθ : 0 < θ) (hK : 0 < K) :
+    #{y ∈ s | kind.eval θ (w y 0) (firstRank s K z w) ≠ 0} < K := by
+  classical
+  by_contra hlt
+  have hle : K ≤ #{y ∈ s | kind.eval θ (w y 0) (firstRank s K z w) ≠ 0} := not_lt.mp hlt
+  have hsub : ({y ∈ s | kind.eval θ (w y 0) (firstRank s K z w) ≠ 0} : Finset ι) ⊆
+      {y ∈ s | kind.entryThreshold θ < w y 0} := by
+    intro y hy
+    obtain ⟨hys, hy⟩ := mem_filter.mp hy
+    exact mem_filter.mpr ⟨hys, not_le.mp fun h => hy (kind.eval_eq_zero_of_entry_le hθ h)⟩
+  have hrank : kind.entryThreshold θ < kthLargest K s (fun y => w y 0) :=
+    (lt_kthLargest_iff hK (kind.entryThreshold_pos hθ).le).mpr (hle.trans (card_le_card hsub))
+  obtain ⟨y, hy⟩ := card_pos.mp (hK.trans_le hle)
+  exact (mem_filter.mp hy).2 (kind.eval_eq_zero_of_rank_ge hθ
+    ((kind.gateThreshold_lt_entryThreshold hθ).le.trans (hrank.le.trans kthLargest_le_firstRank)))
+
+variable {n : ℕ → ℕ} {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} {truth : ι → Fin 2 → ℝ}
+
+/-- The constructed stationary reference preserves each actual polynomial row output through
+the remaining compression schedule. Scalar support, gate, flatness, and margin laws are proved. -/
+theorem stationaryContinuation_eval_eq (hθ : 0 < θ) (hη : 0 ≤ η) (hmargin : η ≤ θ / 10000)
+    (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) (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
+    kind.eval θ (c.row y 0) (firstRank s K c.defaultValue c.row) =
+      kind.eval θ (b.row y 0) (firstRank s K b.defaultValue b.row) := by
+  exact stationaryContinuation_output_eq_dyadic (H := fun x _ q => kind.eval θ x q)
+    hη hK m j r hr hno hfirst hsecond hn (kind.scale_lt_gateThreshold hθ hmargin)
+    (kind.three_mul_gateThreshold_lt_entryThreshold hθ)
+    (fun _ _ _ hx => kind.eval_eq_zero_of_entry_le hθ hx)
+    (fun _ _ _ hq => kind.eval_eq_zero_of_rank_ge hθ hq)
+    (fun _ _ _ _ hq hq' => kind.eval_eq_of_rank_le hθ hmargin hq.2 hq'.2) y hy
+
+/-- A constant depending only on the concrete row function and its two scales bounds the
+continued reference's fourth-root error by actual prefix-error envelopes. No Lipschitz or
+support law is assumed; low-target endpoints need no relative-error hypothesis. -/
+theorem exists_stationaryContinuation_root_bound (hθ : 0 < θ) (hη : 0 < η)
+    (hmargin : η ≤ θ / 10000) :
+    ∃ C : ℝ, 0 ≤ C ∧ ∀ {ι : Type*} (s : Finset ι) (n : ℕ → ℕ) (Δ : ℕ → ι → Fin 2 → ℝ)
+      (a : State ι) (truth : ι → Fin 2 → ℝ) (K : ℕ),
+      0 < K → 0 ≤ a.defaultValue → a.defaultValue ≤ η / 2 →
+      ∀ (m j r : ℕ), j + r ≤ m →
+      (∀ i < j, stepThreshold s n (fun _ => K) (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i) →
+      (∀ y ∈ s, 0 ≤ truth y 0) → (∀ y ∈ s, |truth y 1| ≤ η / 2) →
+      (∀ i, j ≤ i → i < m → K ≤ n i) →
+      ∀ (ε : ℕ → ℝ), (∀ i < j, 0 ≤ ε i) →
+      (∀ i < j, ∀ y ∈ s, η / 2 ≤ truth y 0 →
+        clippedError (truth y 0) (truth y 1) (uncompressedRow Δ a.row (i + 1) y) ≤ ε i) →
+      ∀ y ∈ s,
+      let c := stationaryContinuation s n K (dyadicFloor η m) Δ a truth j r
+      |kind.eval θ (c.row y 0) (firstRank s K c.defaultValue c.row) ^ (4⁻¹ : ℝ) -
+          kind.eval θ (truth y 0) (firstRank s K 0 truth) ^ (4⁻¹ : ℝ)| ≤
+        C * ∑ i ∈ range j, dyadicFloor η m i * ε i := by
+  obtain ⟨L, hL, hroot⟩ := kind.exists_abs_eval_root_sub_le θ
+  refine ⟨3 * L * (12 * (1 + η / 2) / (η / 2)), by positivity, ?_⟩
+  intro ι s n Δ a truth K hK ha haη m j r hr hno hfirst hsecond hn ε hε herr y hy
+  have hentry : ∀ (x v q : ℝ), x ≤ η → (fun x (_ : ℝ) q => kind.eval θ x q) x v q = 0 := by
+    intro x _ q hx
+    exact kind.eval_eq_zero_of_entry_le hθ (hx.trans
+      ((kind.scale_lt_gateThreshold hθ hmargin).le.trans
+        (kind.gateThreshold_lt_entryThreshold hθ).le))
+  have hbound := abs_stationaryState_root_sub_le_weighted_dyadic
+    (H := fun x _ q => kind.eval θ x q) (p := (4⁻¹ : ℝ)) (C := L)
+    hη hK hL ha haη m j ((Nat.le_add_right j r).trans hr) hno hε herr hentry
+    (fun _ _ _ _ hq hq' => kind.eval_eq_of_rank_le hθ hmargin hq.2 hq'.2)
+    (fun x v q x' v' q' _ _ _ _ => (hroot x q x' q').trans
+      (mul_le_mul_of_nonneg_left (by linarith [abs_nonneg (v - v')]) hL)) y hy
+  dsimp only
+  rw [kind.stationaryContinuation_eval_eq hθ hη.le hmargin hK m j r hr hno hfirst hsecond hn y hy]
+  simpa only [mul_assoc] using hbound
+
+end PolynomialAtomRow
+end Cslib
+
+namespace Matrix
+
+open Finset
+
+variable {V : Type*}
+
+/-- The existing preparatory expression is the concrete polynomial preparation row. -/
+theorem atomPrep_polynomial_eq (θ : ℝ) (K : ℕ) (a : ℝ) (G : Matrix V V ℝ)
+    (T : Finset V) (x y : V) :
+    atomPrep (Cslib.polynomialPrepCutoff4 θ) (Cslib.polynomialRowCutoff4 θ) K a G T x y =
+      Cslib.PolynomialAtomRow.preparation.eval θ (G x y / a)
+        (kthLargest K T fun z => G x z / a) := rfl
+
+/-- The existing auxiliary-score expression is the concrete polynomial auxiliary row. -/
+theorem auxScore_polynomial_eq (θ : ℝ) (K : ℕ) (a : ℝ) (G : Matrix V V ℝ)
+    (T : Finset V) (x y : V) :
+    auxScore (Cslib.polynomialAuxCutoff4 θ) K a G T x y =
+      Cslib.PolynomialAtomRow.auxiliary.eval θ (G x y / a)
+        (kthLargest K T fun z => G x z / a) := rfl
+
+end Matrix
diff --git a/ComplexityTests/PolynomialAtomRows.lean b/ComplexityTests/PolynomialAtomRows.lean
new file mode 100644
index 000000000..d60379331
--- /dev/null
+++ b/ComplexityTests/PolynomialAtomRows.lean
@@ -0,0 +1,254 @@
+/-
+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.Probability.PolynomialAtomRows
+import Mathlib.LinearAlgebra.Matrix.Notation
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+
+/-!
+# Concrete polynomial stationary rows
+
+A nonzero first increment incurs actual preloss `1/2097152`. Adding it to a true low entry
+of `260` moves the witness rank strictly into its transition interval `(260,270)`. The true
+high-endpoint witness is one, while the reference witness lies strictly between zero and one.
+The remaining group raises the default and erases a second-coordinate value of `1/4`, yet
+preserves that nonzero witness. Its fourth-root error satisfies the new weighted bound.
+-/
+
+namespace ComplexityTests.PolynomialAtomRows
+
+open Finset Cslib Cslib.RowCompression
+
+private def initial : State (Fin 2) := { defaultValue := 0, row := ![![900, 0], ![0, 0]] }
+
+private noncomputable def truth : Fin 2 → Fin 2 → ℝ := ![![900, 0], ![260, 1 / 4]]
+
+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 → ℝ := ![![900, 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 := ![![900, 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 := ![![900, 0], ![260 + 1 / 2097152, 1 / 4]] } := by
+  unfold reference stationaryState
+  rw [actual_one, raw_one]
+  congr 1
+  funext y ν
+  fin_cases y <;> fin_cases ν <;> norm_num [truth, rawRow]
+
+example : increments 0 1 0 = 1 / 2097152 ∧
+    reference.row 1 0 - truth 1 0 = 1 / 2097152 := by
+  rw [reference_eq]
+  norm_num [increments, truth]
+
+private theorem reference_rank : firstRank univ 2 reference.defaultValue reference.row =
+    260 + 1 / 2097152 := by
+  have hle : kthLargest 2 univ (fun y => reference.row y 0) ≤ 260 + 1 / 2097152 := by
+    refine not_lt.mp fun hlt => ?_
+    have hc := (lt_kthLargest_iff (by norm_num)
+      (by norm_num : (0 : ℝ) ≤ 260 + 1 / 2097152)).mp hlt
+    have hs : ({y | (260 + 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 : (260 + 1 / 2097152 : ℝ) ≤ kthLargest 2 univ (fun y => reference.row y 0) := by
+    apply (le_kthLargest_iff (by norm_num) (by norm_num : (0 : ℝ) < 260 + 1 / 2097152)).mpr
+    have hs : ({y | (260 + 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 theorem true_rank : firstRank univ 2 0 truth = 260 := by
+  norm_num [firstRank, kthLargest, truth, Fin.univ_succ, filter_insert, filter_singleton]
+
+private noncomputable def output (a : State (Fin 2)) : ℝ :=
+  PolynomialAtomRow.witness.eval 10000 (a.row 0 0) (firstRank univ 2 a.defaultValue a.row)
+
+private theorem reference_output : output reference =
+    1 - polynomialSwitch4 260 270 (260 + 1 / 2097152) := by
+  unfold output
+  rw [reference_rank, reference_eq]
+  change polynomialWitnessCutoff4 10000 900 (260 + 1 / 2097152) = _
+  norm_num only [polynomialWitnessCutoff4]
+  rw [polynomialSwitch4_of_ge (by norm_num) le_rfl, one_mul]
+
+private theorem output_between : 0 < output reference ∧ output reference < 1 := by
+  rw [reference_output]
+  have h0 := polynomialSwitch4_nonneg 260 270 (260 + 1 / 2097152)
+  have h1 := polynomialSwitch4_le_one 260 270 (260 + 1 / 2097152)
+  have hn0 : polynomialSwitch4 (260 : ℝ) 270 (260 + 1 / 2097152) ≠ 0 := by
+    rw [ne_eq, polynomialSwitch4_eq_zero_iff (by norm_num)]
+    norm_num
+  have hn1 : polynomialSwitch4 (260 : ℝ) 270 (260 + 1 / 2097152) ≠ 1 := by
+    rw [ne_eq, polynomialSwitch4_eq_one_iff (by norm_num)]
+    norm_num
+  constructor
+  · by_contra hn
+    exact hn1 (by linarith)
+  · by_contra hn
+    exact hn0 (by linarith)
+
+private theorem true_output : PolynomialAtomRow.witness.eval 10000 (truth 0 0)
+    (firstRank univ 2 0 truth) = 1 := by
+  rw [true_rank]
+  exact polynomialWitnessCutoff4_eq_one (by norm_num) (by norm_num [truth]) (by norm_num)
+
+private noncomputable def continued : State (Fin 2) :=
+  stationaryContinuation univ (fun _ => 2) 2 (dyadicFloor 1 2) increments initial truth 1 1
+
+private theorem preserved : output continued = output reference := by
+  exact PolynomialAtomRow.witness.stationaryContinuation_eval_eq
+    (s := univ) (n := fun _ => 2) (Δ := increments) (a := initial) (truth := truth)
+    (θ := 10000) (η := 1) (by norm_num) (by norm_num) (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) 0 (mem_univ 0)
+
+-- The remaining group changes both the actual default and a row coordinate.
+example : reference.defaultValue < continued.defaultValue ∧
+    reference.row 1 1 = 1 / 4 ∧ continued.row 1 1 = 0 := by
+  have hc : continued = advance univ 2 2 (dyadicFloor 1 2 1) 0 reference := rfl
+  rw [hc, reference_eq]
+  norm_num [advance, update, newDefault, threshold, firstRank, kthLargest, entrySize,
+    dyadicFloor, dyadicSlack, Fin.univ_succ, filter_insert, filter_singleton,
+    updateEntry, radius, defaultEntry]
+
+-- The preserved output and its root discrepancy are both nonzero.
+example : 0 < output continued ∧
+    0 < |output continued ^ (4⁻¹ : ℝ) -
+      PolynomialAtomRow.witness.eval 10000 (truth 0 0) (firstRank univ 2 0 truth) ^ (4⁻¹ : ℝ)| := by
+  rw [preserved, true_output, Real.one_rpow]
+  refine ⟨output_between.1, abs_pos.mpr ?_⟩
+  exact sub_ne_zero.mpr (ne_of_lt (Real.rpow_lt_one output_between.1.le output_between.2
+    (by norm_num)))
+
+-- Apply the theorem to a valid raw-prefix error envelope, with no scalar-law premises.
+example : ∃ C : ℝ, 0 ≤ C ∧
+    |output continued ^ (4⁻¹ : ℝ) - 1| ≤ C / 1048576 := by
+  obtain ⟨C, hC, hbound⟩ := PolynomialAtomRow.witness.exists_stationaryContinuation_root_bound
+    (θ := 10000) (η := 1) (by norm_num) (by norm_num) (by norm_num)
+  refine ⟨C, hC, ?_⟩
+  have h := hbound univ (fun _ => 2) increments initial truth 2 (by norm_num)
+    (by norm_num [initial]) (by norm_num [initial]) 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)
+    (fun _ => 1) (by intros; norm_num) (fun _ _ _ _ _ => clippedError_le_one _ _ _)
+    0 (mem_univ 0)
+  change |output continued ^ (4⁻¹ : ℝ) -
+    PolynomialAtomRow.witness.eval 10000 (truth 0 0)
+      (firstRank univ 2 0 truth) ^ (4⁻¹ : ℝ)| ≤ _ at h
+  simpa only [true_output, Real.one_rpow, sum_range_succ, sum_range_zero, zero_add, mul_one,
+    floor_zero, div_eq_mul_inv, one_mul] using h
+
+-- The actual retained output has strict capacity, and a positive default still emits zero.
+example : #{y ∈ (univ : Finset (Fin 2)) | PolynomialAtomRow.witness.eval 10000
+    (reference.row y 0) (firstRank univ 2 reference.defaultValue reference.row) ≠ 0} < 2 :=
+  PolynomialAtomRow.witness.card_filter_eval_ne_zero_lt (by norm_num) (by norm_num)
+
+example : PolynomialAtomRow.witness.eval 10000 reference.defaultValue
+    (firstRank univ 2 reference.defaultValue reference.row) = 0 :=
+  PolynomialAtomRow.witness.eval_default_eq_zero (by norm_num)
+
+-- When K exceeds the retained cardinality, positive dummy padding still affects the output.
+-- The second raw coordinate is negative; it is not an input to this pre-incoming function.
+example :
+    let w : Unit → Fin 2 → ℝ := fun _ => ![900, -7]
+    PolynomialAtomRow.witness.eval 10000 900 (firstRank univ 2 265 w) = 1 / 2 ∧
+      PolynomialAtomRow.witness.eval 10000 900 (firstRank univ 2 0 w) = 1 := by
+  norm_num [PolynomialAtomRow.eval, firstRank, kthLargest, polynomialWitnessCutoff4,
+    polynomialSwitch4, polynomialTransition4, transitionPolynomial4]
+
+-- Both bridges expose the polynomial row functions in the existing atom API.
+example (G : Matrix (Fin 2) (Fin 2) ℝ) (x y : Fin 2) :
+    Matrix.atomPrep (polynomialPrepCutoff4 10000) (polynomialRowCutoff4 10000) 2 1 G univ x y =
+      PolynomialAtomRow.preparation.eval 10000 (G x y)
+        (firstRank univ 2 0 fun z _ => G x z) := by
+  rw [Matrix.atomPrep_polynomial_eq, PolynomialAtomRow.eval_firstRank_zero]
+  simp only [div_one]
+
+example (G : Matrix (Fin 2) (Fin 2) ℝ) (x y : Fin 2) :
+    Matrix.auxScore (polynomialAuxCutoff4 10000) 2 1 G univ x y =
+      PolynomialAtomRow.auxiliary.eval 10000 (G x y)
+        (firstRank univ 2 0 fun z _ => G x z) := by
+  rw [Matrix.auxScore_polynomial_eq, PolynomialAtomRow.eval_firstRank_zero]
+  simp only [div_one]
+
+end ComplexityTests.PolynomialAtomRows