feat(logspace): bound polynomial row errors without overflow

Complexity.lean

@@ -2480,6 +2480,7 @@ public import Complexity.Foundations.Analysis.LpNormMeasure
 public import Complexity.Foundations.Analysis.MarkovBrothersInequality
 public import Complexity.Foundations.Analysis.RootError
 public import Complexity.Foundations.Analysis.RowCompression
+public import Complexity.Foundations.Analysis.RowCompression.ClippedError
 public import Complexity.Foundations.Analysis.RowCompression.FalseOverflow
 public import Complexity.Foundations.Analysis.RowCompression.Floors
 public import Complexity.Foundations.Analysis.RowCompression.GateClosure
@@ -2723,6 +2724,7 @@ public import Complexity.Foundations.Data.Finset.Average
 public import Complexity.Foundations.Data.Finset.Expect
 public import Complexity.Foundations.Data.Finset.Finpartition
 public import Complexity.Foundations.Data.Finset.KthLargest
+public import Complexity.Foundations.Data.Finset.KthLargest.Truncation
 public import Complexity.Foundations.Data.Finset.Markov
 public import Complexity.Foundations.Data.Finset.OrderGlue
 public import Complexity.Foundations.Data.Finset.OrderedFilter
@@ -2922,9 +2924,12 @@ 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.PolynomialAtomRows.ClippedError
 public import Complexity.Foundations.Probability.PolynomialAtomRows.FirstOverflow
+public import Complexity.Foundations.Probability.PolynomialAtomRows.NoOverflow
 public import Complexity.Foundations.Probability.PolynomialAtomRows.Relative
 public import Complexity.Foundations.Probability.PolynomialAtomRows.RootError
+public import Complexity.Foundations.Probability.PolynomialAtomRows.Saturation
 public import Complexity.Foundations.Probability.ProductError
 public import Complexity.Foundations.Probability.RootMetric
 public import Complexity.Foundations.Probability.RootMetric.Minkowski

Complexity/Foundations/Analysis/RowCompression/ClippedError.lean

@@ -0,0 +1,41 @@
+/-
+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.Preloss
+import Mathlib.Tactic.Linarith
+
+/-!
+# Recovering coordinate bounds from small clipped errors
+
+Below one, the maximum of the clipped relative first-channel error and clipped absolute
+second-channel error bounds both original errors. This shared fact is used by the static
+polynomial comparison and by the adjacent-prefix sentinel estimates.
+
+## Main results
+
+* `Cslib.RowCompression.abs_sub_le_of_clippedError_le`: small clipped error gives the actual
+  relative first-coordinate and absolute second-coordinate bounds.
+-/
+
+public section
+
+namespace Cslib.RowCompression
+
+/-- 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
+
+end Cslib.RowCompression

Complexity/Foundations/Analysis/RowCompression/SentinelRelative.lean

@@ -8,7 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Foundations.Analysis.RowCompression.Perturbation
-public import Complexity.Foundations.Analysis.RowCompression.Preloss
+public import Complexity.Foundations.Analysis.RowCompression.ClippedError
 public import Complexity.Foundations.Analysis.RowCompression.SentinelIteration
 import Mathlib.Algebra.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
