feat(logspace): bound overflow noise from individual moment budgets

Complexity.lean

@@ -2450,6 +2450,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.OverflowBudget
 public import Complexity.Foundations.Analysis.RowCompression.OverflowNoise
 public import Complexity.Foundations.Analysis.RowCompression.Preloss
 public import Complexity.Foundations.Analysis.RowCompression.Reference
@@ -2876,6 +2877,7 @@ 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.RootMetric.Minkowski
 public import Complexity.Foundations.Probability.SecondMoment
 public import Complexity.Foundations.Probability.SourceRelease
 public import Complexity.Foundations.Probability.StochasticAtom

Complexity/Foundations/Analysis/RowCompression/OverflowBudget.lean

@@ -0,0 +1,63 @@
+/-
+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.OverflowNoise
+public import Complexity.Foundations.Probability.RootMetric.Minkowski
+
+/-!
+# Moment budgets for the actual first-overflow noise tail
+
+The pointwise unique-tail comparison and finite Minkowski inequality turn individual noise
+moment budgets into a budget for the actual first-overflow tail. All arrays and events may
+depend on the same environment. No conditional rarity factor is applied to noise.
+
+This supplies the finite Minkowski step of [OpenAI2026LogSpace, Section 8.4], leading to
+`buf-noise-sum`. The individual prefix-noise estimates, propagation-weight bounds and the
+uniform bound on their weighted budget sum remain separate obligations.
+
+## Main results
+
+* `Cslib.RowCompression.vertexNormPow_firstOverflowNoiseTail_le_pow_sum`: the actual tail
+  satisfies the power of the weighted sum of individual moment budgets.
+
+## 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
+
+/-- **The finite first-overflow noise budget.** Individual normalized `p`-th moments bounded
+by `ε i ^ p` give a tail budget `(∑ i < m, w i * ε i) ^ p`. This allows arbitrary correlation
+between all noise arrays, the compression run, and the retained sources. -/
+theorem vertexNormPow_firstOverflowNoiseTail_le_pow_sum {Ω V ι : Type*}
+    [Fintype Ω] [Fintype V] (S : Ω → V → Finset ι) (n K : ℕ → ℕ) (ρ : ℕ → ℝ)
+    (Δ : Ω → V → ℕ → ι → Fin 2 → ℝ) (a : Ω → V → State ι) (m : ℕ)
+    {p : ℕ} (hp : p ≠ 0) {N u : ℝ} (hNu : 0 ≤ N * u)
+    (X : Ω → V → Prop) [∀ σ x, Decidable (X σ x)]
+    (w ε : ℕ → ℝ) (γ : ℕ → Ω → V → ℝ)
+    (hw : ∀ i < m, 0 ≤ w i) (hε : ∀ i < m, 0 ≤ ε i)
+    (hγ : ∀ i < m, ∀ σ x, X σ x → 0 ≤ γ i σ x)
+    (hbudget : ∀ i < m, vertexNormPow p N u X (γ i) ≤ ε i ^ p) :
+    vertexNormPow p N u X (fun σ x =>
+      firstOverflowNoiseTail (S σ x) n K ρ (Δ σ x) (a σ x) m w (fun i => γ i σ x)) ≤
+        (∑ i ∈ range m, w i * ε i) ^ p :=
+  (vertexNormPow_firstOverflowNoiseTail_le S n K ρ Δ a m hNu X w γ hw hγ).trans
+    (vertexNormPow_sum_le_pow_sum hp hNu (range m) γ w ε
+      (fun i hi => hw i (mem_range.mp hi)) (fun i hi => hε i (mem_range.mp hi))
+      (fun i hi => hbudget i (mem_range.mp hi)))
+
+end Cslib.RowCompression

Complexity/Foundations/Probability/RootMetric/Minkowski.lean

