diff --git a/Complexity.lean b/Complexity.lean
index 4ec2d31ed..c21e7baad 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2873,6 +2873,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.PolynomialAtomFalseOverflow
 public import Complexity.Foundations.Probability.PolynomialAtomRows
 public import Complexity.Foundations.Probability.ProductError
 public import Complexity.Foundations.Probability.RootMetric
diff --git a/Complexity/Foundations/Probability/PolynomialAtomFalseOverflow.lean b/Complexity/Foundations/Probability/PolynomialAtomFalseOverflow.lean
new file mode 100644
index 000000000..e49cb3ee8
--- /dev/null
+++ b/Complexity/Foundations/Probability/PolynomialAtomFalseOverflow.lean
@@ -0,0 +1,269 @@
+/-
+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.PolynomialAtomRows
+public import Complexity.Foundations.Probability.HeavyCount
+public import Complexity.Foundations.Probability.RootMetric
+public import Complexity.Foundations.Analysis.RowCompression.FalseOverflow
+import Mathlib.Algebra.Order.BigOperators.Expect
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
+
+/-!
+# Actual polynomial row errors on false first overflows
+
+The computed and true polynomial row outputs are in `[0,1]`, and each has fewer than `K`
+retained nonzero entries. Their fourth-root discrepancy therefore has summed fourth power
+at most `2 * K`, independently of the row width, default, and later compression states.
+At a false first overflow, the existing actual-prefix charge pays for this bounded error.
+
+The resulting normalized bound uses the final state of the real compression recursion and
+the raw prefix at `j + 1`. The environment may jointly determine the increments, initial
+states, true rows, retained endpoints, and first overflow. No independence is assumed.
+
+This is the bounded-output integration of `buf-false-charge` in the proof of
+[OpenAI2026LogSpace, Section 8.4, Proposition 8.5], on the fourth-moment route of issue #1721.
+It does not supply prefix mean/noise budgets, sum their geometric costs, prove post-overflow
+relative stability, or assert the complete integrated compression estimate.
+
+## Main definitions
+
+* `Cslib.PolynomialAtomRow.stateRootError`: the actual fourth-root output discrepancy, using
+  both states' padded ranks and defaults.
+
+## Main results
+
+* `Cslib.PolynomialAtomRow.sum_stateRootError_pow_four_le`: a width-independent support bound.
+* `Cslib.PolynomialAtomRow.rowNormPow_falseFirstOverflow_le`: the normalized false-overflow
+  output charge at a specified group.
+* `Cslib.PolynomialAtomRow.rowNormPow_falseFirstOverflowBefore_le`: the finite union over
+  possible first-overflow groups, with no additional factor from their number.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 8.4, equations labelled `buf-false-charge` and `buf-false-sum`
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+namespace Cslib.PolynomialAtomRow
+
+open Finset RowCompression Probability
+open scoped BigOperators
+
+variable {ι : Type*} (kind : PolynomialAtomRow)
+
+/-- The actual fourth-root discrepancy of two row states, with their own padded ranks. -/
+@[expose] noncomputable def stateRootError (θ : ℝ) (S : Finset ι) (K : ℕ)
+    (a b : State ι) (y : ι) : ℝ :=
+  kind.eval θ (a.row y 0) (firstRank S K a.defaultValue a.row) ^ (4⁻¹ : ℝ) -
+    kind.eval θ (b.row y 0) (firstRank S K b.defaultValue b.row) ^ (4⁻¹ : ℝ)
+
+/-- Both actual output roots lie in `[0,1]`, for every input row and default. -/
+theorem abs_stateRootError_le_one (θ : ℝ) (S : Finset ι) (K : ℕ)
+    (a b : State ι) (y : ι) : |kind.stateRootError θ S K a b y| ≤ 1 := by
+  have ha0 := Real.rpow_nonneg (kind.eval_nonneg θ (a.row y 0)
+    (firstRank S K a.defaultValue a.row)) (4⁻¹ : ℝ)
+  have hb0 := Real.rpow_nonneg (kind.eval_nonneg θ (b.row y 0)
+    (firstRank S K b.defaultValue b.row)) (4⁻¹ : ℝ)
+  have ha1 := Real.rpow_le_one (kind.eval_nonneg θ (a.row y 0) _)
+    (kind.eval_le_one θ (a.row y 0) (firstRank S K a.defaultValue a.row))
+    (by norm_num : (0 : ℝ) ≤ 4⁻¹)
+  have hb1 := Real.rpow_le_one (kind.eval_nonneg θ (b.row y 0) _)
+    (kind.eval_le_one θ (b.row y 0) (firstRank S K b.defaultValue b.row))
+    (by norm_num : (0 : ℝ) ≤ 4⁻¹)
+  unfold stateRootError
+  apply abs_sub_le_iff.mpr
+  constructor <;> linarith
+
+/-- The discrepancy is supported on the union of the two actual supports. Neither the
+ambient cardinality nor a bound on the row entries occurs in its fourth-power sum. -/
+theorem sum_stateRootError_pow_four_le {θ : ℝ} (hθ : 0 < θ) (S : Finset ι) {K : ℕ}
+    (hK : 0 < K) (a b : State ι) :
+    ∑ y ∈ S, |kind.stateRootError θ S K a b y| ^ 4 ≤ 2 * (K : ℝ) := by
+  classical
+  let A := {y ∈ S | kind.eval θ (a.row y 0) (firstRank S K a.defaultValue a.row) ≠ 0}
+  let B := {y ∈ S | kind.eval θ (b.row y 0) (firstRank S K b.defaultValue b.row) ≠ 0}
+  let D := {y ∈ S | kind.stateRootError θ S K a b y ≠ 0}
+  have hsub : D ⊆ A ∪ B := by
+    intro y hy
+    obtain ⟨hyS, hy⟩ := mem_filter.mp hy
+    by_cases ha : kind.eval θ (a.row y 0) (firstRank S K a.defaultValue a.row) = 0
+    · apply mem_union_right
+      refine mem_filter.mpr ⟨hyS, fun hb => hy ?_⟩
+      simp [stateRootError, ha, hb]
+    · exact mem_union_left _ (mem_filter.mpr ⟨hyS, ha⟩)
+  have hcard : #D ≤ 2 * K := by
+    have hA : #A < K := kind.card_filter_eval_ne_zero_lt hθ hK
+    have hB : #B < K := kind.card_filter_eval_ne_zero_lt hθ hK
+    have h := (card_le_card hsub).trans (card_union_le A B)
+    omega
+  rw [← sum_filter_of_ne (p := fun y => kind.stateRootError θ S K a b y ≠ 0)
+    fun y _ h hy => h (by rw [hy, abs_zero, zero_pow (by decide)])]
+  calc
+    _ ≤ ∑ _y ∈ D, (1 : ℝ) := by
+      refine sum_le_sum fun y _ => ?_
+      simpa using pow_le_pow_left₀ (abs_nonneg (kind.stateRootError θ S K a b y))
+        (kind.abs_stateRootError_le_one θ S K a b y) 4
+    _ = (#D : ℝ) := by simp
+    _ ≤ 2 * (K : ℝ) := by exact_mod_cast hcard
+
+private theorem sum_stateRootError_pow_four_le_of_false {θ η : ℝ} (hθ : 0 < θ)
+    {S : Finset ι} {n : ℕ → ℕ} {K : ℕ} (hK : 0 < K)
+    {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} {truth : ι → Fin 2 → ℝ}
+    (hη : 0 < η) (hη1 : η ≤ 1) (ha : a.defaultValue = 0)
+    (m j : ℕ) (hj : j < m) (hn : 0 < n j)
+    (hover : IsFirstOverflow S n (fun _ => K) (dyadicFloor η m) Δ a j)
+    (hfirst : ∀ y ∈ S, 0 ≤ truth y 0)
+    (hsecond : ∀ y ∈ S, truth y 0 ≤ dyadicFloor η m j / 4 → truth y 1 = 0)
+    (hheavy : 2 * #{y ∈ S | dyadicFloor η m j / 4 < truth y 0} < n j)
+    (b : State ι) :
+    ∑ y ∈ S, |kind.stateRootError θ S K b ⟨0, truth⟩ y| ^ 4 ≤
+      (64 * (K : ℝ) / ((n j : ℝ) * dyadicFloor η m j ^ 4)) *
+        ∑ y ∈ S, |clippedError (truth y 0) (truth y 1)
+          (uncompressedRow Δ a.row (j + 1) y)| ^ 4 := by
+  have hcharge := one_le_sum_clippedError_pow_of_firstOverflow_dyadic hη hη1 ha
+    m j hj hn hover hfirst hsecond hheavy 4
+  have he (y : ι) : |clippedError (truth y 0) (truth y 1)
+      (uncompressedRow Δ a.row (j + 1) y)| =
+      clippedError (truth y 0) (truth y 1) (uncompressedRow Δ a.row (j + 1) y) :=
+    abs_of_nonneg (clippedError_nonneg _ _ _)
+  calc
+    _ ≤ 2 * (K : ℝ) := kind.sum_stateRootError_pow_four_le hθ S hK _ _
+    _ = (2 * (K : ℝ)) * 1 := by ring
+    _ ≤ (2 * (K : ℝ)) * ((2 : ℝ) ^ (4 + 1) /
+        ((n j : ℝ) * dyadicFloor η m j ^ 4) *
+          ∑ y ∈ S, clippedError (truth y 0) (truth y 1)
+            (uncompressedRow Δ a.row (j + 1) y) ^ 4) :=
+      mul_le_mul_of_nonneg_left hcharge (by positivity)
+    _ = _ := by simp only [he]; norm_num; ring
+
+variable {Ω V : Type*} [Fintype Ω] [Fintype V]
+
+open Classical in
+/-- The final actual polynomial outputs on a specified false-first-overflow event are paid
+for by the raw-prefix moment at `j + 1`. Every random quantity may share the environment. -/
+theorem rowNormPow_falseFirstOverflow_le {θ η N u : ℝ} (hθ : 0 < θ)
+    (hη : 0 < η) (hη1 : η ≤ 1) (hNu : 0 ≤ N * u)
+    (X Y : Ω → V → Prop) [∀ σ x, Decidable (X σ x)] [∀ σ y, Decidable (Y σ y)]
+    (n : ℕ → ℕ) (K : ℕ) (hK : 0 < K) (m j : ℕ) (hj : j < m) (hn : 0 < n j)
+    (Δ : Ω → V → ℕ → V → Fin 2 → ℝ) (a : Ω → V → State V)
+    (truth : Ω → V → V → Fin 2 → ℝ)
+    (ha : ∀ σ x, X σ x → (a σ x).defaultValue = 0)
+    (hfirst : ∀ σ x y, X σ x → Y σ y → 0 ≤ truth σ x y 0)
+    (hsecond : ∀ σ x y, X σ x → Y σ y →
+      truth σ x y 0 ≤ dyadicFloor η m j / 4 → truth σ x y 1 = 0) :
+    let S := fun σ => ({y | Y σ y} : Finset V)
+    let b := fun σ x => iterate (S σ) n (fun _ => K) (dyadicFloor η m) (Δ σ x) (a σ x) m
+    let F := fun σ x => IsFirstOverflow (S σ) n (fun _ => K)
+      (dyadicFloor η m) (Δ σ x) (a σ x) j ∧
+        ¬ heavyCountEvent Y univ (fun y => truth σ x y 0) (dyadicFloor η m j) (n j) σ
+    rowNormPow 4 N u X Y (fun σ x y =>
+      if F σ x then kind.stateRootError θ (S σ) K (b σ x) ⟨0, truth σ x⟩ y else 0) ≤
+      (64 * (K : ℝ) / ((n j : ℝ) * dyadicFloor η m j ^ 4)) *
+        rowNormPow 4 N u X Y (fun σ x y => clippedError (truth σ x y 0) (truth σ x y 1)
+          (uncompressedRow (Δ σ x) (a σ x).row (j + 1) y)) := by
+  classical
+  dsimp only
+  unfold rowNormPow
+  have hc : 0 ≤ 64 * (K : ℝ) / ((n j : ℝ) * dyadicFloor η m j ^ 4) := by positivity
+  calc
+    _ ≤ (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V),
+        (64 * (K : ℝ) / ((n j : ℝ) * dyadicFloor η m j ^ 4)) *
+          ∑ y ∈ ({y | Y σ y} : Finset V),
+            |clippedError (truth σ x y 0) (truth σ x y 1)
+              (uncompressedRow (Δ σ x) (a σ x).row (j + 1) y)| ^ 4 := by
+      refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (inv_nonneg.mpr hNu)
+      refine sum_le_sum fun x hx => ?_
+      have hx' := (mem_filter.mp hx).2
+      dsimp only
+      split_ifs with hF
+      · apply kind.sum_stateRootError_pow_four_le_of_false hθ hK hη hη1 (ha σ x hx')
+          m j hj hn hF.1
+        · intro y hy
+          exact hfirst σ x y hx' (mem_filter.mp hy).2
+        · intro y hy
+          exact hsecond σ x y hx' (mem_filter.mp hy).2
+        · simpa only [heavyCountEvent, filter_filter] using Nat.lt_of_not_ge hF.2
+      · simp only [abs_zero, zero_pow (by decide : (4 : ℕ) ≠ 0), sum_const_zero]
+        exact mul_nonneg hc (sum_nonneg fun _ _ => by positivity)
+    _ = _ := by simp only [← mul_sum, ← mul_expect]; ring
+
+open Classical in
+/-- **The false-type contribution to actual final output error.** Taking the union of the
+possible false first overflows gives the sum of their raw-prefix charges. Both sides use the
+same `RootMetric` normalization, and no independence or final-output error premise is required. -/
+theorem rowNormPow_falseFirstOverflowBefore_le {θ η N u : ℝ} (hθ : 0 < θ)
+    (hη : 0 < η) (hη1 : η ≤ 1) (hNu : 0 ≤ N * u)
+    (X Y : Ω → V → Prop) [∀ σ x, Decidable (X σ x)] [∀ σ y, Decidable (Y σ y)]
+    (n : ℕ → ℕ) (K : ℕ) (hK : 0 < K) (m : ℕ) (hn : ∀ j < m, 0 < n j)
+    (Δ : Ω → V → ℕ → V → Fin 2 → ℝ) (a : Ω → V → State V)
+    (truth : Ω → V → V → Fin 2 → ℝ)
+    (ha : ∀ σ x, X σ x → (a σ x).defaultValue = 0)
+    (hfirst : ∀ σ x y, X σ x → Y σ y → 0 ≤ truth σ x y 0)
+    (hsecond : ∀ j < m, ∀ σ x y, X σ x → Y σ y →
+      truth σ x y 0 ≤ dyadicFloor η m j / 4 → truth σ x y 1 = 0) :
+    let S := fun σ => ({y | Y σ y} : Finset V)
+    let b := fun σ x => iterate (S σ) n (fun _ => K) (dyadicFloor η m) (Δ σ x) (a σ x) m
+    let F := fun j σ x => IsFirstOverflow (S σ) n (fun _ => K)
+      (dyadicFloor η m) (Δ σ x) (a σ x) j ∧
+        ¬ heavyCountEvent Y univ (fun y => truth σ x y 0) (dyadicFloor η m j) (n j) σ
+    rowNormPow 4 N u X Y (fun σ x y =>
+      if ∃ j < m, F j σ x then kind.stateRootError θ (S σ) K (b σ x) ⟨0, truth σ x⟩ y else 0) ≤
+      ∑ j ∈ range m, (64 * (K : ℝ) / ((n j : ℝ) * dyadicFloor η m j ^ 4)) *
+        rowNormPow 4 N u X Y (fun σ x y => clippedError (truth σ x y 0) (truth σ x y 1)
+          (uncompressedRow (Δ σ x) (a σ x).row (j + 1) y)) := by
+  classical
+  let S := fun σ => ({y | Y σ y} : Finset V)
+  let b := fun σ x => iterate (S σ) n (fun _ => K) (dyadicFloor η m) (Δ σ x) (a σ x) m
+  let F := fun j σ x => IsFirstOverflow (S σ) n (fun _ => K)
+    (dyadicFloor η m) (Δ σ x) (a σ x) j ∧
+      ¬ heavyCountEvent Y univ (fun y => truth σ x y 0) (dyadicFloor η m j) (n j) σ
+  let D := fun σ x y => kind.stateRootError θ (S σ) K (b σ x) ⟨0, truth σ x⟩ y
+  change rowNormPow 4 N u X Y (fun σ x y => if ∃ j < m, F j σ x then D σ x y else 0) ≤ _
+  have hgroup (j : ℕ) (hj : j ∈ range m) :
+      rowNormPow 4 N u X Y (fun σ x y => if F j σ x then D σ x y else 0) ≤
+        (64 * (K : ℝ) / ((n j : ℝ) * dyadicFloor η m j ^ 4)) *
+          rowNormPow 4 N u X Y (fun σ x y => clippedError (truth σ x y 0) (truth σ x y 1)
+            (uncompressedRow (Δ σ x) (a σ x).row (j + 1) y)) :=
+    kind.rowNormPow_falseFirstOverflow_le hθ hη hη1 hNu X Y n K hK m j
+      (mem_range.mp hj) (hn j (mem_range.mp hj)) Δ a truth ha hfirst (hsecond j (mem_range.mp hj))
+  refine le_trans ?_ (sum_le_sum hgroup)
+  have hpoint (σ : Ω) (x y : V) :
+      |if ∃ j < m, F j σ x then D σ x y else 0| ^ 4 ≤
+        ∑ j ∈ range m, |if F j σ x then D σ x y else 0| ^ 4 := by
+    by_cases hF : ∃ j < m, F j σ x
+    · obtain ⟨j, hj, hjF⟩ := hF
+      have hsome : ∃ i < m, F i σ x := ⟨j, hj, hjF⟩
+      have hsingle := single_le_sum (s := range m)
+        (f := fun i => |if F i σ x then D σ x y else 0| ^ 4)
+        (fun _ _ => by positivity) (mem_range.mpr hj)
+      simpa only [hsome, hjF, ↓reduceIte] using hsingle
+    · simp only [hF, ↓reduceIte, abs_zero, zero_pow (by decide : (4 : ℕ) ≠ 0)]
+      exact sum_nonneg fun _ _ => by positivity
+  have hswap (σ : Ω) :
+      (∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V),
+        ∑ j ∈ range m, |if F j σ x then D σ x y else 0| ^ 4) =
+      ∑ j ∈ range m, ∑ x ∈ ({x | X σ x} : Finset V),
+        ∑ y ∈ ({y | Y σ y} : Finset V), |if F j σ x then D σ x y else 0| ^ 4 := by
+    simp_rw [sum_comm (s := ({y | Y σ y} : Finset V)) (t := range m)]
+    rw [sum_comm]
+  unfold rowNormPow
+  calc
+    _ ≤ (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V),
+        ∑ y ∈ ({y | Y σ y} : Finset V), ∑ j ∈ range m,
+          |if F j σ x then D σ x y else 0| ^ 4 := by
+      refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (inv_nonneg.mpr hNu)
+      exact sum_le_sum fun x _ => sum_le_sum fun y _ => hpoint σ x y
+    _ = _ := by simp only [hswap, expect_sum_comm, mul_sum]
+
+end Cslib.PolynomialAtomRow
diff --git a/ComplexityTests/PolynomialAtomFalseOverflow.lean b/ComplexityTests/PolynomialAtomFalseOverflow.lean
new file mode 100644
index 000000000..c67e36bdd
--- /dev/null
+++ b/ComplexityTests/PolynomialAtomFalseOverflow.lean
@@ -0,0 +1,246 @@
+/-
+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.PolynomialAtomFalseOverflow
+import Mathlib.LinearAlgebra.Matrix.Notation
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum
+
+/-!
+# Actual polynomial output error on a false first overflow
+
+The same Boolean environment controls retention and the signed increments. On `true`, the
+real compression update raises the default to `1/8192` and erases a negative second channel.
+Both true targets are zero, so its first overflow is false. Its final preparation output is
+one at the first endpoint, while the true output is zero. The masked fourth moment is exactly
+`1/2`; the normalized single-group and finite-union bounds apply to that nonzero error.
+-/
+
+namespace ComplexityTests.PolynomialAtomFalseOverflow
+
+open Finset Cslib Cslib.RowCompression Cslib.Probability
+open scoped BigOperators
+
+private def source (_σ : Bool) (x : Fin 2) : Prop := x = 0
+
+private def retained (σ : Bool) (y : Fin 2) : Prop := σ = true ∨ y = 0
+
+private instance (σ : Bool) (x : Fin 2) : Decidable (source σ x) :=
+  inferInstanceAs (Decidable (x = 0))
+
+private instance (σ : Bool) (y : Fin 2) : Decidable (retained σ y) :=
+  inferInstanceAs (Decidable (σ = true ∨ y = 0))
+
+private theorem source_set (σ : Bool) : ({x | source σ x} : Finset (Fin 2)) = {0} := by
+  change (univ.filter fun x : Fin 2 => x = 0) = {0}
+  decide
+
+private theorem retained_true : ({y | retained true y} : Finset (Fin 2)) = univ := by
+  ext y
+  simp [retained]
+
+private theorem retained_false : ({y | retained false y} : Finset (Fin 2)) = {0} := by
+  ext y
+  simp [retained]
+
+private def initial : State (Fin 2) := { defaultValue := 0, row := 0 }
+
+private noncomputable def incoming : Fin 2 → Fin 2 → ℝ :=
+  ![![1, 0], ![1 / 8192, -1 / 16384]]
+
+private noncomputable def increments (σ : Bool) (_x : Fin 2) (i : ℕ) : Fin 2 → Fin 2 → ℝ :=
+  if σ = true ∧ i = 0 then incoming else 0
+
+private noncomputable def actual (σ : Bool) (x : Fin 2) : State (Fin 2) :=
+  iterate {y | retained σ y} (fun _ => 2) (fun _ => 2) (dyadicFloor (1 / 16) 1)
+    (increments σ x) initial 1
+
+private theorem rank_two (v : Fin 2 → ℝ) (h0 : v 0 = 1) (h1 : v 1 = 1 / 8192) :
+    kthLargest 2 univ v = 1 / 8192 := by
+  apply le_antisymm
+  · refine not_lt.mp fun hlt => ?_
+    have hc := (lt_kthLargest_iff (by norm_num)
+      (by norm_num : (0 : ℝ) ≤ 1 / 8192)).mp hlt
+    have hs : ({y | (1 / 8192 : ℝ) < 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 / 8192)).mpr
+    have hs : ({y | (1 / 8192 : ℝ) ≤ v y} : Finset (Fin 2)) = univ := by
+      ext y
+      fin_cases y <;> norm_num [h0, h1]
+    rw [hs]
+    norm_num
+
+private theorem incoming_threshold :
+    threshold univ 2 (dyadicFloor (1 / 16) 1 0) 0 incoming = 1 / 8192 := by
+  unfold threshold
+  rw [rank_two (fun y => entrySize (incoming y)) (by norm_num [incoming, entrySize])
+    (by norm_num [incoming, entrySize])]
+  norm_num [dyadicFloor, dyadicSlack]
+
+private theorem incoming_default :
+    newDefault univ 2 2 (dyadicFloor (1 / 16) 1 0) 0 incoming = 1 / 8192 := by
+  unfold newDefault
+  rw [incoming_threshold, rank_two (fun y => incoming y 0) (by norm_num [incoming])
+    (by norm_num [incoming])]
+  norm_num
+
+private theorem actual_true (x : Fin 2) : actual true x =
+    { defaultValue := 1 / 8192, row := ![![1, 0], ![1 / 8192, 0]] } := by
+  unfold actual
+  rw [retained_true]
+  have hin : initial.row + increments true x 0 = incoming := by simp [initial, increments]
+  change advance univ 2 2 (dyadicFloor (1 / 16) 1 0) (increments true x 0) initial = _
+  unfold advance
+  rw [hin]
+  change State.mk (newDefault univ 2 2 (dyadicFloor (1 / 16) 1 0) 0 incoming)
+    (update univ 2 2 (dyadicFloor (1 / 16) 1 0) 0 incoming) = _
+  rw [incoming_default]
+  congr 1
+  unfold update
+  rw [incoming_threshold, incoming_default]
+  funext y ν
+  fin_cases y <;> fin_cases ν <;>
+    norm_num [updateEntry, radius, entrySize, defaultEntry, incoming]
+
+private def falseEvent (σ : Bool) (x : Fin 2) : Prop :=
+  IsFirstOverflow {y | retained σ y} (fun _ => 2) (fun _ => 2)
+      (dyadicFloor (1 / 16) 1) (increments σ x) initial 0 ∧
+    ¬ heavyCountEvent retained univ (fun _ => 0) (dyadicFloor (1 / 16) 1 0) 2 σ
+
+private theorem falseEvent_iff (σ : Bool) (x : Fin 2) : falseEvent σ x ↔ σ = true := by
+  cases σ
+  · unfold falseEvent
+    rw [retained_false]
+    norm_num [IsFirstOverflow, stepThreshold, inputRow, initial, increments,
+      dyadicFloor, dyadicSlack, threshold, kthLargest, entrySize]
+  · unfold falseEvent
+    rw [retained_true]
+    have hin : inputRow univ (fun _ => 2) (fun _ => 2) (dyadicFloor (1 / 16) 1)
+        (increments true x) initial 0 = incoming := by simp [inputRow, initial, increments]
+    have ht : stepThreshold univ (fun _ => 2) (fun _ => 2) (dyadicFloor (1 / 16) 1)
+        (increments true x) initial 0 = 1 / 8192 := by
+      unfold stepThreshold
+      rw [hin]
+      exact incoming_threshold
+    norm_num [IsFirstOverflow, ht, heavyCountEvent, dyadicFloor, dyadicSlack]
+
+-- Both the actual compression change and the false-overflow classification are nontrivial.
+example (x : Fin 2) : falseEvent true x ∧ ¬ falseEvent false x ∧
+    (actual true x).defaultValue = 1 / 8192 ∧
+    uncompressedRow (increments true x) initial.row 1 1 1 = -1 / 16384 ∧
+    (actual true x).row 1 1 = 0 := by
+  rw [actual_true]
+  norm_num [falseEvent_iff, uncompressedRow, increments, incoming, initial]
+
+private theorem actual_rank (x : Fin 2) :
+    firstRank univ 2 (actual true x).defaultValue (actual true x).row = 1 / 8192 := by
+  rw [actual_true]
+  unfold firstRank
+  rw [rank_two (fun y => (![![1, 0], ![1 / 8192, 0]] : Fin 2 → Fin 2 → ℝ) y 0)
+    (by norm_num) (by norm_num)]
+  norm_num
+
+private theorem actual_error_true (x y : Fin 2) :
+    PolynomialAtomRow.preparation.stateRootError 1 univ 2 (actual true x) ⟨0, 0⟩ y =
+      if y = 0 then 1 else 0 := by
+  unfold PolynomialAtomRow.stateRootError
+  rw [actual_rank, actual_true]
+  have htrue : PolynomialAtomRow.preparation.eval 1 0
+      (firstRank (univ : Finset (Fin 2)) 2 0 0) = 0 :=
+    polynomialPrepRow4_eq_zero_of_entry_le (by norm_num) (by norm_num)
+  simp only [Pi.zero_apply, htrue, Real.zero_rpow (by norm_num : (4⁻¹ : ℝ) ≠ 0), sub_zero]
+  change polynomialPrepRow4 1 _ (1 / 8192) ^ (4⁻¹ : ℝ) = _
+  rw [polynomialPrepRow4_of_rank_le (by norm_num) (by norm_num)]
+  fin_cases y
+  · rw [polynomialPrepCutoff4_eq_one (by norm_num) (by norm_num)]
+    norm_num
+  · rw [polynomialPrepCutoff4_eq_zero (by norm_num) (by norm_num)]
+    norm_num
+
+open Classical in
+private noncomputable def maskedError (σ : Bool) (x y : Fin 2) : ℝ :=
+  if falseEvent σ x then PolynomialAtomRow.preparation.stateRootError 1 {y | retained σ y}
+    2 (actual σ x) ⟨0, 0⟩ y else 0
+
+private theorem maskedError_eq (σ : Bool) (x y : Fin 2) :
+    maskedError σ x y = if σ = true ∧ y = 0 then 1 else 0 := by
+  cases σ <;> simp [maskedError, falseEvent_iff, retained, actual_error_true]
+
+-- The exact normalized output moment is positive; it is not an empty-mask application.
+example : rowNormPow 4 1 1 source retained maskedError = 1 / 2 := by
+  norm_num [rowNormPow, source_set, retained, maskedError_eq, expect_eq_sum_div_card,
+    sum_filter, Fintype.sum_bool, Fin.sum_univ_two]
+
+private noncomputable def prefixError (σ : Bool) (x y : Fin 2) : ℝ :=
+  clippedError 0 0 (uncompressedRow (increments σ x) initial.row 1 y)
+
+-- Apply the specified-group theorem with every truth, default, and floor hypothesis discharged.
+example : rowNormPow 4 1 1 source retained maskedError ≤
+    (64 * 2 / (2 * dyadicFloor (1 / 16) 1 0 ^ 4)) *
+      rowNormPow 4 1 1 source retained prefixError := by
+  have h := PolynomialAtomRow.preparation.rowNormPow_falseFirstOverflow_le
+      (θ := 1) (η := 1 / 16) (N := 1) (u := 1)
+      (by norm_num) (by norm_num) (by norm_num) (by norm_num)
+      source retained (fun _ => 2) 2 (by norm_num) 1 0 (by norm_num) (by norm_num)
+      increments (fun _ _ => initial) (fun _ _ _ => 0)
+      (by intros; rfl) (by intros; exact le_rfl) (by intros; rfl)
+  dsimp only at h
+  convert h using 1
+  · congr 1
+    funext σ x y
+    simp only [maskedError, falseEvent, actual, Pi.zero_apply, Pi.zero_def]
+    congr 1
+  · rfl
+
+-- The raw error moment is measured before the negative second channel is erased.
+example : rowNormPow 4 1 1 source retained prefixError = (1 + (1 / 8192 : ℝ) ^ 4) / 2 := by
+  norm_num [rowNormPow, source_set, retained, prefixError, uncompressedRow, increments, incoming,
+    initial, clippedError, expect_eq_sum_div_card, sum_filter, Fintype.sum_bool, Fin.sum_univ_two]
+
+-- The union theorem gives the same normalization, with the actual prefix at `j + 1`.
+open Classical in
+example :
+    rowNormPow 4 1 1 source retained (fun σ x y =>
+      if ∃ j < 1,
+        IsFirstOverflow {y | retained σ y} (fun _ => 2) (fun _ => 2)
+            (dyadicFloor (1 / 16) 1) (increments σ x) initial j ∧
+          ¬ heavyCountEvent retained univ (fun _ => 0) (dyadicFloor (1 / 16) 1 j) 2 σ
+      then PolynomialAtomRow.preparation.stateRootError 1 {y | retained σ y}
+        2 (actual σ x) ⟨0, 0⟩ y else 0) ≤
+      ∑ j ∈ range 1, (64 * 2 / (2 * dyadicFloor (1 / 16) 1 j ^ 4)) *
+        rowNormPow 4 1 1 source retained (fun σ x y =>
+          clippedError 0 0 (uncompressedRow (increments σ x) initial.row (j + 1) y)) :=
+  PolynomialAtomRow.preparation.rowNormPow_falseFirstOverflowBefore_le
+    (θ := 1) (η := 1 / 16) (N := 1) (u := 1)
+    (by norm_num) (by norm_num) (by norm_num) (by norm_num)
+    source retained (fun _ => 2) 2 (by norm_num) 1 (by intros; norm_num)
+    increments (fun _ _ => initial) (fun _ _ _ => 0)
+    (by intros; rfl) (by intros; exact le_rfl) (by intros; rfl)
+
+-- The finite-union result also admits an empty horizon without a capacity premise.
+open Classical in
+example :
+    rowNormPow 4 1 1 source retained (fun σ x y =>
+      if ∃ j < 0,
+        IsFirstOverflow {y | retained σ y} (fun _ => 0) (fun _ => 2)
+            (dyadicFloor (1 / 16) 0) (increments σ x) initial j ∧
+          ¬ heavyCountEvent retained univ (fun _ => 0) (dyadicFloor (1 / 16) 0 j) 0 σ
+      then PolynomialAtomRow.preparation.stateRootError 1 {y | retained σ y}
+        2 initial ⟨0, 0⟩ y else 0) ≤
+      ∑ j ∈ range 0, (64 * 2 / (0 * dyadicFloor (1 / 16) 0 j ^ 4)) *
+        rowNormPow 4 1 1 source retained (fun σ x y =>
+          clippedError 0 0 (uncompressedRow (increments σ x) initial.row (j + 1) y)) :=
+  PolynomialAtomRow.preparation.rowNormPow_falseFirstOverflowBefore_le
+    (θ := 1) (η := 1 / 16) (N := 1) (u := 1)
+    (by norm_num) (by norm_num) (by norm_num) (by norm_num)
+    source retained (fun _ => 0) 2 (by norm_num) 0 (by simp)
+    increments (fun _ _ => initial) (fun _ _ _ => 0)
+    (by intros; rfl) (by intros; exact le_rfl) (by intros; rfl)
+
+end ComplexityTests.PolynomialAtomFalseOverflow