From dfa6f5b694d2f775d95140608e0db0a064cf0d26 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:36:11 +0000 Subject: [PATCH 1/4] feat(logspace): bound source release through correction atoms Prove the finite double-counting inequality in the source-domain part of OpenAI2026LogSpace Lemma 7.3 and its exact K * (f / u) cost in integrated table and vector norms. Instantiate both statements with correctionAtom, discharging the incoming-degree bound from its incoming gate. Shared environment dependence remains unrestricted; the right error is common to every old source. Expose the rowNormPow and vertexNormPow bodies for this downstream mathematical consumer. No definitions or theorem statements change. Validation against base 2d1638ce: direct Lean elaboration with project options and warnings as errors passed for RootMetric, SourceRelease, ComplexityTests.SourceRelease and the existing ComplexityTests.RootMetric (covering AtomCutoffs and RootError). Outputs were private; dependencies were read-only. Hygiene with --check-simp and git diff --check passed. The changed-file lint requires the absent ComplexityAbstracts.ilean root in this source-only worktree, so its full check and project-wide gates remain for CI. Aggregate imports are left to the integrating coordinator. Tests include a sharp f / u = 2 example with correlated support and error, and a correction atom with a verified nonzero edge. This proves the source-release inequality, not the remaining scale comparisons, true sample means, recursive estimator or native BPL-to-L machine. AI assistance: OpenAI Codex implemented and checked this change. Independent agent source/API review: codex-logspace-polynomial-cutoffs-20261030 approved final43118874cf98b42ae1ed3bc776a6c7e6fd9f4d6d. Publication adds only the generated aggregate import. Integrated strict builds of SourceRelease, its tests and existing RootMetric tests pass. Full gates run in PR CI. --- Complexity.lean | 4 + .../Foundations/Probability/RootMetric.lean | 4 +- .../Probability/SourceRelease.lean | 163 ++++++++++++++++++ ComplexityTests/SourceRelease.lean | 138 +++++++++++++++ 4 files changed, 307 insertions(+), 2 deletions(-) create mode 100644 Complexity/Foundations/Probability/SourceRelease.lean create mode 100644 ComplexityTests/SourceRelease.lean diff --git a/Complexity.lean b/Complexity.lean index 9a3bc3cde..2ddb0cb3a 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2352,6 +2352,9 @@ public import Complexity.Foundations.Analysis.LpNorm 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.Floors +public import Complexity.Foundations.Analysis.RowCompression.Iteration public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos public import Complexity.Foundations.Analysis.SpecialFunctions.SmoothSwitch public import Complexity.Foundations.BooleanAnalysis.Bernoulli @@ -2733,6 +2736,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 diff --git a/Complexity/Foundations/Probability/RootMetric.lean b/Complexity/Foundations/Probability/RootMetric.lean index 419b8cccd..651f7bbf2 100644 --- a/Complexity/Foundations/Probability/RootMetric.lean +++ b/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 diff --git a/Complexity/Foundations/Probability/SourceRelease.lean b/Complexity/Foundations/Probability/SourceRelease.lean new file mode 100644 index 000000000..0df6d50d1 --- /dev/null +++ b/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 diff --git a/ComplexityTests/SourceRelease.lean b/ComplexityTests/SourceRelease.lean new file mode 100644 index 000000000..466bb1d79 --- /dev/null +++ b/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 From 755e8f673310980b206af68e718fa73d5fbe9b97 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:49:04 +0000 Subject: [PATCH 2/4] fix(logspace): keep source-release aggregate independent of compression Remove three stray aggregate imports introduced during local integration. Source-release proofs, APIs and tests remain unchanged. The committed import graph is now checked before publication. --- Complexity.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Complexity.lean b/Complexity.lean index 2ddb0cb3a..fdc2c232d 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2352,9 +2352,6 @@ public import Complexity.Foundations.Analysis.LpNorm 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.Floors -public import Complexity.Foundations.Analysis.RowCompression.Iteration public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos public import Complexity.Foundations.Analysis.SpecialFunctions.SmoothSwitch public import Complexity.Foundations.BooleanAnalysis.Bernoulli From b9868847c6efc58cfdf516553801e873a277f7a2 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:02:38 +0000 Subject: [PATCH 3/4] feat(logspace): prove true sampled product means Prove the direct dense and correction-dense mean identities from the actual atom definitions on their finite conditioning slices. The exact terminal density ratio changes to the nested usage slice, and f / pi_f cancels the intermediate retention density. Finite product averages factorize because the true right dense atom uses only the terminal seed. Both atom normalizations are derived from the existing gate and pair-count hypotheses, rather than assumed as mean contracts. This implements the direct/product part of OpenAI2026LogSpace Lemma 7.1 at pinned source revision 7ef5c0cc, before division by the parent scale. Copy, detector, reward and conditional-walk assembly remain separate. It makes no estimator-error or machine-space claim. Validation against source-release 43118874: TrueSampleMeans and ComplexityTests.TrueSampleMeans elaborate with project options and warnings as errors, using private outputs and read-only dependencies. Hygiene with --check-simp and git diff --check passed. Full project gates and import aggregate registration remain for the integrating coordinator and CI. The concrete example has middle hit probability 1/2, terminal broad density 1/2 and usage density 1/4. Both correction factors equal two; the active sample is 2/3 and the conditional product mean is 1/6. All gate, pair-count, subset and density hypotheses are discharged. AI assistance: OpenAI Codex implemented and checked this change. Independent agent source/API review: codex-logspace-polynomial-cutoffs-20261030 approved 9c1014a804ed32d06ba499196f460987b6a3d87d against the pinned Lemma7.1. Publication preserves the reviewed source/tests and adds only generated import registration. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --- Complexity.lean | 1 + .../Probability/TrueSampleMeans.lean | 233 ++++++++++++++++++ ComplexityTests/TrueSampleMeans.lean | 158 ++++++++++++ 3 files changed, 392 insertions(+) create mode 100644 Complexity/Foundations/Probability/TrueSampleMeans.lean create mode 100644 ComplexityTests/TrueSampleMeans.lean diff --git a/Complexity.lean b/Complexity.lean index fdc2c232d..23713eb44 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2735,6 +2735,7 @@ 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.Probability.TrueSampleMeans public import Complexity.Foundations.Quantum.Measurement public import Complexity.Foundations.Relation.InductiveCounting public import Complexity.Foundations.Relation.RelatesWithinSteps diff --git a/Complexity/Foundations/Probability/TrueSampleMeans.lean b/Complexity/Foundations/Probability/TrueSampleMeans.lean new file mode 100644 index 000000000..90e504c52 --- /dev/null +++ b/Complexity/Foundations/Probability/TrueSampleMeans.lean @@ -0,0 +1,233 @@ +/- +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.CorrectionAtom +import Mathlib.Algebra.BigOperators.Field +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# True means of sampled atom products + +The direct and correction--dense sample terms of [OpenAI2026LogSpace, Lemma 7.1] use a broad +terminal conditioning slice and a possibly narrower usage slice. Their exact retention-density +ratio changes the conditioning. In a product, a second ratio cancels the sampling of the +intermediate vertex. + +These results use the concrete `Matrix.denseAtom` and `Matrix.correctionAtom` definitions. +The true dense atom is a function of the terminal seed alone, while the correction atom uses +the source and intermediate seeds. Thus the required factorization follows from finite product +averages. No independence of estimated factors, estimator correctness, or machine certificate +is assumed. + +The formulas are the raw direct and product terms before division by the parent first-channel +scale. Copy projections, detector and reward assembly, and the conditional-walk schedule remain +separate parts of the estimator construction. + +## Main results + +* `Finset.expect_mul_dens_div_of_subset`: change a finite conditioning slice by its exact + density ratio, for a function supported on the smaller slice. +* `Matrix.expect_denseAtom_change_usage`: the importance-weighted dense-atom mean. +* `Matrix.expect_correctionAtom_unconditioned`: the correction-atom mean when the intermediate + seed is unconditioned. +* `Matrix.expect_correctionAtom_mul_denseAtom`: the exact correction--dense product mean on + the source/terminal conditioning slice, with the intermediate seed averaged over all draws. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 7.2, Lemma 7.1, September 23, 2026 revision `7ef5c0cc` (preprint, not peer reviewed). +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Finset + +/-- A function supported on `T ⊆ S` has the same mean after restricting to `T` and multiplying +its mean on `S` by the exact ratio of the two uniform densities. -/ +theorem expect_mul_dens_div_of_subset {Ω : Type*} [Fintype Ω] {S T : Finset Ω} + (hTS : T ⊆ S) (hT : T.Nonempty) (v : Ω → ℝ) + (hv : ∀ σ ∈ S, σ ∉ T → v σ = 0) : + 𝔼 σ ∈ S, ((dens S : ℝ) / dens T) * v σ = 𝔼 σ ∈ T, v σ := by + have hS : S.Nonempty := hT.mono hTS + have hScard : (#S : ℝ) ≠ 0 := by exact_mod_cast hS.card_ne_zero + have hTcard : (#T : ℝ) ≠ 0 := by exact_mod_cast hT.card_ne_zero + have hΩcard : (Fintype.card Ω : ℝ) ≠ 0 := by + have hpos : 0 < Fintype.card Ω := hT.card_pos.trans_le (card_le_univ T) + exact_mod_cast hpos.ne' + have hsum : ∑ σ ∈ S, v σ = ∑ σ ∈ T, v σ := (sum_subset hTS hv).symm + rw [← mul_expect, expect_eq_sum_div_card, expect_eq_sum_div_card, hsum, + dens_eq_card_div_card, dens_eq_card_div_card] + push_cast + field_simp + +/-- Averaging a supported function over the full seed space multiplies its conditional mean +by the exact retention density. -/ +theorem expect_eq_dens_mul_expect_of_eq_zero {Ω : Type*} [Fintype Ω] (S : Finset Ω) + (v : Ω → ℝ) (hv : ∀ σ ∉ S, v σ = 0) : + 𝔼 σ, v σ = (dens S : ℝ) * 𝔼 σ ∈ S, v σ := by + classical + have hmask : ∀ σ, v σ = if σ ∈ S then v σ else 0 := by + intro σ + split_ifs with hσ + · rfl + · exact hv σ hσ + calc + 𝔼 σ, v σ = 𝔼 σ, if σ ∈ S then v σ else 0 := + expect_congr rfl fun σ _ => hmask σ + _ = _ := by simpa only [NNRat.smul_def] using Fintype.expect_ite_mem S v + +end Finset + +namespace Matrix + +variable {V κ : Type*} [Fintype V] [Fintype κ] + +/-- The actual dense atom, averaged on a broader terminal slice, has the correct mean after +the exact density-ratio importance correction [OpenAI2026LogSpace, Lemma 7.1]. The sufficient +gate hypotheses are those of `Matrix.expect_denseAtom`. -/ +theorem expect_denseAtom_change_usage {Y Ya Yt : κ → V → Prop} + [∀ t v, Decidable (Y t v)] [∀ t v, Decidable (Ya t v)] [∀ t v, Decidable (Yt t v)] + {k h ρ : ℝ → ℝ} {K : ℕ} {b : ℝ} {G : Matrix V V ℝ} {x y : V} + (hYt : ∀ t, Yt t y → Ya t y) (hS : ({t | Yt t y} : Finset κ).Nonempty) + (hkh : ∀ d, k d ≠ 0 → h d = 1) (hρ0 : ∀ r, 0 ≤ ρ r) (hρ1 : ∀ r, ρ r ≤ 1) {η : ℝ} + (hη : 0 < η) (hρη : ∀ r, r ≤ η → ρ r = 1) (hb : 0 < b) (hG0 : ∀ w, 0 ≤ G x w) + {M : ℝ} (hGM : ∑ w, G x w ≤ M) {c : ℝ} (hc : 0 ≤ c) (hK : 2 * (1 + c * M / η) ≤ K) + (hpair : ∀ w, w ≠ y → (#{t | Yt t y ∧ Y t w} : ℝ) ≤ c * b * #{t | Yt t y}) : + 𝔼 t ∈ ({t | Ya t y} : Finset κ), + b * ((dens {t | Ya t y} : ℝ) / dens {t | Yt t y}) * denseAtom Y Yt k h ρ K b G t x y = + b * k (G x y / b) := by + have hsub : ({t | Yt t y} : Finset κ) ⊆ ({t | Ya t y} : Finset κ) := by + intro t ht + exact mem_filter.mpr ⟨mem_univ _, hYt t (by simpa using ht)⟩ + have hchange := expect_mul_dens_div_of_subset hsub hS (fun t => denseAtom Y Yt k h ρ K b G t x y) + (fun t _ ht => by + have hnot : ¬ Yt t y := by simpa using ht + simp [denseAtom, hnot]) + simp only [mul_assoc] + rw [← mul_expect, hchange, + expect_denseAtom hS hkh hρ0 hρ1 hη hρη hb hG0 hGM hc hK hpair] + +variable {ι : Type*} [Fintype ι] + +/-- The intermediate seed may be left unconditioned: the actual correction atom then has +mean `π_f * Q (G x z / f) * g₀ z`, where `π_f` is the exact density of its usage slice. +Its built-in mask supplies the support condition. -/ +theorem expect_correctionAtom_unconditioned {I : ℝ → ℝ → ℝ} {τ Q h ρ : ℝ → ℝ} + {K Kc : ℕ} {f : ℝ} {G : Matrix V V ℝ} {g₀ : V → ℝ} + {X : ι → V → Prop} {Z Zt : κ → V → Prop} + [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Z t v)] [∀ t v, Decidable (Zt t v)] + {x z : V} (hSx : ({s | X s x} : Finset ι).Nonempty) + (hSz : ({t | Zt t z} : Finset κ).Nonempty) (hQh : ∀ v, Q v ≠ 0 → h v = 1) + (hρ0 : ∀ r, 0 ≤ ρ r) (hρ1 : ∀ r, ρ r ≤ 1) {η : ℝ} (hη : 0 < η) + (hρη : ∀ r, r ≤ η → ρ r = 1) (hτ0 : ∀ r, 0 ≤ τ r) (hτ1 : ∀ r, τ r ≤ 1) + {τ₀ : ℝ} (hτ₀ : 0 ≤ τ₀) (hττ : ∀ r, r ≤ τ₀ → τ r = 1) {e : ℝ} + (hI : ∀ v r, v ≤ e → I v r = 0) (hf : 0 < f) (hG0 : ∀ w, 0 ≤ G x w) + {M : ℝ} (hGM : ∑ w, G x w ≤ M) {c : ℝ} (hc : 0 ≤ c) + (hK : 4 * (1 + c * M / η) ≤ K) + (hpairZ : ∀ w, w ≠ z → (#{t | Zt t z ∧ Z t w} : ℝ) ≤ c * f * #{t | Zt t z}) + {p : ℝ} (hp : 0 ≤ p) + (hpairX : ∀ w, w ≠ x → (#{s | X s x ∧ X s w} : ℝ) ≤ p * #{s | X s x}) + {B : ℝ} (hB : g₀ z ≠ 0 → p * #({w | e < G w z / f} : Finset V) ≤ B) + (hKc : 4 * (1 + B) ≤ Kc) : + 𝔼 d ∈ ({s | X s x} : Finset ι) ×ˢ (univ : Finset κ), + correctionAtom I τ K Kc f G X Z Zt Q h ρ g₀ d x z = + (dens {t | Zt t z} : ℝ) * (Q (G x z / f) * g₀ z) := by + have hmean := expect_correctionAtom hSx hSz hQh hρ0 hρ1 hη hρη hτ0 hτ1 hτ₀ hττ hI + hf hG0 hGM hc hK hpairZ hp hpairX hB hKc + have hsupport : ∀ s, (𝔼 t, correctionAtom I τ K Kc f G X Z Zt Q h ρ g₀ (s, t) x z) = + (dens {t | Zt t z} : ℝ) * 𝔼 t ∈ ({t | Zt t z} : Finset κ), + correctionAtom I τ K Kc f G X Z Zt Q h ρ g₀ (s, t) x z := by + intro s + refine expect_eq_dens_mul_expect_of_eq_zero _ _ fun t ht => ?_ + have hnot : ¬ Zt t z := by simpa using ht + simp [correctionAtom, hnot] + rw [expect_product] + simp_rw [hsupport] + rw [← mul_expect, ← expect_product', hmean] + +/-- **The true correction--dense product mean** [OpenAI2026LogSpace, Lemma 7.1]. Average the +actual sample over the source slice, all intermediate seeds, and the broad terminal slice. +The terminal density ratio changes to the usage slice; `f / πf` cancels intermediate sampling. +The result is the product of the two deterministic entries in their original matrix units. + +The uniform intermediate hit probability is stated as the actual density equality `hZπ`. +All atom normalizations follow from their gate and pair-count hypotheses; none are postulated +as mean identities. The true right atom only uses the third seed coordinate. -/ +theorem expect_correctionAtom_mul_denseAtom {υ : Type*} [Fintype υ] + {I : ℝ → ℝ → ℝ} {τ Q hF ρF k hB ρB : ℝ → ℝ} {KF Kc KB : ℕ} + {f b πf : ℝ} {G H : Matrix V V ℝ} {g₀ : V → ℝ} + {X : ι → V → Prop} {Z Zt : κ → V → Prop} {Y Ya Yt : υ → V → Prop} + [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Z t v)] [∀ t v, Decidable (Zt t v)] + [∀ t v, Decidable (Y t v)] [∀ t v, Decidable (Ya t v)] [∀ t v, Decidable (Yt t v)] + {x y : V} (hSx : ({s | X s x} : Finset ι).Nonempty) + (hZπ : ∀ z, (dens {t | Zt t z} : ℝ) = πf) (hπf : 0 < πf) + (hYt : ∀ t, Yt t y → Ya t y) (hSy : ({t | Yt t y} : Finset υ).Nonempty) + (hQh : ∀ v, Q v ≠ 0 → hF v = 1) (hρF0 : ∀ r, 0 ≤ ρF r) (hρF1 : ∀ r, ρF r ≤ 1) + {ηF : ℝ} (hηF : 0 < ηF) (hρFη : ∀ r, r ≤ ηF → ρF r = 1) + (hτ0 : ∀ r, 0 ≤ τ r) (hτ1 : ∀ r, τ r ≤ 1) {τ₀ : ℝ} (hτ₀ : 0 ≤ τ₀) + (hττ : ∀ r, r ≤ τ₀ → τ r = 1) {e : ℝ} (hI : ∀ v r, v ≤ e → I v r = 0) + (hf : 0 < f) (hG0 : ∀ w, 0 ≤ G x w) {MF : ℝ} (hGM : ∑ w, G x w ≤ MF) + {cF : ℝ} (hcF : 0 ≤ cF) (hKF : 4 * (1 + cF * MF / ηF) ≤ KF) + (hpairZ : ∀ z w, w ≠ z → (#{t | Zt t z ∧ Z t w} : ℝ) ≤ cF * f * #{t | Zt t z}) + {p : ℝ} (hp : 0 ≤ p) + (hpairX : ∀ w, w ≠ x → (#{s | X s x ∧ X s w} : ℝ) ≤ p * #{s | X s x}) + {R : ℝ} (hR : ∀ z, g₀ z ≠ 0 → p * #({w | e < G w z / f} : Finset V) ≤ R) + (hKc : 4 * (1 + R) ≤ Kc) + (hkh : ∀ v, k v ≠ 0 → hB v = 1) (hρB0 : ∀ r, 0 ≤ ρB r) (hρB1 : ∀ r, ρB r ≤ 1) + {ηB : ℝ} (hηB : 0 < ηB) (hρBη : ∀ r, r ≤ ηB → ρB r = 1) (hb : 0 < b) + (hH0 : ∀ z w, 0 ≤ H z w) {MB : ℝ} (hHM : ∀ z, ∑ w, H z w ≤ MB) + {cB : ℝ} (hcB : 0 ≤ cB) (hKB : 2 * (1 + cB * MB / ηB) ≤ KB) + (hpairY : ∀ w, w ≠ y → (#{t | Yt t y ∧ Y t w} : ℝ) ≤ cB * b * #{t | Yt t y}) : + 𝔼 d ∈ (({s | X s x} : Finset ι) ×ˢ (univ : Finset κ)) ×ˢ ({t | Ya t y} : Finset υ), + b * ((dens {t | Ya t y} : ℝ) / dens {t | Yt t y}) * (f / πf) * + ∑ z, correctionAtom I τ KF Kc f G X Z Zt Q hF ρF g₀ d.1 x z * + denseAtom Y Yt k hB ρB KB b H d.2 z y = + ∑ z, (f * Q (G x z / f) * g₀ z) * (b * k (H z y / b)) := by + have hSz : ∀ z, ({t | Zt t z} : Finset κ).Nonempty := by + intro z + have hpos : (0 : ℝ) < dens {t | Zt t z} := by rw [hZπ]; exact hπf + refine dens_ne_zero.mp ?_ + intro hz + rw [hz] at hpos + norm_num at hpos + have hleft : ∀ z, (𝔼 d ∈ ({s | X s x} : Finset ι) ×ˢ (univ : Finset κ), + correctionAtom I τ KF Kc f G X Z Zt Q hF ρF g₀ d x z) = + πf * (Q (G x z / f) * g₀ z) := by + intro z + rw [expect_correctionAtom_unconditioned hSx (hSz z) hQh hρF0 hρF1 hηF hρFη hτ0 hτ1 + hτ₀ hττ hI hf hG0 hGM hcF hKF (hpairZ z) hp hpairX (hR z) hKc, hZπ] + have hright : ∀ z, (𝔼 t ∈ ({t | Ya t y} : Finset υ), + b * ((dens {t | Ya t y} : ℝ) / dens {t | Yt t y}) * + denseAtom Y Yt k hB ρB KB b H t z y) = b * k (H z y / b) := by + intro z + exact expect_denseAtom_change_usage hYt hSy hkh hρB0 hρB1 hηB hρBη hb (hH0 z) + (hHM z) hcB hKB hpairY + simp_rw [mul_sum] + rw [expect_sum_comm] + refine sum_congr rfl fun z _ => ?_ + rw [expect_product] + calc + _ = 𝔼 l ∈ ({s | X s x} : Finset ι) ×ˢ (univ : Finset κ), + 𝔼 t ∈ ({t | Ya t y} : Finset υ), + ((f / πf) * correctionAtom I τ KF Kc f G X Z Zt Q hF ρF g₀ l x z) * + (b * ((dens {t | Ya t y} : ℝ) / dens {t | Yt t y}) * + denseAtom Y Yt k hB ρB KB b H t z y) := by + refine expect_congr rfl fun l _ => expect_congr rfl fun t _ => ?_ + ring + _ = _ := by + rw [← expect_mul_expect, ← mul_expect, hleft z, hright z] + field_simp + +end Matrix diff --git a/ComplexityTests/TrueSampleMeans.lean b/ComplexityTests/TrueSampleMeans.lean new file mode 100644 index 000000000..d1b237e82 --- /dev/null +++ b/ComplexityTests/TrueSampleMeans.lean @@ -0,0 +1,158 @@ +/- +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.TrueSampleMeans +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Tests for the true sampled means + +The source and intermediate channels each retain on one of two seeds. The broad terminal slice +has two of four seeds; its usage slice has only one. Both correction factors are therefore two. +The correction edge `0 → 1` has weight `1/2`, and the dense edge `1 → 0` has weight `1/3`. +The product sample is `2/3` on one of its four conditioning draws and zero on the others, giving +the prescribed positive product `1/6`. +-/ + +namespace ComplexityTests.TrueSampleMeans + +open Finset Matrix +open scoped BigOperators + +private abbrev X (s : Bool) (_ : Fin 2) : Prop := s = true +private abbrev Z (t : Bool) (_ : Fin 2) : Prop := t = true +private abbrev Y (_ : Fin 4) (_ : Fin 2) : Prop := True +private abbrev Ya (t : Fin 4) (_ : Fin 2) : Prop := t.val < 2 +private abbrev Yt (t : Fin 4) (_ : Fin 2) : Prop := t = 0 + +private noncomputable def left (x z : Fin 2) : ℝ := if x = 0 ∧ z = 1 then 1 / 2 else 0 +private noncomputable def right (z y : Fin 2) : ℝ := if z = 1 ∧ y = 0 then 1 / 3 else 0 + +private theorem source_slice (x : Fin 2) : ({s | X s x} : Finset Bool) = {true} := by + change ({s | s = true} : Finset Bool) = {true} + decide + +private theorem middle_slice (z : Fin 2) : ({t | Z t z} : Finset Bool) = {true} := by + change ({t | t = true} : Finset Bool) = {true} + decide + +private theorem broad_slice (y : Fin 2) : ({t | Ya t y} : Finset (Fin 4)) = {0, 1} := by + change ({t : Fin 4 | t.val < 2} : Finset (Fin 4)) = {0, 1} + decide + +private theorem usage_slice (y : Fin 2) : ({t | Yt t y} : Finset (Fin 4)) = {0} := by + change ({t | t = 0} : Finset (Fin 4)) = {0} + decide + +private theorem middle_density (z : Fin 2) : (dens {t | Z t z} : ℝ) = 1 / 2 := by + rw [middle_slice, dens_eq_card_div_card] + norm_num + +private theorem broad_density (y : Fin 2) : (dens {t | Ya t y} : ℝ) = 1 / 2 := by + rw [broad_slice, dens_eq_card_div_card] + norm_num + +private theorem usage_density (y : Fin 2) : (dens {t | Yt t y} : ℝ) = 1 / 4 := by + rw [usage_slice, dens_eq_card_div_card] + norm_num + +private theorem usage_subset (y : Fin 2) (t : Fin 4) (ht : Yt t y) : Ya t y := by + rcases ht with rfl + norm_num [Ya] + +private theorem column_support (z : Fin 2) : #{w : Fin 2 | 0 < left w z} ≤ 1 := by + refine card_le_one.2 fun u hu v hv => ?_ + have hu0 : u = 0 := by + by_contra h + simp [left, h] at hu + have hv0 : v = 0 := by + by_contra h + simp [left, h] at hv + exact hu0.trans hv0.symm + +private noncomputable def correction (d : Bool × Bool) (x z : Fin 2) : ℝ := + correctionAtom (fun _ _ => 0) (fun _ => 1) 8 8 1 left X Z Z id (fun _ => 1) + (fun _ => 1) (fun _ => 1) d x z + +private noncomputable def dense (t : Fin 4) (z y : Fin 2) : ℝ := + denseAtom Y Yt id (fun _ => 1) (fun _ => 1) 4 1 right t z y + +private theorem correction_eq (d : Bool × Bool) (x z : Fin 2) : + correction d x z = if d.2 = true then left x z else 0 := by + have hn : correctionNormalizer (fun _ _ => 0) (fun _ => 1) 8 8 1 left X Z Z + (fun _ => 1) (fun _ => 1) x z = 1 := by + simp [correctionNormalizer, correctionPrep, rowGate, incomingGate, X, Z, filter_eq'] + norm_num [correction, correctionAtom, rowGate, incomingGate, Z, hn] + +private theorem dense_eq (t : Fin 4) (z y : Fin 2) : + dense t z y = if t = 0 then right z y else 0 := by + norm_num [dense, denseAtom, atomNormalizer, atomPrep, rowGate, Yt, filter_eq'] + +private noncomputable def sample (d : (Bool × Bool) × Fin 4) : ℝ := + 4 * ∑ z, correction d.1 0 z * dense d.2 z 0 + +-- Both scalar corrections are nontrivial, and the integrand is genuinely nonzero. +example : (dens {t | Ya t 0} : ℝ) / dens {t | Yt t 0} = 2 ∧ + (1 : ℝ) / dens {t | Z t 0} = 2 := by + rw [broad_density, usage_density, middle_density] + norm_num + +example : sample ((true, true), 0) = 2 / 3 := by + norm_num [sample, correction_eq, dense_eq, left, right, Fin.sum_univ_two] + +example : sample ((true, false), 0) = 0 ∧ sample ((true, true), 1) = 0 := by + norm_num [sample, correction_eq, dense_eq, left, right, Fin.sum_univ_two] + +-- The direct term changes from the two-draw broad slice to the singleton usage slice. +private theorem direct_mean : + 𝔼 t ∈ ({t | Ya t 0} : Finset (Fin 4)), 2 * dense t 1 0 = 1 / 3 := by + have h := expect_denseAtom_change_usage (Y := Y) (Ya := Ya) (Yt := Yt) (k := id) + (h := fun _ => 1) (ρ := fun _ => 1) (K := 4) (b := 1) (G := right) (x := 1) (y := 0) + (usage_subset 0) ⟨0, by decide⟩ (fun _ _ => rfl) (fun _ => zero_le_one) (fun _ => le_rfl) + (η := 1) one_pos (fun _ _ => rfl) one_pos + (fun w => by fin_cases w <;> norm_num [right]) (M := 1) (by norm_num [right, Fin.sum_univ_two]) + (c := 1) zero_le_one (by norm_num) (fun w _ => by simp [Y, Yt]) + rw [broad_density, usage_density] at h + norm_num [dense, right] at h ⊢ + exact h + +-- Adding the independent source conditioning leaves the direct mean unchanged. +example : 𝔼 d ∈ ({s | X s 1} : Finset Bool) ×ˢ ({t | Ya t 0} : Finset (Fin 4)), + 2 * dense d.2 1 0 = 1 / 3 := by + rw [expect_product] + simp only [direct_mean, source_slice, expect_singleton] + +-- The product theorem is applied with every gate, pair-count and density hypothesis discharged. +-- In particular the coefficient `f / πf = 2` is justified by the actual middle-channel density. +example : 𝔼 d ∈ (({s | X s 0} : Finset Bool) ×ˢ (univ : Finset Bool)) ×ˢ + ({t | Ya t 0} : Finset (Fin 4)), sample d = 1 / 6 := by + have h := expect_correctionAtom_mul_denseAtom + (I := fun _ _ => 0) (τ := fun _ => 1) (Q := id) (hF := fun _ => 1) (ρF := fun _ => 1) + (k := id) (hB := fun _ => 1) (ρB := fun _ => 1) (KF := 8) (Kc := 8) (KB := 4) + (f := 1) (b := 1) (πf := 1 / 2) (G := left) (H := right) (g₀ := fun _ => 1) + (X := X) (Z := Z) (Zt := Z) (Y := Y) (Ya := Ya) (Yt := Yt) (x := 0) (y := 0) + (hSx := ⟨true, by decide⟩) (hZπ := middle_density) (hπf := by norm_num) + (hYt := usage_subset 0) (hSy := ⟨0, by decide⟩) + (hQh := fun _ _ => rfl) (hρF0 := fun _ => zero_le_one) (hρF1 := fun _ => le_rfl) + (ηF := 1) (hηF := one_pos) (hρFη := fun _ _ => rfl) + (hτ0 := fun _ => zero_le_one) (hτ1 := fun _ => le_rfl) (τ₀ := 0) (hτ₀ := le_rfl) + (hττ := fun _ _ => rfl) (e := 0) (hI := fun _ _ _ => rfl) + (hf := one_pos) (hG0 := fun w => by fin_cases w <;> norm_num [left]) + (MF := 1) (hGM := by norm_num [left, Fin.sum_univ_two]) (cF := 1) (hcF := zero_le_one) + (hKF := by norm_num) (hpairZ := fun z w _ => by simp [Z]) + (p := 1) (hp := zero_le_one) (hpairX := fun w _ => by simp [X]) + (R := 1) (hR := fun z _ => by simpa using column_support z) + (hKc := by norm_num) (hkh := fun _ _ => rfl) (hρB0 := fun _ => zero_le_one) + (hρB1 := fun _ => le_rfl) (ηB := 1) (hηB := one_pos) (hρBη := fun _ _ => rfl) + (hb := one_pos) (hH0 := fun z w => by fin_cases z <;> fin_cases w <;> norm_num [right]) + (MB := 1) (hHM := fun z => by fin_cases z <;> norm_num [right, Fin.sum_univ_two]) + (cB := 1) (hcB := zero_le_one) (hKB := by norm_num) (hpairY := fun w _ => by simp [Y, Yt]) + rw [broad_density, usage_density] at h + norm_num [sample, correction, dense, left, right, Fin.sum_univ_two] at h ⊢ + exact h + +end ComplexityTests.TrueSampleMeans From cfa2bc719f8c3d1b70ae32a7b9c7143941674527 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:18:03 +0000 Subject: [PATCH 4/4] feat(logspace): bound coupled correction-dense product errors Independent non-author source/API review by compression_review approved exact source revision fcbb5797a9c8b5c9bde9fd80de74ed84ec2c1e90 against the pinned Lemma 7.3, with no findings. Reviewed source files are unchanged. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --- Complexity.lean | 1 + .../Foundations/Probability/ProductError.lean | 327 ++++++++++++++++++ .../Foundations/Probability/RootMetric.lean | 2 +- ComplexityTests/ProductError.lean | 175 ++++++++++ 4 files changed, 504 insertions(+), 1 deletion(-) create mode 100644 Complexity/Foundations/Probability/ProductError.lean create mode 100644 ComplexityTests/ProductError.lean diff --git a/Complexity.lean b/Complexity.lean index 23713eb44..9c4cce3bf 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2731,6 +2731,7 @@ public import Complexity.Foundations.Probability.Gaussian.Multivariate public import Complexity.Foundations.Probability.Gaussian.Real public import Complexity.Foundations.Probability.Gaussian.Sheppard public import Complexity.Foundations.Probability.HierarchyParams +public import Complexity.Foundations.Probability.ProductError public import Complexity.Foundations.Probability.RootMetric public import Complexity.Foundations.Probability.SecondMoment public import Complexity.Foundations.Probability.SourceRelease diff --git a/Complexity/Foundations/Probability/ProductError.lean b/Complexity/Foundations/Probability/ProductError.lean new file mode 100644 index 000000000..d9c849a31 --- /dev/null +++ b/Complexity/Foundations/Probability/ProductError.lean @@ -0,0 +1,327 @@ +/- +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.SourceRelease +import Complexity.Foundations.Analysis.RootError +import Mathlib.Algebra.Order.BigOperators.Expect +import Mathlib.Algebra.Order.Ring.Basic +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Coupled product errors and source release + +For four nonnegative tables on one environment, compare the concrete products +`P σ x y = ∑ z ∈ Z σ, F σ x z * B σ z y` and `P'` built from `F'`, `B'`. +Splitting each product through `F' * B` charges the left error against the row support of `B` +and the right error against the incoming support of `F'`. The latter changes source rate from +`u` to `f` and has the exact normalization cost `f / u`. + +The root-metric estimate uses the homogeneous-loss mixture inequality and scalar product-root +comparison. Its explicit conservative constant is `2 ^ (2 * (s - 1)) * s ^ s`, or `16384` at +`s = 4`. All four tables may depend on the same environment. The right error is a common table +at `(z, y)`, with no additional old-source argument. + +This is the product and source-domain part of the proof of [OpenAI2026LogSpace, Lemma 7.3]. +The coarse/fine terminal scale comparisons and conditional-mean estimates remain separate. +No final-estimator or machine-space contract is assumed. + +## Main results + +* `Cslib.rootDistPow_mul_le`: a coupled product-table estimate with row and incoming caps. +* `Matrix.correctionAtom_denseAtom_rootDistPow_le`: the actual atom specialization, deriving + both support caps from the incoming and row gates. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + proof of Lemma 7.3, September 23, 2026 revision `7ef5c0cc` (preprint, not peer reviewed). +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Cslib + +private theorem root_mul_sub_pow_le {s : ℕ} (hs : s ≠ 0) {a a' b b' : ℝ} + (ha : 0 ≤ a) (ha' : 0 ≤ a') (hb : 0 ≤ b) (hb' : 0 ≤ b') : + |(a * b) ^ (s⁻¹ : ℝ) - (a' * b') ^ (s⁻¹ : ℝ)| ^ s ≤ + 2 ^ (s - 1) * (b * |a ^ (s⁻¹ : ℝ) - a' ^ (s⁻¹ : ℝ)| ^ s + + a' * |b ^ (s⁻¹ : ℝ) - b' ^ (s⁻¹ : ℝ)| ^ s) := by + have heq : (a * b) ^ (s⁻¹ : ℝ) - (a' * b') ^ (s⁻¹ : ℝ) = + (a ^ (s⁻¹ : ℝ) - a' ^ (s⁻¹ : ℝ)) * b ^ (s⁻¹ : ℝ) + + a' ^ (s⁻¹ : ℝ) * (b ^ (s⁻¹ : ℝ) - b' ^ (s⁻¹ : ℝ)) := by + rw [Real.mul_rpow ha hb, Real.mul_rpow ha' hb'] + ring + have habs : |(a * b) ^ (s⁻¹ : ℝ) - (a' * b') ^ (s⁻¹ : ℝ)| ≤ + |a ^ (s⁻¹ : ℝ) - a' ^ (s⁻¹ : ℝ)| * b ^ (s⁻¹ : ℝ) + + a' ^ (s⁻¹ : ℝ) * |b ^ (s⁻¹ : ℝ) - b' ^ (s⁻¹ : ℝ)| := by + rw [heq] + refine (abs_add_le _ _).trans_eq ?_ + rw [abs_mul, abs_mul, abs_of_nonneg (Real.rpow_nonneg hb _), + abs_of_nonneg (Real.rpow_nonneg ha' _)] + refine (pow_le_pow_left₀ (abs_nonneg _) habs s).trans ?_ + refine (add_pow_le (by positivity) (by positivity) s).trans_eq ?_ + rw [mul_pow, mul_pow, Real.rpow_inv_natCast_pow hb hs, Real.rpow_inv_natCast_pow ha' hs] + ring + +private theorem root_sum_mul_sub_pow_le {α : Type*} (T : Finset α) {s : ℕ} (hs : s ≠ 0) + {a a' b b' : α → ℝ} (ha : ∀ z ∈ T, 0 ≤ a z) (ha' : ∀ z ∈ T, 0 ≤ a' z) + (hb : ∀ z ∈ T, 0 ≤ b z) (hb' : ∀ z ∈ T, 0 ≤ b' z) : + |(∑ z ∈ T, a z * b z) ^ (s⁻¹ : ℝ) - (∑ z ∈ T, a' z * b' z) ^ (s⁻¹ : ℝ)| ^ s ≤ + (2 ^ (2 * (s - 1)) * (s : ℝ) ^ s) * + ∑ z ∈ T, (b z * |a z ^ (s⁻¹ : ℝ) - a' z ^ (s⁻¹ : ℝ)| ^ s + + a' z * |b z ^ (s⁻¹ : ℝ) - b' z ^ (s⁻¹ : ℝ)| ^ s) := by + have hsum := homogeneousLoss_sum_le T hs (w := fun _ => 1) + (F := fun z => a z * b z) (F' := fun z => a' z * b' z) (fun _ _ => zero_le_one) + (fun z hz => mul_nonneg (ha z hz) (hb z hz)) + (fun z hz => mul_nonneg (ha' z hz) (hb' z hz)) + simp only [one_mul] at hsum + calc + _ ≤ 2 ^ (s - 1) * homogeneousLoss s (∑ z ∈ T, a z * b z) (∑ z ∈ T, a' z * b' z) := + rpow_inv_sub_pow_le_homogeneousLoss hs + (sum_nonneg fun z hz => mul_nonneg (ha z hz) (hb z hz)) + (sum_nonneg fun z hz => mul_nonneg (ha' z hz) (hb' z hz)) + _ ≤ 2 ^ (s - 1) * ∑ z ∈ T, homogeneousLoss s (a z * b z) (a' z * b' z) := + mul_le_mul_of_nonneg_left hsum (by positivity) + _ ≤ 2 ^ (s - 1) * ∑ z ∈ T, (s : ℝ) ^ s * + (2 ^ (s - 1) * (b z * |a z ^ (s⁻¹ : ℝ) - a' z ^ (s⁻¹ : ℝ)| ^ s + + a' z * |b z ^ (s⁻¹ : ℝ) - b' z ^ (s⁻¹ : ℝ)| ^ s)) := by + refine mul_le_mul_of_nonneg_left (sum_le_sum fun z hz => ?_) (by positivity) + exact (homogeneousLoss_le_rpow_inv_sub_pow hs (mul_nonneg (ha z hz) (hb z hz)) + (mul_nonneg (ha' z hz) (hb' z hz))).trans + (mul_le_mul_of_nonneg_left (root_mul_sub_pow_le hs (ha z hz) (ha' z hz) + (hb z hz) (hb' z hz)) (by positivity)) + _ = _ := by + simp only [← mul_sum] + rw [show 2 * (s - 1) = (s - 1) + (s - 1) by omega, pow_add] + ring + +private theorem sum_le_mul_of_card_support_le {α : Type*} (T : Finset α) {v : α → ℝ} + {C : ℝ} (hC : 0 ≤ C) (hv : ∀ z, v z ≤ C) {K : ℕ} (hK : #{z ∈ T | v z ≠ 0} ≤ K) : + ∑ z ∈ T, v z ≤ K * C := by + classical + have hsum : ∑ z ∈ T, v z = ∑ z ∈ T with v z ≠ 0, v z := by + rw [sum_filter] + refine sum_congr rfl fun z _ => ?_ + split_ifs with hz + · rfl + · exact not_ne_iff.mp hz + rw [hsum] + calc + _ ≤ ∑ z ∈ T with v z ≠ 0, C := sum_le_sum fun z _ => hv z + _ = (#{z ∈ T | v z ≠ 0} : ℝ) * C := by rw [sum_const, nsmul_eq_mul] + _ ≤ K * C := mul_le_mul_of_nonneg_right (by exact_mod_cast hK) hC + +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)] + +/-- **Coupled product errors with source release**. The true or estimated tables may share +all their randomness. Only `B` needs the row cap and bound `CB`, and only `F'` needs the incoming +cap and bound `CF`, because the scalar comparison splits through `F' * B`. +The source normalization in the right error is exactly `f / u`. -/ +theorem rootDistPow_mul_le (hs : s ≠ 0) (hN : 0 < N) (hu : 0 < u) (hf : 0 < f) + {F F' B B' : Ω → V → V → ℝ} + (hF : ∀ σ x z, 0 ≤ F σ x z) (hF' : ∀ σ x z, 0 ≤ F' σ x z) + (hB : ∀ σ z y, 0 ≤ B σ z y) (hB' : ∀ σ z y, 0 ≤ B' σ z y) + {CF CB : ℝ} (hCF : 0 ≤ CF) (hCB : 0 ≤ CB) + (hFbound : ∀ σ x z, F' σ x z ≤ CF) (hBbound : ∀ σ z y, B σ z y ≤ CB) + {Kr Kc : ℕ} (hrow : ∀ σ z, Z σ z → #{y ∈ ({y | Y σ y} : Finset V) | B σ z y ≠ 0} ≤ Kr) + (hcol : ∀ σ z, Z σ z → #{x ∈ ({x | X σ x} : Finset V) | F' σ x z ≠ 0} ≤ Kc) : + rootDistPow s N u X Y (fun σ x y => ∑ z ∈ ({z | Z σ z} : Finset V), F σ x z * B σ z y) + (fun σ x y => ∑ z ∈ ({z | Z σ z} : Finset V), F' σ x z * B' σ z y) ≤ + (2 ^ (2 * (s - 1)) * (s : ℝ) ^ s) * + (CB * Kr * rootDistPow s N u X Z F F' + + CF * Kc * (f / u) * rootDistPow s N f Z Y B B') := by + classical + let eF : Ω → V → V → ℝ := fun σ x z => |F σ x z ^ (s⁻¹ : ℝ) - F' σ x z ^ (s⁻¹ : ℝ)| ^ s + let eB : Ω → V → V → ℝ := fun σ z y => |B σ z y ^ (s⁻¹ : ℝ) - B' σ z y ^ (s⁻¹ : ℝ)| ^ s + have heF : ∀ σ x z, 0 ≤ eF σ x z := fun _ _ _ => by dsimp [eF]; positivity + have heB : ∀ σ z y, 0 ≤ eB σ z y := fun _ _ _ => by dsimp [eB]; positivity + have hleft : (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + ∑ z ∈ ({z | Z σ z} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), B σ z y * eF σ x z ≤ + CB * Kr * rootDistPow s N u X Z F F' := by + calc + _ ≤ (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + ∑ z ∈ ({z | Z σ z} : Finset V), ((Kr : ℝ) * CB) * eF σ x z := by + refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (by positivity) + refine sum_le_sum fun x _ => sum_le_sum fun z hz => ?_ + rw [← sum_mul] + exact mul_le_mul_of_nonneg_right + (sum_le_mul_of_card_support_le _ hCB (hBbound σ z) (hrow σ z (by simpa using hz))) + (heF σ x z) + _ = _ := by + simp only [rootDistPow, rowNormPow, eF, ← mul_sum, ← mul_expect] + ring + have hright : (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + ∑ z ∈ ({z | Z σ z} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), F' σ x z * eB σ z y ≤ + CF * Kc * (f / u) * rootDistPow s N f Z Y B B' := by + have hpoint : ∀ σ x, + ∑ z ∈ ({z | Z σ z} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), F' σ x z * eB σ z y ≤ + CF * ∑ z ∈ ({z | Z σ z} : Finset V) with F' σ x z ≠ 0, + ∑ y ∈ ({y | Y σ y} : Finset V), eB σ z y := by + intro σ x + conv_rhs => rw [mul_sum, sum_filter] + refine sum_le_sum fun z _ => ?_ + by_cases hz : F' σ x z = 0 + · simp [hz] + · simp only [hz, ne_eq, not_false_eq_true, ↓reduceIte] + rw [← mul_sum] + exact mul_le_mul_of_nonneg_right (hFbound σ x z) (sum_nonneg fun y _ => heB σ z y) + have hrelease : (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + ∑ z ∈ ({z | Z σ z} : Finset V) with F' σ x z ≠ 0, + ∑ y ∈ ({y | Y σ y} : Finset V), eB σ z y ≤ + Kc * (f / u) * rootDistPow s N f Z Y B B' := by + exact sourceRelease_le_rowNormPow hN hu hf (fun σ x z => F' σ x z ≠ 0) hcol + (fun σ z y => B σ z y ^ (s⁻¹ : ℝ) - B' σ z y ^ (s⁻¹ : ℝ)) + calc + _ ≤ (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + CF * ∑ z ∈ ({z | Z σ z} : Finset V) with F' σ x z ≠ 0, + ∑ y ∈ ({y | Y σ y} : Finset V), eB σ z y := by + exact mul_le_mul_of_nonneg_left + (expect_le_expect fun σ _ => sum_le_sum fun x _ => hpoint σ x) (by positivity) + _ = CF * ((N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), + ∑ z ∈ ({z | Z σ z} : Finset V) with F' σ x z ≠ 0, + ∑ y ∈ ({y | Y σ y} : Finset V), eB σ z y) := by + simp only [← mul_sum, ← mul_expect] + ring + _ ≤ CF * (Kc * (f / u) * rootDistPow s N f Z Y B B') := + mul_le_mul_of_nonneg_left hrelease hCF + _ = _ := by ring + have hswap : ∀ σ x, + ∑ y ∈ ({y | Y σ y} : Finset V), ∑ z ∈ ({z | Z σ z} : Finset V), + (B σ z y * eF σ x z + F' σ x z * eB σ z y) = + (∑ z ∈ ({z | Z σ z} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), B σ z y * eF σ x z) + + ∑ z ∈ ({z | Z σ z} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), F' σ x z * eB σ z y := by + intro σ x + rw [sum_comm] + simp only [sum_add_distrib] + rw [rootDistPow, rowNormPow] + calc + _ ≤ (N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), + (2 ^ (2 * (s - 1)) * (s : ℝ) ^ s) * + ∑ z ∈ ({z | Z σ z} : Finset V), (B σ z y * eF σ x z + F' σ x z * eB σ z y) := by + refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (by positivity) + refine sum_le_sum fun x _ => sum_le_sum fun y _ => ?_ + exact root_sum_mul_sub_pow_le _ hs (fun z _ => hF σ x z) (fun z _ => hF' σ x z) + (fun z _ => hB σ z y) (fun z _ => hB' σ z y) + _ = (2 ^ (2 * (s - 1)) * (s : ℝ) ^ s) * + (((N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ z ∈ ({z | Z σ z} : Finset V), + ∑ y ∈ ({y | Y σ y} : Finset V), B σ z y * eF σ x z) + + ((N * u)⁻¹ * 𝔼 σ, ∑ x ∈ ({x | X σ x} : Finset V), ∑ z ∈ ({z | Z σ z} : Finset V), + ∑ y ∈ ({y | Y σ y} : Finset V), F' σ x z * eB σ z y)) := by + simp only [← mul_sum, ← mul_expect] + simp_rw [hswap] + simp only [sum_add_distrib, expect_add_distrib, ← mul_sum] + ring + _ ≤ _ := mul_le_mul_of_nonneg_left (add_le_add hleft hright) (by positivity) + +end Cslib + +namespace Matrix + +variable {Ω V ι κ υ : Type*} [Fintype Ω] [Fintype V] [Fintype ι] [Fintype κ] [Fintype υ] + {s KF Kc KB : ℕ} {N u f b : ℝ} {I : ℝ → ℝ → ℝ} {τ Q hF ρF k hB ρB : ℝ → ℝ} + {X : ι → V → Prop} {Z Zt : κ → V → Prop} {Y Yt : υ → V → Prop} + [∀ t x, Decidable (X t x)] [∀ t z, Decidable (Z t z)] [∀ t z, Decidable (Zt t z)] + [∀ t y, Decidable (Y t y)] [∀ t y, Decidable (Yt t y)] + +private theorem nonneg_correctionAtom {G : Matrix V V ℝ} {g₀ : V → ℝ} + (hQ0 : ∀ v, 0 ≤ Q v) (hρ0 : ∀ r, 0 ≤ ρF r) (hτ0 : ∀ r, 0 ≤ τ r) + (hg₀ : ∀ z, 0 ≤ g₀ z) (d : ι × κ) (x z : V) : + 0 ≤ correctionAtom I τ KF Kc f G X Z Zt Q hF ρF g₀ d x z := by + rw [correctionAtom] + split_ifs + · refine mul_nonneg (div_nonneg (mul_nonneg (hQ0 _) (mul_nonneg (hρ0 _) (hτ0 _))) ?_) + (hg₀ z) + exact le_trans (by norm_num : (0 : ℝ) ≤ 1 / 2) (le_max_left _ _) + · exact le_rfl + +private theorem nonneg_denseAtom {H : Matrix V V ℝ} + (hk0 : ∀ v, 0 ≤ k v) (hρ0 : ∀ r, 0 ≤ ρB r) (t : υ) (z y : V) : + 0 ≤ denseAtom Y Yt k hB ρB KB b H t z y := by + rw [denseAtom] + split_ifs + · refine div_nonneg (mul_nonneg (hk0 _) (hρ0 _)) ?_ + exact le_trans (by norm_num : (0 : ℝ) ≤ 1 / 2) (le_max_left _ _) + · exact le_rfl + +/-- **Product errors for actual correction and dense atoms**. The matrices, multipliers, and +both seed maps may depend on one shared environment. The bounded cutoffs give `CF = 2 * AF` +and `CB = 2 * AB`; the actual incoming and row gates give caps `Kc` and `KB`. + +The intermediate source normalization changes from `u` to the correction scale `f`, with exact +factor `f / u`. This theorem does not change the terminal scale `b` or take conditional means. -/ +theorem correctionAtom_denseAtom_rootDistPow_le + (drawF : Ω → ι × κ) (drawB : Ω → υ) + (G G' H H' : Ω → Matrix V V ℝ) (g g' : Ω → V → ℝ) + (hs : s ≠ 0) (hN : 0 < N) (hu : 0 < u) (hf : 0 < f) + (hQ0 : ∀ v, 0 ≤ Q v) (hk0 : ∀ v, 0 ≤ k v) + (hρF0 : ∀ r, 0 ≤ ρF r) (hρF1 : ∀ r, ρF r ≤ 1) + (hτ0 : ∀ r, 0 ≤ τ r) (hτ1 : ∀ r, τ r ≤ 1) + (hρB0 : ∀ r, 0 ≤ ρB r) (hρB1 : ∀ r, ρB r ≤ 1) + (hg0 : ∀ σ z, 0 ≤ g σ z) (hg'0 : ∀ σ z, 0 ≤ g' σ z) (hg'1 : ∀ σ z, g' σ z ≤ 1) + {AF AB : ℝ} (hAF : 0 ≤ AF) (hAB : 0 ≤ AB) + (hQbound : ∀ σ x z, Q (G' σ x z / f) ≤ AF) + (hkbound : ∀ σ z y, k (H σ z y / b) ≤ AB) + (hKc : 0 < Kc) (hIQ : ∀ v r, Q v ≠ 0 → ρF r ≠ 0 → I v r = 1) + {gF : ℝ} (hgF : gF ≤ 1) (hτclose : ∀ r, gF ≤ r → τ r = 0) + (hYt : ∀ t y, Yt t y → Y t y) (hKB : 0 < KB) + {eB gB : ℝ} (heB : 0 ≤ eB) (hkzero : ∀ v, v ≤ eB → k v = 0) + (hgB : gB ≤ eB) (hρBclose : ∀ r, gB ≤ r → ρB r = 0) : + let F := fun σ => correctionAtom I τ KF Kc f (G σ) X Z Zt Q hF ρF (g σ) (drawF σ) + let F' := fun σ => correctionAtom I τ KF Kc f (G' σ) X Z Zt Q hF ρF (g' σ) (drawF σ) + let B := fun σ => denseAtom Y Yt k hB ρB KB b (H σ) (drawB σ) + let B' := fun σ => denseAtom Y Yt k hB ρB KB b (H' σ) (drawB σ) + Cslib.rootDistPow s N u (fun σ x => X (drawF σ).1 x) (fun σ y => Yt (drawB σ) y) + (fun σ x y => ∑ z ∈ ({z | Zt (drawF σ).2 z} : Finset V), F σ x z * B σ z y) + (fun σ x y => ∑ z ∈ ({z | Zt (drawF σ).2 z} : Finset V), F' σ x z * B' σ z y) ≤ + (2 ^ (2 * (s - 1)) * (s : ℝ) ^ s) * + ((2 * AB) * KB * Cslib.rootDistPow s N u (fun σ x => X (drawF σ).1 x) + (fun σ z => Zt (drawF σ).2 z) F F' + + (2 * AF) * Kc * (f / u) * Cslib.rootDistPow s N f (fun σ z => Zt (drawF σ).2 z) + (fun σ y => Yt (drawB σ) y) B B') := by + classical + dsimp only + refine Cslib.rootDistPow_mul_le hs hN hu hf + (fun σ => nonneg_correctionAtom hQ0 hρF0 hτ0 (hg0 σ) (drawF σ)) + (fun σ => nonneg_correctionAtom hQ0 hρF0 hτ0 (hg'0 σ) (drawF σ)) + (fun σ => nonneg_denseAtom hk0 hρB0 (drawB σ)) + (fun σ => nonneg_denseAtom hk0 hρB0 (drawB σ)) + (by positivity) (by positivity) ?_ ?_ ?_ ?_ + · intro σ x z + calc + _ ≤ |correctionAtom I τ KF Kc f (G' σ) X Z Zt Q hF ρF (g' σ) (drawF σ) x z| := + le_abs_self _ + _ ≤ 2 * |Q (G' σ x z / f)| * |g' σ z| := abs_correctionAtom_le hρF0 hρF1 hτ0 hτ1 _ _ _ + _ = 2 * Q (G' σ x z / f) * g' σ z := by + rw [abs_of_nonneg (hQ0 _), abs_of_nonneg (hg'0 _ _)] + _ ≤ (2 * AF) * 1 := mul_le_mul + (mul_le_mul_of_nonneg_left (hQbound σ x z) (by norm_num)) (hg'1 σ z) (hg'0 σ z) + (by positivity) + _ = _ := mul_one _ + · intro σ z y + calc + _ ≤ |denseAtom Y Yt k hB ρB KB b (H σ) (drawB σ) z y| := le_abs_self _ + _ ≤ 2 * |k (H σ z y / b)| := abs_denseAtom_le hρB0 hρB1 _ _ _ + _ = 2 * k (H σ z y / b) := by rw [abs_of_nonneg (hk0 _)] + _ ≤ _ := mul_le_mul_of_nonneg_left (hkbound σ z y) (by norm_num) + · intro σ z _ + refine (card_le_card ?_).trans + (card_filter_denseAtom_ne_zero_lt (h := hB) (a := b) (G := H σ) + hYt hKB heB hkzero hgB hρBclose (drawB σ) z).le + intro y hy + exact mem_filter.mpr ⟨mem_univ _, (mem_filter.mp hy).2⟩ + · intro σ z _ + exact (card_filter_correctionAtom_col_ne_zero_lt hKc hIQ hgF hτclose (drawF σ) z).le + +end Matrix diff --git a/Complexity/Foundations/Probability/RootMetric.lean b/Complexity/Foundations/Probability/RootMetric.lean index 651f7bbf2..5b98e8774 100644 --- a/Complexity/Foundations/Probability/RootMetric.lean +++ b/Complexity/Foundations/Probability/RootMetric.lean @@ -76,7 +76,7 @@ variable (s : ℕ) (N u : ℝ) (X Y : Ω → V → Prop) [∀ σ v, Decidable (X /-- The `s`-th power `d_{u,a}(H, H')^s` of the root distance of two random tables [OpenAI2026LogSpace, (5.19)]. -/ -noncomputable def rootDistPow (H H' : Ω → V → V → ℝ) : ℝ := +@[expose] noncomputable def rootDistPow (H H' : Ω → V → V → ℝ) : ℝ := rowNormPow s N u X Y fun σ x y => H σ x y ^ (s⁻¹ : ℝ) - H' σ x y ^ (s⁻¹ : ℝ) /-- The `s`-th power `‖v‖^s_{u;s}` of the integrated norm of a random vertex array diff --git a/ComplexityTests/ProductError.lean b/ComplexityTests/ProductError.lean new file mode 100644 index 000000000..e5d591fb7 --- /dev/null +++ b/ComplexityTests/ProductError.lean @@ -0,0 +1,175 @@ +/- +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.ProductError +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Tests for coupled product errors + +An actual correction edge `0 → 1` and dense edge `1 → 2` have weights `1` in the first +version and `16` in the second. Their usage channels use the same Boolean seed, so their +masks are perfectly correlated. The product-root error has positive fourth power `81 / 2`, +while the source normalizations `u = 1/3`, `f = 1` make the release factor three. +-/ + +namespace ComplexityTests.ProductError + +open Finset Matrix Cslib +open scoped BigOperators + +private abbrev full {α : Type*} (_ : α) (_ : Fin 3) : Prop := True +private abbrev mask (σ : Bool) (_ : Fin 3) : Prop := σ = true + +private noncomputable def left (w : ℝ) (x z : Fin 3) : ℝ := + if x = 0 ∧ z = 1 then w else 0 + +private noncomputable def right (w : ℝ) (z y : Fin 3) : ℝ := + if z = 1 ∧ y = 2 then w + 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 noncomputable def Q (v : ℝ) : ℝ := max v 0 +private noncomputable def k (v : ℝ) : ℝ := max (v - 1) 0 + +private theorem gate_nonneg (r : ℝ) : 0 ≤ gate r := by + unfold gate + split_ifs <;> norm_num + +private theorem gate_le_one (r : ℝ) : gate r ≤ 1 := by + unfold gate + split_ifs <;> norm_num + +private theorem gate_zero (r : ℝ) (hr : 1 ≤ r) : gate r = 0 := ite_eq_right (not_lt.mpr hr) + +private theorem score_one (v r : ℝ) (hv : Q v ≠ 0) (_ : (1 : ℝ) ≠ 0) : score v r = 1 := by + have hv0 : v ≠ 0 := fun h => hv (by simp [Q, h]) + exact ite_eq_right hv0 + +private theorem incoming_one (w : ℝ) (z : Fin 3) : + incomingGate score gate 3 2 1 (left w) univ univ z = 1 := by + have hcard : #{x : Fin 3 | 1 ≤ auxScore score 3 1 (left w) univ x z} ≤ 1 := by + refine card_le_one.2 fun x hx x' hx' => ?_ + have hx0 : x = 0 := by + by_contra h + norm_num [auxScore, score, left, h] at hx + have hx'0 : x' = 0 := by + by_contra h + norm_num [auxScore, score, left, h] at hx' + exact hx0.trans hx'0.symm + have hlt : kthLargest 2 univ (fun x => auxScore score 3 1 (left w) univ x z) < 1 := by + exact lt_of_not_ge fun h => by + have := (le_kthLargest_iff (by decide) zero_lt_one).mp h + omega + exact ite_eq_left hlt + +private theorem row_one (w : ℝ) (z : Fin 3) : rowGate gate 2 1 (right w) univ z = 1 := by + have hcard : #{y : Fin 3 | 1 ≤ right w z y / 1} ≤ 1 := by + refine card_le_one.2 fun y hy y' hy' => ?_ + have hy2 : y = 2 := by + by_contra h + norm_num [right, h] at hy + have hy'2 : y' = 2 := by + by_contra h + norm_num [right, h] at hy' + exact hy2.trans hy'2.symm + have hlt : kthLargest 2 univ (fun y => right w z y / 1) < 1 := by + exact lt_of_not_ge fun h => by + have := (le_kthLargest_iff (by decide) zero_lt_one).mp h + omega + exact ite_eq_left hlt + +private noncomputable def correction (w : ℝ) (σ : Bool) (x z : Fin 3) : ℝ := + correctionAtom score gate 3 2 1 (left w) full full mask Q (fun _ => 1) + (fun _ => 1) (fun _ => 1) ((), σ) x z + +private noncomputable def dense (w : ℝ) (σ : Bool) (z y : Fin 3) : ℝ := + denseAtom full mask k (fun _ => 1) gate 2 1 (right w) σ z y + +private theorem correction_eq (w : ℝ) (σ : Bool) (x z : Fin 3) : + correction w σ x z = if σ = true then Q (left w x z) else 0 := by + have hn : correctionNormalizer (ι := Unit) score gate 3 2 1 (left w) full full mask (fun _ => 1) + (fun _ => 1) x z = 1 := by + simp [correctionNormalizer, correctionPrep, rowGate, full, mask, incoming_one, filter_eq'] + norm_num [correction, correctionAtom, rowGate, full, mask, incoming_one, hn] + +private theorem dense_eq (w : ℝ) (σ : Bool) (z y : Fin 3) : + dense w σ z y = if σ = true then k (right w z y) else 0 := by + have hn : atomNormalizer full mask (fun _ => 1) gate 2 1 (right w) z y = 1 := by + simp [atomNormalizer, atomPrep, full, mask, row_one, filter_eq'] + norm_num [dense, denseAtom, full, mask, row_one, hn] + +private noncomputable def sample (w : ℝ) (σ : Bool) (x y : Fin 3) : ℝ := + ∑ z ∈ ({z | mask σ z} : Finset (Fin 3)), correction w σ x z * dense w σ z y + +private theorem sample_eq (w : ℝ) (σ : Bool) (x y : Fin 3) : + sample w σ x y = if σ = true ∧ x = 0 ∧ y = 2 then (max w 0) ^ 2 else 0 := by + fin_cases σ <;> fin_cases x <;> fin_cases y <;> + norm_num [sample, mask, correction_eq, dense_eq, Q, k, left, right, Fin.sum_univ_three, + pow_two] + +example : sample 1 true 0 2 = 1 ∧ sample 16 true 0 2 = 256 ∧ sample 16 false 0 2 = 0 := by + norm_num [sample_eq] + +private theorem root_sixteen : (16 : ℝ) ^ (4⁻¹ : ℝ) = 2 := by + rw [show (16 : ℝ) = 2 ^ 4 by norm_num] + exact Real.pow_rpow_inv_natCast (by norm_num) (by norm_num) + +private theorem root_two_fifty_six : (256 : ℝ) ^ (4⁻¹ : ℝ) = 4 := by + rw [show (256 : ℝ) = 4 ^ 4 by norm_num] + exact Real.pow_rpow_inv_natCast (by norm_num) (by norm_num) + +private theorem product_error : rootDistPow 4 3 (1 / 3) (fun (_ : Bool) => full ()) mask + (sample 1) (sample 16) = 81 / 2 := by + norm_num [rootDistPow, rowNormPow, full, mask, sample_eq, expect_eq_sum_div_card, + sum_filter, Fin.sum_univ_three, Fintype.sum_bool, root_two_fifty_six] + +private theorem left_error : rootDistPow 4 3 (1 / 3) (fun (_ : Bool) => full ()) mask + (correction 1) (correction 16) = 1 / 2 := by + norm_num [rootDistPow, rowNormPow, full, mask, correction_eq, Q, left, + expect_eq_sum_div_card, sum_filter, Fin.sum_univ_three, Fintype.sum_bool, root_sixteen] + +private theorem right_error : rootDistPow 4 3 1 mask mask (dense 1) (dense 16) = 1 / 6 := by + norm_num [rootDistPow, rowNormPow, mask, dense_eq, k, right, expect_eq_sum_div_card, + sum_filter, Fin.sum_univ_three, Fintype.sum_bool, root_sixteen] + +-- Both caps are discharged from the actual atom gates. The two seed maps are correlated. +private theorem actual_atom_bound : + rootDistPow 4 3 (1 / 3) (fun (_ : Bool) => full ()) mask (sample 1) (sample 16) ≤ + 16384 * (4 * rootDistPow 4 3 (1 / 3) (fun (_ : Bool) => full ()) mask + (correction 1) (correction 16) + + 192 * rootDistPow 4 3 1 mask mask (dense 1) (dense 16)) := by + have h := correctionAtom_denseAtom_rootDistPow_le + (X := fun (_ : Unit) => full ()) (Z := fun (_ : Bool) => full ()) (Zt := mask) + (Y := fun (_ : Bool) => full ()) (Yt := mask) + (I := score) (τ := gate) (Q := Q) (hF := fun _ => 1) (ρF := fun _ => 1) + (k := k) (hB := fun _ => 1) (ρB := gate) (KF := 3) (Kc := 2) (KB := 2) + (s := 4) (N := 3) (u := 1 / 3) (f := 1) (b := 1) + (fun σ : Bool => ((), σ)) id (fun _ => left 1) (fun _ => left 16) + (fun _ => right 1) (fun _ => right 16) (fun _ _ => 1) (fun _ _ => 1) + (by decide) (by norm_num) (by norm_num) (by norm_num) + (fun v => le_max_right v 0) (fun v => le_max_right (v - 1) 0) + (fun _ => zero_le_one) (fun _ => le_rfl) gate_nonneg gate_le_one gate_nonneg gate_le_one + (fun _ _ => zero_le_one) (fun _ _ => zero_le_one) (fun _ _ => le_rfl) + (AF := 16) (AB := 1) (by norm_num) (by norm_num) + (fun _ x z => by fin_cases x <;> fin_cases z <;> norm_num [Q, left]) + (fun _ z y => by fin_cases z <;> fin_cases y <;> norm_num [k, right]) + (by decide) score_one (gF := 1) le_rfl gate_zero (fun _ _ _ => True.intro) + (by decide) (eB := 1) (gB := 1) zero_le_one + (fun v hv => max_eq_right (sub_nonpos.mpr hv)) le_rfl gate_zero + norm_num only [Nat.reduceSub, Nat.reduceMul, pow_succ, pow_zero, one_mul, mul_one, + one_div_div, div_one, id_eq, Prod.fst, Prod.snd] at h + exact h + +-- The positive left side and unequal source normalizations are evaluated independently. +example : (81 / 2 : ℝ) ≤ 557056 := by + have h := actual_atom_bound + rw [product_error, left_error, right_error] at h + convert h using 1 + norm_num + +end ComplexityTests.ProductError