feat(logspace): prove polynomial stability after first overflow

Complexity.lean

@@ -2464,11 +2464,13 @@ public import Complexity.Foundations.Analysis.RootError
 public import Complexity.Foundations.Analysis.RowCompression
 public import Complexity.Foundations.Analysis.RowCompression.FalseOverflow
 public import Complexity.Foundations.Analysis.RowCompression.Floors
+public import Complexity.Foundations.Analysis.RowCompression.GateClosure
 public import Complexity.Foundations.Analysis.RowCompression.Iteration
 public import Complexity.Foundations.Analysis.RowCompression.NoiseDecay
 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.PreloadedIteration
 public import Complexity.Foundations.Analysis.RowCompression.Preloss
 public import Complexity.Foundations.Analysis.RowCompression.Reference
 public import Complexity.Foundations.Analysis.RowCompression.Sentinel
@@ -2900,6 +2902,9 @@ 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.FirstOverflow
+public import Complexity.Foundations.Probability.PolynomialAtomRows.Relative
+public import Complexity.Foundations.Probability.PolynomialAtomRows.RootError
 public import Complexity.Foundations.Probability.ProductError
 public import Complexity.Foundations.Probability.RootMetric
 public import Complexity.Foundations.Probability.RootMetric.Minkowski

Complexity/Foundations/Analysis/RowCompression/GateClosure.lean