@@ -0,0 +1,121 @@
+/-
+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.RootMetric
+import Mathlib.Analysis.MeanInequalities
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
+
+/-!
+# Finite Minkowski bounds for the integrated vertex norm
+
+The existing `vertexNormPow` is a normalized finite moment on retained sources. Applying
+Mathlib's finite Minkowski inequality to the joint environment/source domain gives a bound
+on finite sums with arbitrary correlations. The normalization may vanish, and the environment
+or retained source sets may be empty.
+
+The weighted budget theorem turns individual moment budgets into a bound by the power of
+their weighted sum. In particular, it introduces no factor counting the number of summands.
+
+## Main results
+
+* `Cslib.vertexNormPow_add_rpow_le`: the rooted triangle inequality.
+* `Cslib.vertexNormPow_sum_rpow_le`: the rooted finite-sum inequality.
+* `Cslib.vertexNormPow_sum_le_pow_sum`: a finite weighted sum of individual moment budgets.
+-/
+
+public section
+
+open Finset
+open scoped BigOperators
+
+namespace Cslib
+
+variable {Ω V I : Type*} [Fintype Ω] [Fintype V]
+  {p : ℕ} {N u : ℝ} {X : Ω → V → Prop} [∀ σ x, Decidable (X σ x)]
+
+private theorem vertexNormPow_eq_mul_sum (hp : p ≠ 0) (v : Ω → V → ℝ) :
+    vertexNormPow p N u X v =
+      ((N * u)⁻¹ * (Fintype.card Ω : ℝ)⁻¹) *
+        ∑ z : Ω × V, |if X z.1 z.2 then v z.1 z.2 else 0| ^ p := by
+  simp only [vertexNormPow, expect_eq_sum_div_card, card_univ, Fintype.sum_prod_type,
+    sum_filter, div_eq_mul_inv]
+  simp_rw [apply_ite (fun t : ℝ => |t| ^ p), abs_zero, zero_pow hp]
+  ring
+
+/-- Minkowski's inequality in the existing normalized vertex norm. The two arrays may use
+the same environment and retained source set. -/
+theorem vertexNormPow_add_rpow_le (hp : p ≠ 0) (hNu : 0 ≤ N * u)
+    (f g : Ω → V → ℝ) :
+    vertexNormPow p N u X (fun σ x => f σ x + g σ x) ^ (p⁻¹ : ℝ) ≤
+      vertexNormPow p N u X f ^ (p⁻¹ : ℝ) +
+        vertexNormPow p N u X g ^ (p⁻¹ : ℝ) := by
+  let c : ℝ := (N * u)⁻¹ * (Fintype.card Ω : ℝ)⁻¹
+  have hc : 0 ≤ c := mul_nonneg (inv_nonneg.mpr hNu) (by positivity)
+  let F : Ω × V → ℝ := fun z => if X z.1 z.2 then f z.1 z.2 else 0
+  let G : Ω × V → ℝ := fun z => if X z.1 z.2 then g z.1 z.2 else 0
+  have hmask (z : Ω × V) :
+      (if X z.1 z.2 then f z.1 z.2 + g z.1 z.2 else 0) = F z + G z := by
+    simp only [F, G]
+    split_ifs <;> simp
+  have hp' : (1 : ℝ) ≤ p := by exact_mod_cast Nat.one_le_iff_ne_zero.mpr hp
+  have h := Real.Lp_add_le (univ : Finset (Ω × V)) F G hp'
+  simp only [Real.rpow_natCast, one_div] at h
+  rw [vertexNormPow_eq_mul_sum hp, vertexNormPow_eq_mul_sum hp,
+    vertexNormPow_eq_mul_sum hp]
+  simp_rw [hmask]
+  change (c * ∑ z, |F z + G z| ^ p) ^ (p⁻¹ : ℝ) ≤
+    (c * ∑ z, |F z| ^ p) ^ (p⁻¹ : ℝ) + (c * ∑ z, |G z| ^ p) ^ (p⁻¹ : ℝ)
+  rw [Real.mul_rpow hc (by positivity), Real.mul_rpow hc (by positivity),
+    Real.mul_rpow hc (by positivity), ← mul_add]
+  exact mul_le_mul_of_nonneg_left h (Real.rpow_nonneg hc _)
+
+/-- Finite Minkowski inequality. No independence among the arrays is required. -/
+theorem vertexNormPow_sum_rpow_le (hp : p ≠ 0) (hNu : 0 ≤ N * u)
+    (s : Finset I) (f : I → Ω → V → ℝ) :
+    vertexNormPow p N u X (fun σ x => ∑ i ∈ s, f i σ x) ^ (p⁻¹ : ℝ) ≤
+      ∑ i ∈ s, vertexNormPow p N u X (f i) ^ (p⁻¹ : ℝ) := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp [vertexNormPow, hp]
+  | @insert i s hi ih =>
+    simp only [sum_insert hi]
+    exact (vertexNormPow_add_rpow_le hp hNu (f i) (fun σ x => ∑ j ∈ s, f j σ x)).trans
+      (add_le_add le_rfl ih)
+
+/-- A constant scalar factors out of the normalized moment with its absolute `p`-th power. -/
+theorem vertexNormPow_const_mul (w : ℝ) (f : Ω → V → ℝ) :
+    vertexNormPow p N u X (fun σ x => w * f σ x) = |w| ^ p * vertexNormPow p N u X f := by
+  simp only [vertexNormPow, abs_mul, mul_pow, ← mul_sum, ← mul_expect]
+  ring
+
+/-- Individual moment budgets control a weighted finite sum by the `p`-th power of the
+weighted sum of budgets, without a factor depending on the number of terms. -/
+theorem vertexNormPow_sum_le_pow_sum (hp : p ≠ 0) (hNu : 0 ≤ N * u)
+    (s : Finset I) (f : I → Ω → V → ℝ) (w ε : I → ℝ)
+    (hw : ∀ i ∈ s, 0 ≤ w i) (hε : ∀ i ∈ s, 0 ≤ ε i)
+    (hf : ∀ i ∈ s, vertexNormPow p N u X (f i) ≤ ε i ^ p) :
+    vertexNormPow p N u X (fun σ x => ∑ i ∈ s, w i * f i σ x) ≤
+      (∑ i ∈ s, w i * ε i) ^ p := by
+  have hroot := vertexNormPow_sum_rpow_le (X := X) (N := N) (u := u)
+    hp hNu s (fun i σ x => w i * f i σ x)
+  have hterm : ∀ i ∈ s,
+      vertexNormPow p N u X (fun σ x => w i * f i σ x) ^ (p⁻¹ : ℝ) ≤ w i * ε i := by
+    intro i hi
+    rw [vertexNormPow_const_mul, abs_of_nonneg (hw i hi),
+      Real.mul_rpow (pow_nonneg (hw i hi) _) (vertexNormPow_nonneg hNu _),
+      Real.pow_rpow_inv_natCast (hw i hi) hp]
+    apply mul_le_mul_of_nonneg_left _ (hw i hi)
+    exact (Real.rpow_le_rpow (vertexNormPow_nonneg hNu _) (hf i hi) (by positivity)).trans_eq
+      (Real.pow_rpow_inv_natCast (hε i hi) hp)
+  have h := pow_le_pow_left₀ (Real.rpow_nonneg (vertexNormPow_nonneg hNu _) _)
+    (hroot.trans (sum_le_sum hterm)) p
+  rwa [Real.rpow_inv_natCast_pow (vertexNormPow_nonneg hNu _) hp] at h
+
+end Cslib

