feat(logspace): bound source release through correction atoms

Complexity.lean

@@ -2733,6 +2733,7 @@ public import Complexity.Foundations.Probability.Gaussian.Sheppard
 public import Complexity.Foundations.Probability.HierarchyParams
 public import Complexity.Foundations.Probability.RootMetric
 public import Complexity.Foundations.Probability.SecondMoment
+public import Complexity.Foundations.Probability.SourceRelease
 public import Complexity.Foundations.Probability.StochasticAtom
 public import Complexity.Foundations.Quantum.Measurement
 public import Complexity.Foundations.Relation.InductiveCounting

Complexity/Foundations/Probability/RootMetric.lean

@@ -71,7 +71,7 @@ variable (s : ℕ) (N u : ℝ) (X Y : Ω → V → Prop) [∀ σ v, Decidable (X
 
 /-- The `s`-th power `‖Z‖^s_{u,a;s}` of the integrated row norm of a random table
 [OpenAI2026LogSpace, (5.19)]. -/
-noncomputable def rowNormPow (Z : Ω → V → V → ℝ) : ℝ :=
+@[expose] noncomputable def rowNormPow (Z : Ω → V → V → ℝ) : ℝ :=
   (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), |Z σ x y| ^ s
 
 /-- The `s`-th power `d_{u,a}(H, H')^s` of the root distance of two random tables
@@ -81,7 +81,7 @@ noncomputable def rootDistPow (H H' : Ω → V → V → ℝ) : ℝ :=
 
 /-- The `s`-th power `‖v‖^s_{u;s}` of the integrated norm of a random vertex array
 [OpenAI2026LogSpace, (5.20)]. -/
-noncomputable def vertexNormPow (v : Ω → V → ℝ) : ℝ :=
+@[expose] noncomputable def vertexNormPow (v : Ω → V → ℝ) : ℝ :=
   (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), |v σ x| ^ s
 
 end Definitions

Complexity/Foundations/Probability/SourceRelease.lean

@@ -0,0 +1,163 @@
+/-
+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
+public import Complexity.Foundations.Probability.CorrectionAtom
+import Mathlib.Algebra.Order.BigOperators.Expect
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Positivity
+
+/-!
+# Source release through a bounded incoming relation
+
+In a product of stochastic tables, the right factor is queried at an intermediate vertex `z`.
+Its error is a common table `e σ z y`: it does not take the old source `x` as an extra argument.
+If the left support relation has at most `K` retained sources at each `z`, double counting
+eliminates the old source at cost `K`. Changing the source normalization from `1 / u` to
+`1 / f` then contributes exactly `f / u`.
+
+This is the explicit source-release inequality in the proof of [OpenAI2026LogSpace, Lemma 7.3],
+in the September 23, 2026 source version at `openai/math` commit `7ef5c0cc`. Here the indicators
+`X_u`, `Z_f`, and `Y_b` are finite-set restrictions `X`, `Z`, and `Y`; the left normalization
+is written `(N * u)⁻¹`. The exponent is any natural number, including the paper's `s = 8`.
+The theorem proves the source-domain comparison, not the remaining scale comparisons or the
+recursive estimator of that lemma. No independence hypothesis is imposed: the support relation,
+channels, and error may all depend on the same environment `σ`.
+
+The correction-atom corollaries discharge the incoming-degree hypothesis using
+`Matrix.card_filter_correctionAtom_col_ne_zero_lt`. An arbitrary map from the full environment
+to the atom's two seeds allows additional shared coordinates in the right error.
+
+## Main results
+
+* `Finset.sum_sum_filter_le_mul_sum_of_card_le`: the finite double-counting inequality.
+* `Cslib.sourceRelease_le_rowNormPow`, `Cslib.sourceRelease_le_vertexNormPow`: the exact
+  `K * (f / u)` cost for a common right table or vector.
+* `Matrix.correctionAtom_sourceRelease_le_rowNormPow`,
+  `Matrix.correctionAtom_sourceRelease_le_vertexNormPow`: source release for correction atoms.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  proof of Lemma 7.3 (preprint, not peer reviewed).
+-/
+
+public section
+
+open Finset
+open scoped BigOperators
+
+namespace Finset
+
+/-- A nonnegative weight at a target is counted at most `K` times if that target has at most
+`K` incoming sources. The weight is common to all sources. -/
+theorem sum_sum_filter_le_mul_sum_of_card_le {α β : Type*} (S : Finset α) (T : Finset β)
+    (P : α → β → Prop) [∀ x z, Decidable (P x z)] {w : β → ℝ} {K : ℕ}
+    (hw : ∀ z ∈ T, 0 ≤ w z) (hK : ∀ z ∈ T, #{x ∈ S | P x z} ≤ K) :
+    ∑ x ∈ S, ∑ z ∈ T with P x z, w z ≤ K * ∑ z ∈ T, w z := by
+  calc
+    ∑ x ∈ S, ∑ z ∈ T with P x z, w z =
+        ∑ z ∈ T, (#{x ∈ S | P x z} : ℝ) * w z := by
+      simp only [sum_filter]
+      rw [sum_comm]
+      refine sum_congr rfl fun z _ => ?_
+      rw [← sum_filter, sum_const, nsmul_eq_mul]
+    _ ≤ ∑ z ∈ T, (K : ℝ) * w z := by
+      refine sum_le_sum fun z hz => mul_le_mul_of_nonneg_right ?_ (hw z hz)
+      exact_mod_cast hK z hz
+    _ = K * ∑ z ∈ T, w z := (mul_sum ..).symm
+
+end Finset
+
+namespace Cslib
+
+variable {Ω V : Type*} [Fintype Ω] [Fintype V]
+  {s : ℕ} {N u f : ℝ} {X Z Y : Ω → V → Prop}
+  [∀ σ x, Decidable (X σ x)] [∀ σ z, Decidable (Z σ z)] [∀ σ y, Decidable (Y σ y)]
+
+/-- **Source release for a common right table**, the explicit double-counting estimate in the
+proof of [OpenAI2026LogSpace, Lemma 7.3]. A pointwise incoming cap costs `K * (f / u)` in norm
+power. The error and the relation may depend on the same environment. -/
+theorem sourceRelease_le_rowNormPow (hN : 0 < N) (hu : 0 < u) (hf : 0 < f)
+    (P : Ω → V → V → Prop) [∀ σ x z, Decidable (P σ x z)] {K : ℕ}
+    (hK : ∀ σ z, Z σ z → #{x ∈ ({x | X σ x} : Finset V) | P σ x z} ≤ K)
+    (e : Ω → V → V → ℝ) :
+    (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V),
+        ∑ z ∈ ({z | Z σ z} : Finset V) with P σ x z,
+          ∑ y ∈ ({y | Y σ y} : Finset V), |e σ z y| ^ s ≤
+      K * (f / u) * rowNormPow s N f Z Y e := by
+  calc
+    _ ≤ (N * u)⁻¹ * 𝔼 σ, (K : ℝ) *
+        ∑ z ∈ ({z | Z σ z} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V),
+          |e σ z y| ^ s := by
+      refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (by positivity)
+      refine sum_sum_filter_le_mul_sum_of_card_le _ _ (P σ) (fun _ _ => by positivity) ?_
+      intro z hz
+      exact hK σ z (by simpa using hz)
+    _ = _ := by
+      rw [← mul_expect, rowNormPow]
+      field_simp
+
+/-- The vector version of source release, used for the right error in a reward update. -/
+theorem sourceRelease_le_vertexNormPow (hN : 0 < N) (hu : 0 < u) (hf : 0 < f)
+    (P : Ω → V → V → Prop) [∀ σ x z, Decidable (P σ x z)] {K : ℕ}
+    (hK : ∀ σ z, Z σ z → #{x ∈ ({x | X σ x} : Finset V) | P σ x z} ≤ K)
+    (v : Ω → V → ℝ) :
+    (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V),
+        ∑ z ∈ ({z | Z σ z} : Finset V) with P σ x z, |v σ z| ^ s ≤
+      K * (f / u) * vertexNormPow s N f Z v := by
+  calc
+    _ ≤ (N * u)⁻¹ * 𝔼 σ, (K : ℝ) * ∑ z ∈ ({z | Z σ z} : Finset V), |v σ z| ^ s := by
+      refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (by positivity)
+      refine sum_sum_filter_le_mul_sum_of_card_le _ _ (P σ) (fun _ _ => by positivity) ?_
+      intro z hz
+      exact hK σ z (by simpa using hz)
+    _ = _ := by
+      rw [← mul_expect, vertexNormPow]
+      field_simp
+
+end Cslib
+
+namespace Matrix
+
+variable {Ω V ι κ : Type*} [Fintype Ω] [Fintype V] [Fintype ι] [Fintype κ]
+  {s K Kc : ℕ} {N u f : ℝ} {I : ℝ → ℝ → ℝ} {τ Q h ρ : ℝ → ℝ}
+  {G : Matrix V V ℝ} {g₀ : V → ℝ} {X : ι → V → Prop} {Y Yt : κ → V → Prop}
+  [∀ t x, Decidable (X t x)] [∀ t z, Decidable (Y t z)] [∀ t z, Decidable (Yt t z)]
+
+/-- Source release for an actual correction atom. Its incoming gate supplies the degree bound;
+no separate sparsity or independence assumption is needed. `draw` selects the atom's seeds
+from the full shared environment. -/
+theorem correctionAtom_sourceRelease_le_rowNormPow (draw : Ω → ι × κ)
+    (Yb : Ω → V → Prop) [∀ σ y, Decidable (Yb σ y)] (hN : 0 < N) (hu : 0 < u) (hf : 0 < f)
+    (hKc : 0 < Kc) (hIQ : ∀ v r, Q v ≠ 0 → ρ r ≠ 0 → I v r = 1)
+    {g : ℝ} (hg : g ≤ 1) (hτ : ∀ r, g ≤ r → τ r = 0) (e : Ω → V → V → ℝ) :
+    (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X (draw σ).1 x} : Finset V),
+        ∑ z ∈ ({z | Yt (draw σ).2 z} : Finset V)
+          with correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ (draw σ) x z ≠ 0,
+            ∑ y ∈ ({y | Yb σ y} : Finset V), |e σ z y| ^ s ≤
+      Kc * (f / u) * Cslib.rowNormPow s N f (fun σ z => Yt (draw σ).2 z) Yb e := by
+  refine Cslib.sourceRelease_le_rowNormPow hN hu hf _ (fun σ z _ => ?_) e
+  exact (card_filter_correctionAtom_col_ne_zero_lt hKc hIQ hg hτ (draw σ) z).le
+
+/-- Source release for a common right vector through a correction atom, with its incoming
+degree bound supplied by the incoming gate. -/
+theorem correctionAtom_sourceRelease_le_vertexNormPow (draw : Ω → ι × κ)
+    (hN : 0 < N) (hu : 0 < u) (hf : 0 < f) (hKc : 0 < Kc)
+    (hIQ : ∀ v r, Q v ≠ 0 → ρ r ≠ 0 → I v r = 1)
+    {g : ℝ} (hg : g ≤ 1) (hτ : ∀ r, g ≤ r → τ r = 0) (v : Ω → V → ℝ) :
+    (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X (draw σ).1 x} : Finset V),
+        ∑ z ∈ ({z | Yt (draw σ).2 z} : Finset V)
+          with correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ (draw σ) x z ≠ 0,
+            |v σ z| ^ s ≤
+      Kc * (f / u) * Cslib.vertexNormPow s N f (fun σ z => Yt (draw σ).2 z) v := by
+  refine Cslib.sourceRelease_le_vertexNormPow hN hu hf _ (fun σ z _ => ?_) v
+  exact (card_filter_correctionAtom_col_ne_zero_lt hKc hIQ hg hτ (draw σ) z).le
+
+end Matrix

ComplexityTests/SourceRelease.lean

@@ -0,0 +1,138 @@
+/-
+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.SourceRelease
+import Mathlib.LinearAlgebra.Matrix.Notation
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum
+
+/-!
+# Tests for source release
+
+The examples check the double-counting bound, a sharp `f / u = 2` cost with an environment-
+dependent relation and error, and source release through a nonzero concrete correction atom.
+-/
+
+namespace ComplexityTests.SourceRelease
+
+open Finset Matrix Cslib
+open scoped BigOperators
+
+-- Exactly two of three sources contribute to both targets, whose weights are `3` and `7`.
+example : ∑ x : Fin 3, ∑ z ∈ (univ : Finset (Fin 2)) with x ≠ 2, (![3, 7] : Fin 2 → ℝ) z ≤
+    2 * ∑ z : Fin 2, (![3, 7] : Fin 2 → ℝ) z := by
+  refine sum_sum_filter_le_mul_sum_of_card_le univ univ (fun x _ => x ≠ 2) ?_ ?_
+  · intro z _
+    fin_cases z <;> norm_num
+  · intro z _
+    decide
+
+/-- Both the support relation and the error depend on this same two-point environment. -/
+private def error (σ : Fin 2) (_ _ : Fin 2) : ℝ := if σ = 0 then 2 else 3
+
+private noncomputable def releasedTableError : ℝ :=
+  (2 * (1 / 2))⁻¹ * 𝔼 σ : Fin 2, ∑ x : Fin 2,
+    ∑ z ∈ ({z | z = σ} : Finset (Fin 2)) with x = σ,
+      ∑ y ∈ ({y | y = 0} : Finset (Fin 2)), |error σ z y| ^ 4
+
+-- The degree bound is one, while the rate change doubles the child's norm power.
+example : releasedTableError ≤ 2 * rowNormPow 4 2 1 (fun σ z : Fin 2 => z = σ)
+    (fun (_ : Fin 2) (y : Fin 2) => y = 0) error := by
+  have h := sourceRelease_le_rowNormPow (s := 4) (N := 2) (u := 1 / 2) (f := 1)
+    (X := fun (_ : Fin 2) (_ : Fin 2) => True) (Z := fun σ z => z = σ)
+    (Y := fun _ y => y = 0) (by norm_num) (by norm_num) (by norm_num)
+    (fun σ x _ => x = σ) (K := 1) (fun σ z _ => by simp [filter_eq']) error
+  simpa [releasedTableError] using h
+
+example : releasedTableError = 97 / 2 := by
+  norm_num [releasedTableError, error, expect_eq_sum_div_card, sum_filter, Fin.sum_univ_two,
+    filter_eq']
+
+example : rowNormPow 4 2 1 (fun σ z : Fin 2 => z = σ)
+    (fun (_ : Fin 2) (y : Fin 2) => y = 0) error = 97 / 4 := by
+  norm_num [rowNormPow, error, expect_eq_sum_div_card, sum_filter, Fin.sum_univ_two, filter_eq']
+
+-- The vector API uses the same common environment, with no independence assumptions.
+example : (2 * (1 / 2) : ℝ)⁻¹ * 𝔼 σ : Fin 2, ∑ x : Fin 2,
+      ∑ z ∈ ({z | z = σ} : Finset (Fin 2)) with x = σ, |error σ z 0| ^ 4 ≤
+    2 * vertexNormPow 4 2 1 (fun σ z : Fin 2 => z = σ) (fun σ z => error σ z 0) := by
+  have h := sourceRelease_le_vertexNormPow (s := 4) (N := 2) (u := 1 / 2) (f := 1)
+    (X := fun (_ : Fin 2) (_ : Fin 2) => True) (Z := fun σ z => z = σ)
+    (by norm_num) (by norm_num) (by norm_num) (fun σ x _ => x = σ) (K := 1)
+    (fun σ z _ => by simp [filter_eq']) (fun σ z => error σ z 0)
+  simpa using h
+
+/-! ### A concrete correction atom -/
+
+/-- A single nonzero entry, from vertex `0` to vertex `1`. -/
+private def G (x z : Fin 2) : ℝ := if x = 0 ∧ z = 1 then 1 else 0
+
+private noncomputable def score (v _ : ℝ) : ℝ := if v = 0 then 0 else 1
+
+private noncomputable def gate (r : ℝ) : ℝ := if r < 1 then 1 else 0
+
+private abbrev full (_ : Unit) (_ : Fin 2) : Prop := True
+
+private noncomputable def atom (d : Unit × Unit) (x z : Fin 2) : ℝ :=
+  correctionAtom score gate 3 2 1 G full full full id (fun _ => 1) (fun _ => 1) (fun _ => 1) d x z
+
+private theorem score_one (v r : ℝ) (hv : id v ≠ 0) (_ : (1 : ℝ) ≠ 0) : score v r = 1 := by
+  simpa only [id_eq, score, ite_eq_right_iff, zero_ne_one, imp_false] using hv
+
+private theorem gate_zero (r : ℝ) (hr : 1 ≤ r) : gate r = 0 := by
+  exact ite_eq_right (not_lt.mpr hr)
+
+private theorem incoming_one (z : Fin 2) :
+    incomingGate score gate 3 2 1 G univ univ z = 1 := by
+  have hcard : #{x : Fin 2 | 1 ≤ auxScore score 3 1 G univ x z} < 2 := by
+    fin_cases z <;> norm_num [auxScore, score, G, univ_fin2, filter_insert, filter_singleton]
+  have hlt : kthLargest 2 univ (fun x => auxScore score 3 1 G univ x z) < 1 := by
+    exact lt_of_not_ge fun h => hcard.not_ge ((le_kthLargest_iff (by decide) zero_lt_one).mp h)
+  exact ite_eq_left hlt
+
+-- The test is nonzero: the atom keeps the unique edge and its normalizer is one.
+private theorem atom_eq (d : Unit × Unit) (x z : Fin 2) : atom d x z = G x z := by
+  have hnorm : correctionNormalizer score gate 3 2 1 G full full full (fun _ => 1)
+      (fun _ => 1) x z = 1 := by
+    simp [correctionNormalizer, correctionPrep, rowGate, full, incoming_one]
+  norm_num [atom, correctionAtom, rowGate, full, incoming_one, hnorm]
+
+example : atom ((), ()) 0 1 = 1 := by rw [atom_eq]; norm_num [G]
+
+-- An additional environment coordinate can govern the right error without changing atom seeds.
+-- The incoming cap is discharged by the correction-atom theorem, not supplied as an assumption.
+example : (2 * (1 / 2) : ℝ)⁻¹ * 𝔼 σ : Fin 2, ∑ x : Fin 2,
+      ∑ z ∈ (univ : Finset (Fin 2)) with atom ((), ()) x z ≠ 0,
+        ∑ y : Fin 2, |error σ z y| ^ 4 ≤
+    4 * rowNormPow 4 2 1 (fun (_ : Fin 2) (_ : Fin 2) => True)
+      (fun _ _ => True) error := by
+  have h := correctionAtom_sourceRelease_le_rowNormPow (K := 3) (Kc := 2) (s := 4)
+    (N := 2) (u := 1 / 2) (f := 1) (I := score) (τ := gate) (Q := id)
+    (h := fun _ => 1) (ρ := fun _ => 1) (G := G) (g₀ := fun _ => 1)
+    (X := full) (Y := full) (Yt := full) (fun _ : Fin 2 => ((), ())) (fun _ _ => True)
+    (by norm_num) (by norm_num) (by norm_num) (by decide) score_one (g := 1) le_rfl gate_zero error
+  norm_num [full, atom] at h ⊢
+  exact h
+
+example : (2 * (1 / 2) : ℝ)⁻¹ * 𝔼 σ : Fin 2, ∑ x : Fin 2,
+      ∑ z ∈ (univ : Finset (Fin 2)) with atom ((), ()) x z ≠ 0, |error σ z 0| ^ 4 ≤
+    4 * vertexNormPow 4 2 1 (fun (_ : Fin 2) (_ : Fin 2) => True)
+      (fun σ z => error σ z 0) := by
+  have h := correctionAtom_sourceRelease_le_vertexNormPow (K := 3) (Kc := 2) (s := 4)
+    (N := 2) (u := 1 / 2) (f := 1) (I := score) (τ := gate) (Q := id)
+    (h := fun _ => 1) (ρ := fun _ => 1) (G := G) (g₀ := fun _ => 1)
+    (X := full) (Y := full) (Yt := full) (fun _ : Fin 2 => ((), ()))
+    (by norm_num) (by norm_num) (by norm_num) (by decide) score_one (g := 1) le_rfl gate_zero
+    (fun σ z => error σ z 0)
+  norm_num [full, atom] at h ⊢
+  exact h
+
+-- The analogous vector error has positive mass, equal to `E[2^4, 3^4] = 97/2`.
+example : (2 * (1 / 2) : ℝ)⁻¹ * 𝔼 σ : Fin 2, ∑ x : Fin 2,
+      ∑ z ∈ (univ : Finset (Fin 2)) with atom ((), ()) x z ≠ 0, |error σ z 0| ^ 4 = 97 / 2 := by
+  simp only [atom_eq]
+  norm_num [error, G, expect_eq_sum_div_card, sum_filter, Fin.sum_univ_two, filter_eq']
+
+end ComplexityTests.SourceRelease