@@ -50,8 +50,6 @@ 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.abs_increment_le_of_clippedError_le`: adjacent prefix errors bound
   the actual two-channel increment.
 * `Cslib.RowCompression.iterate_sentinelState_stability_of_clippedError_le`: quantitative
@@ -72,17 +70,6 @@ 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
-
 /-- Adjacent small clipped-prefix errors control the actual increment in both channels. -/
 theorem abs_increment_le_of_clippedError_le {ι : Type*} {Δ : ℕ → ι → Fin 2 → ℝ}
     {raw₀ : ι → Fin 2 → ℝ} {truth : Fin 2 → ℝ} {ε ε' : ℝ} {i : ℕ} {y : ι}

Complexity/Foundations/Data/Finset/KthLargest/Truncation.lean

@@ -0,0 +1,55 @@
+/-
+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.Data.Finset.KthLargest
+
+/-!
+# Upper truncation of zero-padded order statistics
+
+Capping every value at a nonnegative threshold caps the positive-order `k`-th largest value
+at the same threshold. Nonnegativity of the cap preserves the zero padding. Input values may
+be negative, and the retained cardinality may be smaller than the requested rank.
+
+## Main results
+
+* `Finset.kthLargest_min`: upper truncation commutes with the padded order statistic.
+-/
+
+public section
+
+namespace Finset
+
+variable {α R : Type*} [LinearOrder R] [Zero R] {s : Finset α} {k : ℕ} {f : α → R} {t : R}
+
+/-- An upper cap that preserves zero commutes with every positive-order padded rank. -/
+theorem kthLargest_min (hk : 0 < k) (ht : 0 ≤ t) :
+    kthLargest k s (fun x => min t (f x)) = min t (kthLargest k s f) := by
+  classical
+  apply le_antisymm
+  · refine le_min (kthLargest_le ht fun _ _ => min_le_left _ _) ?_
+    refine not_lt.mp fun hlt => ?_
+    have hc := (lt_kthLargest_iff hk kthLargest_nonneg).mp hlt
+    have hs : ({x ∈ s | kthLargest k s f < min t (f x)} : Finset α) ⊆
+        {x ∈ s | kthLargest k s f < f x} := by
+      intro x hx
+      exact mem_filter.mpr ⟨(mem_filter.mp hx).1,
+        (mem_filter.mp hx).2.trans_le (min_le_right _ _)⟩
+    exact lt_irrefl _ ((lt_kthLargest_iff hk kthLargest_nonneg).mpr
+      (hc.trans (card_le_card hs)))
+  · by_cases hzero : min t (kthLargest k s f) ≤ 0
+    · exact hzero.trans kthLargest_nonneg
+    have hpos : 0 < min t (kthLargest k s f) := not_le.mp hzero
+    apply (le_kthLargest_iff hk hpos).mpr
+    have hc := (le_kthLargest_iff hk hpos).mp (min_le_right t (kthLargest k s f))
+    apply hc.trans (card_le_card ?_)
+    intro x hx
+    exact mem_filter.mpr ⟨(mem_filter.mp hx).1,
+      le_min (min_le_left _ _) (mem_filter.mp hx).2⟩
+
+end Finset

Complexity/Foundations/Probability/PolynomialAtomRows/ClippedError.lean

@@ -0,0 +1,134 @@
+/-
+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.RootError
+public import Complexity.Foundations.Probability.PolynomialAtomRows.Saturation
+public import Complexity.Foundations.Analysis.RowCompression.ClippedError
+import Complexity.Foundations.Data.Finset.KthLargest.Truncation
+import Mathlib.Algebra.Order.Group.MinMax
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+
+/-!
+# Static polynomial row comparison from clipped raw error
+
+Compare a raw row and the true row after adding the same bounded first-coordinate loss and
+using the same arbitrary default. Their actual polynomial fourth-root outputs differ by at
+most a fixed coefficient times the clipped raw-error envelope. The coefficient depends only
+on the concrete function and support scale, independently of the largest true entry.
+
+Upper entry saturation and gate closure let us cap entries and padded ranks at `θ` without
+changing any output. For error at most `1/2`, entries with true first coordinate above
+`4 * (θ + 1)` cap to the same value; every other capped discrepancy is at most
+`(4 * θ + 5) * ε`. Capping commutes with the zero-padded order statistic, so the same bound
+controls the capped rank. Larger errors are handled by the proved output range.
+
+This is the static final-prefix comparison used in the no-overflow bound following Lemma 8.2
+of [OpenAI2026LogSpace, Section 8.3]. No threshold bound, count branch, compression schedule, or
+assumed final-output estimate occurs in this module.
+
+## Main results
+
+* `Cslib.PolynomialAtomRow.eval_eq_upperCapped`: actual output is invariant under upper caps
+  on its entry and rank arguments.
+* `Cslib.PolynomialAtomRow.exists_commonLoss_root_bound`: actual clipped raw error controls
+  output-root error after a common bounded first-coordinate loss and arbitrary common default.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 8.3, the no-overflow comparison following Lemma 8.2
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+namespace Cslib.PolynomialAtomRow
+
+open Finset RowCompression
+
+variable (kind : PolynomialAtomRow) {θ : ℝ}
+
+/-- Capping either scalar argument at the support scale leaves the actual output unchanged. -/
+theorem eval_eq_upperCapped (hθ : 0 < θ) (v r : ℝ) :
+    kind.eval θ v r = kind.eval θ (min θ v) (min θ r) := by
+  have hentry : kind.eval θ v r = kind.eval θ (min θ v) r := by
+    by_cases hv : v ≤ θ
+    · rw [min_eq_right hv]
+    · rw [min_eq_left (not_le.mp hv).le]
+      exact kind.eval_eq_of_entry_ge hθ (not_le.mp hv).le le_rfl
+  apply hentry.trans
+  by_cases hr : r ≤ θ
+  · rw [min_eq_right hr]
+  · rw [min_eq_left (not_le.mp hr).le]
+    exact (kind.eval_eq_zero_of_rank_ge hθ
+      ((kind.gateThreshold_le_scale hθ).trans (not_le.mp hr).le)).trans
+        (kind.eval_eq_zero_of_rank_ge hθ (kind.gateThreshold_le_scale hθ)).symm
+
+private theorem abs_min_add_sub_min_add_le {d raw loss ε : ℝ} (hθ : 0 < θ)
+    (hε : 0 ≤ ε) (hεsmall : ε ≤ 1 / 2)
+    (hraw : |raw - d| ≤ (1 + d) * ε) (hloss : |loss| ≤ θ) :
+    |min θ (raw + loss) - min θ (d + loss)| ≤ (4 * θ + 5) * ε := by
+  have hδ : 0 ≤ (4 * θ + 5) * ε := by positivity
+  by_cases hdlarge : d ≤ 4 * (θ + 1)
+  · apply (abs_min_sub_min_le_max _ _ _ _).trans
+    refine max_le (by simpa only [sub_self, abs_zero] using hδ) ?_
+    simp only [add_sub_add_right_eq_sub]
+    exact hraw.trans (mul_le_mul_of_nonneg_right (by linarith) hε)
+  · have hproduct := mul_le_mul_of_nonneg_left hεsmall (by linarith [not_le.mp hdlarge] : 0 ≤ 1 + d)
+    have hrawlo := (abs_le.mp hraw).1
+    have hlosslo := (abs_le.mp hloss).1
+    have hcapraw : θ ≤ raw + loss := by nlinarith [not_le.mp hdlarge]
+    have hcaptruth : θ ≤ d + loss := by linarith [not_le.mp hdlarge]
+    simpa only [min_eq_left hcapraw, min_eq_left hcaptruth, sub_self, abs_zero] using hδ
+
+/-- A clipped raw-error envelope controls the actual polynomial root outputs after a common
+loss. Only the first loss coordinate is bounded; second coordinates and the common default
+are unrestricted. The final coefficient is independent of all row data and entry magnitudes. -/
+theorem exists_commonLoss_root_bound (hθ : 0 < θ) :
+    ∃ C : ℝ, 0 ≤ C ∧ ∀ {ι : Type*} (s : Finset ι) (K : ℕ) (z : ℝ)
+      (truth raw loss : ι → Fin 2 → ℝ), 0 < K →
+      (∀ y ∈ s, 0 ≤ truth y 0) → (∀ y ∈ s, |loss y 0| ≤ θ) →
+      ∀ (ε : ℝ), 0 ≤ ε →
+      (∀ y ∈ s, clippedError (truth y 0) (truth y 1) (raw y) ≤ ε) →
+      ∀ y ∈ s,
+      |kind.stateRootError θ s K ⟨z, raw + loss⟩ ⟨z, truth + loss⟩ y| ≤ C * ε := by
+  obtain ⟨A, hA, hroot⟩ := kind.exists_abs_eval_root_sub_le θ
+  let B := 4 * θ + 5
+  have hB : 0 ≤ B := by dsimp only [B]; positivity
+  refine ⟨2 + 2 * A * B, by positivity, ?_⟩
+  intro ι s K z truth raw loss hK hfirst hloss ε hε herr y hy
+  by_cases hsmall : ε ≤ 1 / 2
+  · have hcap (x : ι) (hx : x ∈ s) :
+        |min θ ((raw + loss) x 0) - min θ ((truth + loss) x 0)| ≤ B * ε :=
+      abs_min_add_sub_min_add_le hθ hε hsmall
+        (abs_sub_le_of_clippedError_le (hfirst x hx) (by linarith : ε < 1) (herr x hx)).1
+        (hloss x hx)
+    have hq : |min θ (firstRank s K z (raw + loss)) -
+        min θ (firstRank s K z (truth + loss))| ≤ B * ε := by
+      simp only [firstRank, min_max_distrib_left]
+      rw [← kthLargest_min (f := fun x => (raw + loss) x 0) hK hθ.le,
+        ← kthLargest_min (f := fun x => (truth + loss) x 0) hK hθ.le]
+      exact (abs_max_sub_max_le_max _ _ _ _).trans (max_le
+        (by simpa only [sub_self, abs_zero] using mul_nonneg hB hε)
+        (abs_kthLargest_sub_kthLargest_le hK (mul_nonneg hB hε) hcap))
+    unfold stateRootError
+    rw [kind.eval_eq_upperCapped hθ ((raw + loss) y 0) (firstRank s K z (raw + loss)),
+      kind.eval_eq_upperCapped hθ ((truth + loss) y 0) (firstRank s K z (truth + loss))]
+    calc
+      _ ≤ A * (|min θ ((raw + loss) y 0) - min θ ((truth + loss) y 0)| +
+          |min θ (firstRank s K z (raw + loss)) -
+            min θ (firstRank s K z (truth + loss))|) := hroot _ _ _ _
+      _ ≤ A * (B * ε + B * ε) := mul_le_mul_of_nonneg_left (add_le_add (hcap y hy) hq) hA
+      _ ≤ (2 + 2 * A * B) * ε := by nlinarith
+  · apply (kind.abs_stateRootError_le_one θ s K ⟨z, raw + loss⟩ ⟨z, truth + loss⟩ y).trans
+    have hlarge : 1 / 2 < ε := not_le.mp hsmall
+    nlinarith [mul_nonneg (mul_nonneg hA hB) hε]
+
+end Cslib.PolynomialAtomRow