@@ -0,0 +1,103 @@
+/-
+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.Tactic.Linarith
+
+/-!
+# Persistent closure of the rank gate
+
+A marked collection whose actual raw first coordinates stay above `3 * G` has two possible
+behaviors. As long as the default remains below `G`, every marked entry stays in the identity
+region of compression and follows its raw prefix exactly. Once a threshold reaches `G`, the
+new default reaches `G` and can never fall below it. With at least `K` marked retained entries,
+the actual default-padded first rank is therefore at least `G` throughout the calculation.
+
+This is the large-heavy-set branch in [OpenAI2026LogSpace, Section 8.3, Lemma 8.3]. The raw
+lower bound is an explicit hypothesis here; the concrete polynomial-row client derives it
+from small clipped-prefix errors and large true first entries. Neither an upper bound on the
+thresholds nor agreement of exception lists is required.
+
+## Main results
+
+* `Cslib.RowCompression.gate_le_default_or_iterate_row_eq`: either the default closes the
+  gate, or every marked compressed entry still equals its raw prefix.
+* `Cslib.RowCompression.le_iterate_firstRank_of_raw_large`: enough such entries force the
+  actual padded rank above the gate threshold.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 8.3, proof of Lemma 8.3, the branch with at least `K` entries above `L₀`
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+namespace Cslib.RowCompression
+
+open Finset
+
+variable {ι : Type*} {s D : Finset ι} {n K : ℕ → ℕ} {ρ : ℕ → ℝ}
+  {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} {G : ℝ}
+
+/-- A large raw entry is preserved until a threshold raises the default to the gate level.
+Both channels are preserved, even when the second channel is signed. -/
+theorem gate_le_default_or_iterate_row_eq (m : ℕ)
+    (hraw : ∀ i ≤ m, ∀ y ∈ D, 3 * G ≤ uncompressedRow Δ a.row i y 0) :
+    G ≤ (iterate s n K ρ Δ a m).defaultValue ∨
+      ∀ y ∈ D, (iterate s n K ρ Δ a m).row y = uncompressedRow Δ a.row m y := by
+  induction m with
+  | zero => exact Or.inr fun _ _ => (congrFun uncompressedRow_zero _).symm
+  | succ m ih =>
+    by_cases hu : G ≤ stepThreshold s n K ρ Δ a m
+    · exact Or.inl (hu.trans threshold_le_newDefault)
+    · have hprevious : ∀ y ∈ D, (iterate s n K ρ Δ a m).row y =
+          uncompressedRow Δ a.row m y := by
+        rcases ih (fun i hi => hraw i (hi.trans (Nat.le_succ m))) with hz | hw
+        · exact False.elim (hu (hz.trans le_threshold))
+        · exact hw
+      refine Or.inr fun y hy => ?_
+      have hinput : inputRow s n K ρ Δ a m y = uncompressedRow Δ a.row (m + 1) y := by
+        funext ν
+        rw [uncompressedRow_succ]
+        change (iterate s n K ρ Δ a m).row y ν + Δ m y ν = _
+        rw [hprevious y hy]
+      have hlarge : 3 * stepThreshold s n K ρ Δ a m ≤
+          entrySize (inputRow s n K ρ Δ a m y) := by
+        have hr := hraw (m + 1) (le_refl _) y hy
+        have hv := (le_abs_self (inputRow s n K ρ Δ a m y 0)).trans
+          (abs_apply_le_entrySize (inputRow s n K ρ Δ a m y) 0)
+        rw [hinput]
+        rw [hinput] at hv
+        linarith [not_le.mp hu]
+      change update s (n m) (K m) (ρ m) (iterate s n K ρ Δ a m).defaultValue
+        (inputRow s n K ρ Δ a m) y = _
+      rw [update_eq_self_of_three_mul_le hlarge]
+      exact hinput
+
+/-- At least `k` large raw first entries close the actual padded rank gate. The compression
+capacities may vary independently; no threshold upper bound is assumed. -/
+theorem le_iterate_firstRank_of_raw_large {k : ℕ} (hG : 0 < G) (hk : 0 < k)
+    (hDs : D ⊆ s) (hcard : k ≤ #D) (m : ℕ)
+    (hraw : ∀ i ≤ m, ∀ y ∈ D, 3 * G ≤ uncompressedRow Δ a.row i y 0) :
+    G ≤ firstRank s k (iterate s n K ρ Δ a m).defaultValue
+      (iterate s n K ρ Δ a m).row := by
+  classical
+  rcases gate_le_default_or_iterate_row_eq m hraw with hz | hw
+  · exact hz.trans default_le_firstRank
+  · apply le_trans _ kthLargest_le_firstRank
+    apply (le_kthLargest_iff hk hG).mpr
+    apply hcard.trans (card_le_card ?_)
+    intro y hy
+    apply mem_filter.mpr ⟨hDs hy, ?_⟩
+    rw [hw y hy]
+    linarith [hraw m (le_refl _) y hy]
+
+end Cslib.RowCompression

Complexity/Foundations/Analysis/RowCompression/PreloadedIteration.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.SentinelRelative
+public import Mathlib.Order.Interval.Finset.Nat
+import Mathlib.Algebra.BigOperators.Intervals
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.Positivity
+
+/-!
+# Restarting compression from an already-added group input
+
+At a first overflow in group `j`, the available error estimate concerns the raw input after
+adding group `j`, not the preceding raw prefix. Start the local calculation from the actual
+`inputRow` and use zero as its first increment. The local calculation agrees exactly with the
+original calculation after every positive number of updates.
+
+The corresponding local error sequence repeats the overflow group's error at indices zero and
+one. Its adjacent-prefix propagation budget is at most four times the usual weighted tail sum.
+Only errors from group `j` onward occur in this bound. These are exact indexing and finite-sum
+identities; they require no overflow event, row bounds, or probabilistic hypotheses.
+
+## Main definitions
+
+* `Cslib.RowCompression.preloadedIncrement`: the remaining increment schedule with its first
+  increment already added to the initial state.
+* `Cslib.RowCompression.preloadedError`: the error envelope at the resulting local raw prefixes.
+
+## Main results
+
+* `Cslib.RowCompression.iterate_preloadedIncrement`: equality of the restarted and original
+  compressed calculations after a positive number of updates.
+* `Cslib.RowCompression.uncompressedRow_preloadedIncrement`: equality of the corresponding
+  raw prefixes after a positive number of local increments.
+* `Cslib.RowCompression.prefixErrorBudget_preloadedError_le`: the adjacent-prefix budget is
+  bounded by four times the original weighted tail sum.
+-/
+
+public section
+
+namespace Cslib.RowCompression
+
+open Finset
+
+variable {ι : Type*}
+
+/-- Restart at group `j` after its increment has already been added. The first local increment
+is zero; later local increments are the actual subsequent increments. -/
+@[expose] def preloadedIncrement (Δ : ℕ → ι → Fin 2 → ℝ) (j : ℕ) :
+    ℕ → ι → Fin 2 → ℝ
+  | 0 => 0
+  | i + 1 => Δ (j + i + 1)
+
+@[simp]
+theorem preloadedIncrement_zero (Δ : ℕ → ι → Fin 2 → ℝ) (j : ℕ) :
+    preloadedIncrement Δ j 0 = 0 := rfl
+
+@[simp]
+theorem preloadedIncrement_succ (Δ : ℕ → ι → Fin 2 → ℝ) (j i : ℕ) :
+    preloadedIncrement Δ j (i + 1) = Δ (j + i + 1) := rfl
+
+/-- Both local prefixes zero and one use the already-added group `j` input. Later local
+prefixes use the errors of the subsequent groups. -/
+@[expose] def preloadedError (ε : ℕ → ℝ) (j : ℕ) : ℕ → ℝ
+  | 0 => ε j
+  | i + 1 => ε (j + i)
+
+@[simp]
+theorem preloadedError_zero (ε : ℕ → ℝ) (j : ℕ) : preloadedError ε j 0 = ε j := rfl
+
+@[simp]
+theorem preloadedError_succ (ε : ℕ → ℝ) (j i : ℕ) :
+    preloadedError ε j (i + 1) = ε (j + i) := rfl
+
+/-- A restart from the already-added input gives exactly the original compressed state after
+any positive number of updates. Group `j` is compressed once, with no duplicated increment. -/
+theorem iterate_preloadedIncrement {s : Finset ι} {n K : ℕ → ℕ} {ρ : ℕ → ℝ}
+    {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} (j : ℕ) {r : ℕ} (hr : 0 < r) :
+    iterate s (fun i => n (j + i)) (fun i => K (j + i)) (fun i => ρ (j + i))
+      (preloadedIncrement Δ j)
+      ⟨(iterate s n K ρ Δ a j).defaultValue, inputRow s n K ρ Δ a j⟩ r =
+        iterate s n K ρ Δ a (j + r) := by
+  cases r with
+  | zero => omega
+  | succ r =>
+    clear hr
+    induction r with
+    | zero =>
+      simp [iterate_succ, advance, inputRow]
+    | succ r ih =>
+      rw [iterate_succ, ih]
+      simp only [preloadedIncrement_succ, Nat.add_succ, iterate_succ]
+
+/-- Raw prefixes after the preloaded restart agree with the original raw prefixes. At local
+index zero the initial row is already global raw prefix `j + 1`. -/
+theorem uncompressedRow_preloadedIncrement {Δ : ℕ → ι → Fin 2 → ℝ}
+    {raw₀ : ι → Fin 2 → ℝ} (j : ℕ) {r : ℕ} (hr : 0 < r) :
+    uncompressedRow (preloadedIncrement Δ j) (uncompressedRow Δ raw₀ (j + 1)) r =
+      uncompressedRow Δ raw₀ (j + r) := by
+  cases r with
+  | zero => omega
+  | succ r =>
+    clear hr
+    induction r with
+    | zero =>
+      funext y ν
+      simp only [uncompressedRow_succ, uncompressedRow_zero, preloadedIncrement_zero,
+        Pi.zero_apply, add_zero]
+    | succ r ih =>
+      funext y ν
+      rw [uncompressedRow_succ, ih]
+      simp only [preloadedIncrement_succ, Nat.add_succ, uncompressedRow_succ]
+
+/-- The adjacent-prefix budget for a preloaded restart is at most four times the original
+weighted tail budget. The estimate does not require any error bound before group `j`. -/
+theorem prefixErrorBudget_preloadedError_le {ε : ℕ → ℝ} (j : ℕ) {r : ℕ}
+    (hr : 0 < r) (hε : ∀ i ∈ Ico j (j + r), 0 ≤ ε i) :
+    prefixErrorBudget (preloadedError ε j) r ≤
+      4 * ∑ i ∈ Ico j (j + r), 28 ^ (j + r - i) * ε i := by
+  cases r with
+  | zero => omega
+  | succ r =>
+    let T : ℝ := ∑ i ∈ range (r + 1), 28 ^ (r + 1 - i) * ε (j + i)
+    have hnonneg (i : ℕ) (hi : i < r + 1) : 0 ≤ ε (j + i) :=
+      hε (j + i) (mem_Ico.mpr ⟨Nat.le_add_right _ _, Nat.add_lt_add_left hi _⟩)
+    have htail : (∑ i ∈ Ico j (j + (r + 1)), (28 : ℝ) ^ (j + (r + 1) - i) * ε i) =
+        T := by
+      rw [sum_Ico_eq_sum_range]
+      simp only [Nat.add_sub_cancel_left, Nat.add_sub_add_left]
+      rfl
+    have hfirst : (28 : ℝ) ^ (r + 1) * ε j ≤ T := by
+      have h := single_le_sum (s := range (r + 1))
+        (f := fun i => (28 : ℝ) ^ (r + 1 - i) * ε (j + i))
+        (fun i hi => mul_nonneg (by positivity) (hnonneg i (mem_range.mp hi)))
+        (mem_range.mpr (Nat.zero_lt_succ r))
+      simpa only [Nat.sub_zero, Nat.add_zero] using h
+    have hback :
+        (∑ i ∈ range r, (28 : ℝ) ^ (r - i) * ε (j + i)) ≤ T := by
+      calc
+        _ ≤ ∑ i ∈ range r, (28 : ℝ) ^ (r + 1 - i) * ε (j + i) := 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 (Nat.le_succ r) i)) ?_
+          exact hnonneg i ((mem_range.mp hi).trans_le (Nat.le_succ r))
+        _ ≤ T := sum_le_sum_of_subset_of_nonneg (range_mono (Nat.le_succ r))
+          (fun i hi _ => mul_nonneg (by positivity) (hnonneg i (mem_range.mp hi)))
+    have hbefore :
+        (∑ i ∈ range (r + 1), (28 : ℝ) ^ (r + 1 - i) * preloadedError ε j i) ≤ 2 * T := by
+      rw [sum_range_succ']
+      simp only [preloadedError_succ, preloadedError_zero, Nat.add_sub_add_right, Nat.sub_zero]
+      linarith
+    have hafter :
+        (∑ i ∈ range (r + 1), (28 : ℝ) ^ (r + 1 - i) * preloadedError ε j (i + 1)) = T := by
+      simp only [preloadedError_succ]
+      rfl
+    rw [htail]
+    unfold prefixErrorBudget
+    simp only [mul_add, sum_add_distrib, preloadedError_zero]
+    rw [hafter]
+    linarith
+
+end Cslib.RowCompression