ComplexityTests/OverflowMomentBudget.lean

@@ -0,0 +1,148 @@
+/-
+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.OverflowBudget
+import Complexity.Foundations.Data.Finset.Expect
+import Mathlib.LinearAlgebra.Matrix.Notation
+import Mathlib.Tactic.NormNum
+
+/-!
+# Tests for correlated moment budgets and actual overflow tails
+
+The active source, both noise arrays and the overflow event share one Boolean draw.
+At normalization `N = 1`, `u = 1/2`, the individual budgets are attained, so the
+weighted fourth-moment estimate is sharp. Values outside the retained source can be negative.
+An actual compression run then yields the strict tail comparison `21^4 ≤ 49^4`.
+-/
+
+namespace ComplexityTests.OverflowMomentBudget
+
+open Finset Cslib Cslib.RowCompression
+open scoped BigOperators
+
+private def active (σ : Bool) (_ : Fin 1) : Prop := σ = true
+
+private instance (σ : Bool) (x : Fin 1) : Decidable (active σ x) :=
+  inferInstanceAs (Decidable (σ = true))
+
+private def signal (i σ : Bool) (_ : Fin 1) : ℝ :=
+  if σ then if i then 2 else 1 else -100
+
+private def weight (i : Bool) : ℝ := if i then 5 else 3
+
+private def budget (i : Bool) : ℝ := if i then 2 else 1
+
+private theorem signal_moment (i : Bool) :
+    vertexNormPow 4 1 (1 / 2) active (signal i) = budget i ^ 4 := by
+  unfold vertexNormPow
+  rw [Fintype.expect_bool]
+  cases i <;> norm_num [active, signal, budget]
+
+-- The common draw gives no independence, and the weighted Minkowski budget is attained.
+example : vertexNormPow 4 1 (1 / 2) active
+    (fun σ x => ∑ i : Bool, weight i * signal i σ x) = 28561 := by
+  unfold vertexNormPow
+  rw [Fintype.expect_bool]
+  norm_num [active, signal, weight, Fintype.sum_bool]
+
+example : vertexNormPow 4 1 (1 / 2) active
+    (fun σ x => ∑ i : Bool, weight i * signal i σ x) ≤ 28561 := by
+  have h := vertexNormPow_sum_le_pow_sum (X := active) (N := 1) (u := 1 / 2)
+    (by decide : 4 ≠ 0) (by norm_num) (univ : Finset Bool) signal weight budget
+    (by intro i _; cases i <;> norm_num [weight])
+    (by intro i _; cases i <;> norm_num [budget])
+    (fun i _ => (signal_moment i).le)
+  norm_num [weight, budget, Fintype.sum_bool] at h ⊢
+  exact h
+
+-- Scalars of either sign factor out with absolute value.
+example : vertexNormPow 4 1 (1 / 2) active (fun σ x => -3 * signal false σ x) = 81 := by
+  rw [vertexNormPow_const_mul, signal_moment]
+  norm_num [budget]
+
+-- The positive-moment sum theorem includes empty index sets and zero normalization.
+example : vertexNormPow 4 1 (1 / 2) active
+    (fun σ x => ∑ i ∈ (∅ : Finset Bool), signal i σ x) = 0 := by
+  simp [vertexNormPow]
+
+example : vertexNormPow 1 0 1 active
+    (fun σ x => ∑ i : Bool, signal i σ x) ≤ (0 : ℝ) := by
+  have h := vertexNormPow_sum_le_pow_sum (X := active) (N := 0) (u := 1)
+    (by decide : 1 ≠ 0) (by norm_num) (univ : Finset Bool) signal (fun _ => 1) (fun _ => 0)
+    (by intros; norm_num) (by intros; norm_num)
+    (by intros; simp [vertexNormPow])
+  simpa using h
+
+example : vertexNormPow 4 1 1 (fun (_ : Empty) (_ : Fin 1) => True)
+    (fun σ _ => nomatch σ) = 0 := by
+  simp [vertexNormPow]
+
+private def initial : State (Fin 1) := { defaultValue := 0, row := 0 }
+
+private def increments (σ : Bool) (i : ℕ) (_ : Fin 1) : Fin 2 → ℝ :=
+  if σ = true ∧ i = 1 then ![4, -2] else 0
+
+private def noiseBudget (i : ℕ) : ℝ := if i = 0 then 4 else 3
+
+private def noise (i : ℕ) (σ : Bool) (_ : Fin 1) : ℝ :=
+  if σ then noiseBudget i else -100
+
+private theorem first_overflow :
+    IsFirstOverflow univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+      (increments true) 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 selected_tail :
+    firstOverflowNoiseTail univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+      (increments true) initial 2 (fun _ => 7) (fun i => noise i true 0) = 21 := by
+  have hevent (j : ℕ) :
+      IsFirstOverflow univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+        (increments true) initial j ↔ j = 1 :=
+    ⟨fun hj => hj.unique first_overflow, fun h => h ▸ first_overflow⟩
+  unfold firstOverflowNoiseTail
+  simp only [hevent]
+  norm_num [sum_range_succ, noise, noiseBudget, Finset.sum_Ico_succ_top]
+
+private theorem noise_moment (i : ℕ) :
+    vertexNormPow 4 1 (1 / 2) active (noise i) = noiseBudget i ^ 4 := by
+  unfold vertexNormPow
+  rw [Fintype.expect_bool]
+  by_cases hi : i = 0 <;> norm_num [active, noise, noiseBudget, hi]
+
+-- This consumes the budget theorem for the actual signed-increment compression run.
+example : vertexNormPow 4 1 (1 / 2) active
+    (fun σ _ => firstOverflowNoiseTail univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+      (increments σ) initial 2 (fun _ => 7) (fun i => noise i σ 0)) ≤ 5764801 := by
+  have h := vertexNormPow_firstOverflowNoiseTail_le_pow_sum
+    (fun (_ : Bool) (_ : Fin 1) => (univ : Finset (Fin 1)))
+    (fun _ => 1) (fun _ => 1) (fun _ => 1) (fun σ _ => increments σ)
+    (fun _ _ => initial) 2 (by decide : 4 ≠ 0) (N := 1) (u := 1 / 2) (by norm_num)
+    active (fun _ => 7) noiseBudget noise
+    (by intros; norm_num)
+    (by intro i _; simp only [noiseBudget]; split_ifs <;> norm_num)
+    (by intro i _ σ x hx; change σ = true at hx; subst σ
+        simp only [noise, ↓reduceIte, noiseBudget]; split_ifs <;> norm_num)
+    (fun i _ => (noise_moment i).le)
+  norm_num [sum_range_succ, noiseBudget] at h
+  simpa [noise] using h
+
+example : vertexNormPow 4 1 (1 / 2) active
+    (fun σ _ => firstOverflowNoiseTail univ (fun _ => 1) (fun _ => 1) (fun _ => 1)
+      (increments σ) initial 2 (fun _ => 7) (fun i => noise i σ 0)) = 194481 := by
+  unfold vertexNormPow
+  rw [Fintype.expect_bool]
+  dsimp only
+  rw [selected_tail]
+  norm_num [active]
+
+end ComplexityTests.OverflowMomentBudget