feat(logspace): aggregate noise at the unique first overflow

Complexity.lean

@@ -2423,6 +2423,7 @@ 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.Iteration
+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.Stationary
@@ -2659,6 +2660,7 @@ public import Complexity.Foundations.Data.Finset.Quotient
 public import Complexity.Foundations.Data.Finset.Sampling
 public import Complexity.Foundations.Data.Finset.SubsetSum
 public import Complexity.Foundations.Data.Finset.SymmDiff
+public import Complexity.Foundations.Data.Finset.UniqueTail
 public import Complexity.Foundations.Data.Hamming
 public import Complexity.Foundations.Data.Hamming.Expansion
 public import Complexity.Foundations.Data.Int.LogBounds

Complexity/Foundations/Analysis/RowCompression/OverflowNoise.lean

@@ -0,0 +1,104 @@
+/-
+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.FalseOverflow
+public import Complexity.Foundations.Probability.RootMetric
+public import Complexity.Foundations.Data.Finset.UniqueTail
+import Mathlib.Algebra.Order.BigOperators.Expect
+import Mathlib.Tactic.Positivity
+
+/-!
+# Noise tails at the unique actual first overflow
+
+On each row there is at most one first-overflow index. Hence the sum of its selected noise
+tail is bounded by the full weighted noise sum, pointwise in the environment. The resulting
+integrated moment comparison permits arbitrary dependence between noise and overflow.
+
+This is the pointwise aggregation step in [OpenAI2026LogSpace, Section 8.4], the paragraph
+leading to equation `buf-noise-sum`. The event is `IsFirstOverflow` of the actual compression
+run. No conditional rarity discount is claimed for noise. Prefix-noise budgets, Minkowski,
+propagation weights and convergence of their final series remain separate.
+
+## Main results
+
+* `Cslib.RowCompression.firstOverflowNoiseTail_le`: selected actual tails cost at most one full sum.
+* `Cslib.RowCompression.vertexNormPow_firstOverflowNoiseTail_le`: integrated moment comparison
+  in the existing `RootMetric` normalization, allowing all correlations.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 8.4, proof paragraph leading to equation labelled `buf-noise-sum`
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+open Finset
+open scoped BigOperators
+
+namespace Cslib.RowCompression
+
+variable {ι : Type*}
+
+/-- The sum of weighted tails selected by actual first-overflow events before group `m`.
+This finite quantity is defined even for runs without an overflow. -/
+@[expose] noncomputable def firstOverflowNoiseTail (s : Finset ι) (n K : ℕ → ℕ)
+    (ρ : ℕ → ℝ) (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (m : ℕ) (w γ : ℕ → ℝ) : ℝ := by
+  classical
+  exact ∑ j ∈ range m, if IsFirstOverflow s n K ρ Δ a j then
+    ∑ i ∈ Ico j m, w i * γ i else 0
+
+/-- Nonnegative weights and noise give a nonnegative selected tail, even without an overflow. -/
+theorem firstOverflowNoiseTail_nonneg (s : Finset ι) (n K : ℕ → ℕ)
+    (ρ : ℕ → ℝ) (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (m : ℕ) {w γ : ℕ → ℝ}
+    (hw : ∀ i < m, 0 ≤ w i) (hγ : ∀ i < m, 0 ≤ γ i) :
+    0 ≤ firstOverflowNoiseTail s n K ρ Δ a m w γ := by
+  classical
+  unfold firstOverflowNoiseTail
+  refine sum_nonneg fun j _ => ?_
+  split_ifs
+  · exact sum_nonneg fun i hi => mul_nonneg (hw i (mem_Ico.mp hi).2) (hγ i (mem_Ico.mp hi).2)
+  · exact le_rfl
+
+/-- **Actual first-overflow noise aggregation.** The first index is unique for every run,
+so its nonnegative weighted tail is bounded by the single full sum. -/
+theorem firstOverflowNoiseTail_le (s : Finset ι) (n K : ℕ → ℕ)
+    (ρ : ℕ → ℝ) (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (m : ℕ) {w γ : ℕ → ℝ}
+    (hw : ∀ i < m, 0 ≤ w i) (hγ : ∀ i < m, 0 ≤ γ i) :
+    firstOverflowNoiseTail s n K ρ Δ a m w γ ≤ ∑ i ∈ range m, w i * γ i := by
+  classical
+  exact sum_ite_Ico_le_sum_range m (IsFirstOverflow s n K ρ Δ a)
+    (fun i hi => mul_nonneg (hw i hi) (hγ i hi)) (fun _ _ _ _ hj hk => hj.unique hk)
+
+/-- **Integrated noise aggregation.** Noise may depend on the same environment as the entire
+compression run. No independence or conditional-frequency hypothesis occurs. -/
+theorem vertexNormPow_firstOverflowNoiseTail_le {Ω V : Type*} [Fintype Ω] [Fintype V]
+    (S : Ω → V → Finset ι) (n K : ℕ → ℕ) (ρ : ℕ → ℝ)
+    (Δ : Ω → V → ℕ → ι → Fin 2 → ℝ) (a : Ω → V → State ι) (m : ℕ)
+    {p : ℕ} {N u : ℝ} (hNu : 0 ≤ N * u) (X : Ω → V → Prop) [∀ σ x, Decidable (X σ x)]
+    (w : ℕ → ℝ) (γ : ℕ → Ω → V → ℝ) (hw : ∀ i < m, 0 ≤ w i)
+    (hγ : ∀ i < m, ∀ σ x, X σ x → 0 ≤ γ i σ x) :
+    vertexNormPow p N u X (fun σ x =>
+      firstOverflowNoiseTail (S σ x) n K ρ (Δ σ x) (a σ x) m w (fun i => γ i σ x)) ≤
+        vertexNormPow p N u X (fun σ x => ∑ i ∈ range m, w i * γ i σ x) := by
+  unfold vertexNormPow
+  refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (inv_nonneg.mpr hNu)
+  refine sum_le_sum fun x hx => ?_
+  have hx' : X σ x := (mem_filter.mp hx).2
+  have hnoise := firstOverflowNoiseTail_nonneg (S σ x) n K ρ (Δ σ x) (a σ x) m hw
+    (fun i hi => hγ i hi σ x hx')
+  have hfull : 0 ≤ ∑ i ∈ range m, w i * γ i σ x :=
+    sum_nonneg fun i hi => mul_nonneg (hw i (mem_range.mp hi)) (hγ i (mem_range.mp hi) σ x hx')
+  rw [abs_of_nonneg hnoise, abs_of_nonneg hfull]
+  exact pow_le_pow_left₀ hnoise
+    (firstOverflowNoiseTail_le (S σ x) n K ρ (Δ σ x) (a σ x) m hw
+      (fun i hi => hγ i hi σ x hx')) p
+
+end Cslib.RowCompression

Complexity/Foundations/Data/Finset/UniqueTail.lean

@@ -0,0 +1,50 @@
+/-
+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 (Mathlib)
+
+public import Complexity.Init
+public import Mathlib.Algebra.Order.BigOperators.Group.Finset
+public import Mathlib.Order.Interval.Finset.Nat
+import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
+
+/-!
+# At most one selected tail of a nonnegative finite sum
+
+If at most one index is selected, summing the selected tails counts each nonnegative summand
+at most once. This pointwise fact needs no probabilistic independence. Its compression
+consumer uses uniqueness of the actual first-overflow index.
+-/
+
+public section
+
+namespace Finset
+
+/-- If at most one starting index is selected, its nonnegative tail is bounded by the full sum.
+The endpoint `m` is excluded from both sums. -/
+theorem sum_ite_Ico_le_sum_range {M : Type*} [AddCommMonoid M] [Preorder M] [AddLeftMono M]
+    (m : ℕ) (P : ℕ → Prop) [DecidablePred P] {f : ℕ → M} (hf : ∀ i < m, 0 ≤ f i)
+    (hunique : ∀ j < m, ∀ k < m, P j → P k → j = k) :
+    (∑ j ∈ range m, if P j then ∑ i ∈ Ico j m, f i else 0) ≤ ∑ i ∈ range m, f i := by
+  have htail (j : ℕ) : (∑ i ∈ Ico j m, f i) ≤ ∑ i ∈ range m, f i :=
+    sum_le_sum_of_subset_of_nonneg
+      (fun i hi => mem_range.mpr (mem_Ico.mp hi).2)
+      (fun i hi _ => hf i (mem_range.mp hi))
+  calc
+    _ ≤ ∑ j ∈ range m, if P j then ∑ i ∈ range m, f i else 0 := by
+      refine sum_le_sum fun j _ => ?_
+      split_ifs
+      · exact htail j
+      · exact le_rfl
+    _ ≤ ∑ i ∈ range m, f i := by
+      rw [sum_ite_zero (range m) P
+        (fun j hj k hk => hunique j (mem_range.mp hj) k (mem_range.mp hk))]
+      split_ifs
+      · exact le_rfl
+      · exact sum_nonneg fun i hi => hf i (mem_range.mp hi)
+
+end Finset

ComplexityTests/RowCompressionOverflowNoise.lean

@@ -0,0 +1,145 @@
+/-
+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.OverflowNoise
+import Complexity.Foundations.Data.Finset.Expect
+import Mathlib.LinearAlgebra.Matrix.Notation
+import Mathlib.Tactic.NormNum
+
+/-!
+# Tests for aggregation of actual first-overflow noise
+
+The first group compresses a zero row to default one. On the false Boolean draw, the next
+group adds `(4, -2)` and first overflows at index one. Its selected weighted noise tail is
+`2 * 5 + 1 * 11 = 21`, while the full weighted sum is `4 * 7 + 2 * 5 + 1 * 11 = 49`.
+Noise vanishes on the other draw, so it is correlated with the overflow event. The actual
+fourth-moment comparison is checked with the existing vertex norm and positive normalization.
+-/
+
+namespace ComplexityTests.RowCompressionOverflowNoise
+
+open Finset Cslib Cslib.RowCompression
+open scoped BigOperators
+
+private def initial : State (Fin 1) := { defaultValue := 0, row := 0 }
+
+private def increments (σ : Bool) (i : ℕ) (_ : Fin 1) : Fin 2 → ℝ :=
+  if σ = false ∧ i = 1 then ![4, -2] else 0
+
+private def weight (i : ℕ) : ℝ := if i = 0 then 4 else if i = 1 then 2 else 1
+
+private def noise (i : ℕ) (σ : Bool) : ℝ :=
+  if σ = false then if i = 0 then 7 else if i = 1 then 5 else 11 else 0
+
+private theorem first_overflow :
+    IsFirstOverflow univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+      (increments false) initial 1 := by
+  constructor
+  · intro i hi
+    have hi0 : i = 0 := by omega
+    subst i
+    norm_num [stepThreshold, inputRow, iterate, initial, increments,
+      threshold, kthLargest, entrySize, Fin.univ_succ, filter_insert, filter_singleton]
+  · norm_num [stepThreshold, inputRow, iterate, advance, initial, increments,
+      newDefault, threshold, kthLargest, entrySize, update, updateEntry, radius, defaultEntry,
+      Fin.univ_succ, filter_insert, filter_singleton]
+
+private theorem first_overflow_iff (j : ℕ) :
+    IsFirstOverflow univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+      (increments false) initial j ↔ j = 1 := by
+  constructor
+  · exact fun hj => hj.unique first_overflow
+  · rintro rfl
+    exact first_overflow
+
+-- The first group changes the stored row, before the nonzero overflow increment arrives.
+example : (iterate univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+    (increments false) initial 1).defaultValue = 1 := by
+  norm_num [iterate, advance, initial, increments, newDefault, threshold, kthLargest,
+    entrySize, Fin.univ_succ, filter_insert, filter_singleton]
+
+-- The event and noise share the same Boolean draw; no independence hypothesis is available.
+example : noise 1 false = 5 ∧ noise 1 true = 0 ∧
+    ¬ IsFirstOverflow univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+      (increments true) initial 1 := by
+  constructor
+  · norm_num [noise]
+  constructor
+  · norm_num [noise]
+  · intro h
+    have hlt := h.2
+    norm_num [stepThreshold, inputRow, iterate, advance, initial, increments,
+      newDefault, threshold, kthLargest, entrySize, update, updateEntry, radius, defaultEntry,
+      Fin.univ_succ, filter_insert, filter_singleton] at hlt
+
+private theorem selected_tail :
+    firstOverflowNoiseTail univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+      (increments false) initial 3 weight (fun i => noise i false) = 21 := by
+  unfold firstOverflowNoiseTail
+  simp only [first_overflow_iff]
+  norm_num [sum_range_succ, weight, noise, Finset.sum_Ico_succ_top]
+
+private theorem full_sum : (∑ i ∈ range 3, weight i * noise i false) = 49 := by
+  norm_num [sum_range_succ, weight, noise]
+
+-- The actual-run theorem gives a strict, nonzero instance, retaining the same full sum once.
+example : firstOverflowNoiseTail univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+    (increments false) initial 3 weight (fun i => noise i false) ≤
+      ∑ i ∈ range 3, weight i * noise i false := by
+  apply firstOverflowNoiseTail_le
+  · intro i _
+    simp only [weight]
+    split_ifs <;> norm_num
+  · intro i _
+    simp only [noise]
+    split_ifs <;> norm_num
+
+example : 0 < firstOverflowNoiseTail univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+    (increments false) initial 3 weight (fun i => noise i false) ∧
+    firstOverflowNoiseTail univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+      (increments false) initial 3 weight (fun i => noise i false) <
+        ∑ i ∈ range 3, weight i * noise i false := by
+  rw [selected_tail, full_sum]
+  norm_num
+
+-- The moment theorem permits the increments, event and noise to depend on the same seed.
+example : vertexNormPow 4 1 1 (fun (_ : Bool) (_ : Fin 1) => True)
+    (fun σ _ => firstOverflowNoiseTail univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+      (increments σ) initial 3 weight (fun i => noise i σ)) ≤
+    vertexNormPow 4 1 1 (fun (_ : Bool) (_ : Fin 1) => True)
+      (fun σ _ => ∑ i ∈ range 3, weight i * noise i σ) := by
+  apply vertexNormPow_firstOverflowNoiseTail_le (fun _ _ => univ)
+    (fun _ => 1) (fun _ => 1) (fun _ => 1) (fun σ _ => increments σ)
+    (fun _ _ => initial) 3 (by norm_num)
+  · intro i _
+    simp only [weight]
+    split_ifs <;> norm_num
+  · intro i _ σ _ _
+    simp only [noise]
+    split_ifs <;> norm_num
+
+example : vertexNormPow 4 1 1 (fun (_ : Bool) (_ : Fin 1) => True)
+    (fun σ _ => firstOverflowNoiseTail univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+      (increments σ) initial 3 weight (fun i => noise i σ)) = 194481 / 2 := by
+  have hz : firstOverflowNoiseTail univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+      (increments true) initial 3 weight (fun i => noise i true) = 0 := by
+    simp [firstOverflowNoiseTail, noise]
+  unfold vertexNormPow
+  rw [Fintype.expect_bool]
+  dsimp only
+  rw [selected_tail, hz]
+  norm_num
+
+example : vertexNormPow 4 1 1 (fun (_ : Bool) (_ : Fin 1) => True)
+    (fun σ _ => ∑ i ∈ range 3, weight i * noise i σ) = 5764801 / 2 := by
+  unfold vertexNormPow
+  rw [Fintype.expect_bool]
+  norm_num [Fin.sum_univ_one, sum_range_succ, weight, noise]
+
+-- Without uniqueness, the same summands can be counted repeatedly in several tails.
+example : (∑ j ∈ range 3, ∑ _i ∈ Ico j 3, (1 : ℝ)) > ∑ _i ∈ range 3, (1 : ℝ) := by
+  norm_num [sum_range_succ]
+
+end ComplexityTests.RowCompressionOverflowNoise