From dfa6f5b694d2f775d95140608e0db0a064cf0d26 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:36:11 +0000 Subject: [PATCH 1/2] 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/2] 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