From c9f089087bbdebaf705660cd93b5bac245e80b4d Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:52:52 +0000 Subject: [PATCH] feat(logspace): bound heavy-count rarity and masked mean errors Prove the conditional true-heavy-count estimate, deterministic endpoint-error and retained-row maximum bounds, and the actual affine-channel instance at two rates. This is the conditional-rarity component of OpenAI2026LogSpace Lemma 8.4 (revision 7ef5c0cc), contributing to #1721 and #1444. Validation: rebuilt the complete 23-module Complexity dependency closure from exact source with pinned Lean 4.36.0-rc2 and strict warnings, then checked the final concrete tests and existing RootMetric tests. Hygiene, tracked import aggregate, focused module-doc name checks and whitespace checks pass. Full project gates run in CI. AI-assisted implementation and tests: OpenAI Codex. Independent nonauthor agent /root/review_heavy_rarity approved source tree 8549f1f49b84a4eea95c59c53e59ad85f37224ea after checking the pinned source and final regression delta. A cache/source mismatch found in review was resolved by exposing exactly the two norm definitions consumed here and rebuilding all local prerequisites. No human approval or full estimator endpoint is claimed. --- Complexity.lean | 3 + .../Foundations/Probability/HeavyCount.lean | 143 +++++++++++ .../Probability/HeavyCountRarity.lean | 181 +++++++++++++ .../Foundations/Probability/RootMetric.lean | 4 +- .../PairwiseIndependentHash/HeavyCount.lean | 74 ++++++ ComplexityTests/HeavyCountRarity.lean | 237 ++++++++++++++++++ 6 files changed, 640 insertions(+), 2 deletions(-) create mode 100644 Complexity/Foundations/Probability/HeavyCount.lean create mode 100644 Complexity/Foundations/Probability/HeavyCountRarity.lean create mode 100644 Complexity/Probability/PairwiseIndependentHash/HeavyCount.lean create mode 100644 ComplexityTests/HeavyCountRarity.lean diff --git a/Complexity.lean b/Complexity.lean index 9735d61c9..d01a34f7e 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2732,6 +2732,8 @@ public import Complexity.Foundations.Probability.DetectedStage 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.HeavyCount +public import Complexity.Foundations.Probability.HeavyCountRarity public import Complexity.Foundations.Probability.HierarchyParams public import Complexity.Foundations.Probability.RootMetric public import Complexity.Foundations.Probability.SecondMoment @@ -3001,6 +3003,7 @@ public import Complexity.Probability.PairwiseIndependentHash public import Complexity.Probability.PairwiseIndependentHash.Affine public import Complexity.Probability.PairwiseIndependentHash.AtomChannels public import Complexity.Probability.PairwiseIndependentHash.DetectorChannels +public import Complexity.Probability.PairwiseIndependentHash.HeavyCount public import Complexity.Probability.PairwiseIndependentHash.HierarchyChannels public import Complexity.Probability.PairwiseIndependentHash.Retention public import Complexity.Probability.PairwiseIndependentHash.RetentionChannel diff --git a/Complexity/Foundations/Probability/HeavyCount.lean b/Complexity/Foundations/Probability/HeavyCount.lean new file mode 100644 index 000000000..7d5481303 --- /dev/null +++ b/Complexity/Foundations/Probability/HeavyCount.lean @@ -0,0 +1,143 @@ +/- +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 Complexity.Foundations.Data.Finset.Markov +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Conditional rarity of retained heavy entries + +A row with first signal `d` has bounded mass `a * ∑ w, d w ≤ M`. At a floor `ρ > 0`, +there are at most `4 * M / (a * ρ)` entries above `ρ / 4`. Suppose that, on a finite slice +of draws, every endpoint other than one specified endpoint is retained on at most a +`c * a` fraction of the draws. The specified endpoint can contribute one retained entry. +Markov's inequality then bounds the fraction of draws retaining at least `n / 2` heavy +entries by `2 * (1 + 4 * c * M) / (n * ρ)` when `ρ ≤ 1`. + +The slice is arbitrary: it may condition on a narrower endpoint channel and a start channel, +provided its explicit pair bound holds. No independence among the heavy-entry hits is required. +The division-free estimate also permits an empty slice or zero capacity. This is the counting +part of [OpenAI2026LogSpace, Lemma 8.4]; weighting deterministic mean errors and the complete +integrated compression bound are separate steps. + +## Main definitions + +* `Cslib.Probability.heavyCountEvent`: at least half the capacity is truly heavy and retained. + +## Main results + +* `Cslib.Probability.card_filter_heavy_mul_le`: the deterministic heavy-set mass bound. +* `Cslib.Probability.card_filter_heavyCountEvent_mul_le`: rarity without division. +* `Cslib.Probability.card_filter_heavyCountEvent_le`: the explicit conditional rarity factor. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.4, Lemma 8.4, equation labelled `buf-rarity` + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Cslib.Probability + +variable {Ω V : Type*} [Fintype V] + +open Classical in +/-- A true heavy count at floor `ρ`: at least half the capacity `n` consists of retained +endpoints whose deterministic first signal exceeds `ρ / 4`. -/ +@[expose] def heavyCountEvent (Y : Ω → V → Prop) (d : V → ℝ) (ρ : ℝ) (n : ℕ) + (σ : Ω) : Prop := + n ≤ 2 * #{w | Y σ w ∧ ρ / 4 < d w} + +/-- The deterministic mass bounds the number of entries above a quarter of the floor. +The multiplied form remains valid at zero scale and for every floor. -/ +theorem card_filter_heavy_mul_le {a ρ M : ℝ} {d : V → ℝ} (ha : 0 ≤ a) + (hd : ∀ w, 0 ≤ d w) (hmass : a * ∑ w, d w ≤ M) : + (#{w | ρ / 4 < d w} : ℝ) * (a * ρ) ≤ 4 * M := by + classical + have hcount : (#{w | ρ / 4 < d w} : ℝ) * (ρ / 4) ≤ ∑ w, d w := + card_filter_mul_le_sum univ _ d (fun w _ => hd w) fun _ _ hw => hw.le + have h := (mul_le_mul_of_nonneg_left hcount ha).trans hmass + linarith + +open Classical in +/-- Conditional rarity of a true heavy count, without division. The endpoint `y` may be +forced by the conditioning slice, while all other endpoints satisfy its pair-count bound. +The slice and the capacity may be empty or zero. -/ +theorem card_filter_heavyCountEvent_mul_le (Y : Ω → V → Prop) (T : Finset Ω) (y : V) + {d : V → ℝ} {a ρ c M : ℝ} (ha : 0 < a) (hρ : 0 < ρ) (hc : 0 ≤ c) + (hd : ∀ w, 0 ≤ d w) (hmass : a * ∑ w, d w ≤ M) + (hpair : ∀ w, w ≠ y → (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T) (n : ℕ) : + (#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) * n * ρ ≤ + #T * (2 * (ρ + 4 * c * M)) := by + classical + let D : Finset V := {w | ρ / 4 < d w} + have hfilter (σ : Ω) : ({w ∈ D | Y σ w} : Finset V) = + ({w | Y σ w ∧ ρ / 4 < d w} : Finset V) := by + ext w + simp [D, and_comm] + have hevent (σ : Ω) : (n + 1) / 2 ≤ #{w ∈ D | Y σ w} ↔ + heavyCountEvent Y d ρ n σ := by + rw [hfilter] + unfold heavyCountEvent + omega + have hcount := card_filter_le_card_filter_mul_le Y T D y (mul_nonneg hc ha.le) + (fun w _ hw => hpair w hw) ((n + 1) / 2) + simp only [hevent] at hcount + have hn : (n : ℝ) ≤ 2 * (((n + 1) / 2 : ℕ) : ℝ) := by + exact_mod_cast (show n ≤ 2 * ((n + 1) / 2) by omega) + have hmassD : (#D : ℝ) * (a * ρ) ≤ 4 * M := + card_filter_heavy_mul_le ha.le hd hmass + have hmassc : c * a * #D * ρ ≤ 4 * c * M := by + have h := mul_le_mul_of_nonneg_left hmassD hc + nlinarith + calc + _ ≤ (#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) * + (2 * (((n + 1) / 2 : ℕ) : ℝ)) * ρ := + mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hn (by positivity)) hρ.le + _ = 2 * ((#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) * + (((n + 1) / 2 : ℕ) : ℝ)) * ρ := by ring + _ ≤ 2 * (#T * (1 + c * a * #D)) * ρ := + mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hcount (by norm_num)) hρ.le + _ = #T * (2 * (ρ + c * a * #D * ρ)) := by ring + _ ≤ #T * (2 * (ρ + 4 * c * M)) := + mul_le_mul_of_nonneg_left + (mul_le_mul_of_nonneg_left (add_le_add le_rfl hmassc) (by norm_num)) (by positivity) + +open Classical in +/-- The conditional rarity factor `2 * (1 + 4 * c * M) / (n * ρ)` for a positive capacity +and a floor in `(0, 1]`. Empty slices require no special convention. -/ +theorem card_filter_heavyCountEvent_le (Y : Ω → V → Prop) (T : Finset Ω) (y : V) + {d : V → ℝ} {a ρ c M : ℝ} (ha : 0 < a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) + (hc : 0 ≤ c) (hd : ∀ w, 0 ≤ d w) (hmass : a * ∑ w, d w ≤ M) + (hpair : ∀ w, w ≠ y → (#{σ ∈ T | Y σ w} : ℝ) ≤ c * a * #T) + {n : ℕ} (hn : 0 < n) : + (#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) ≤ + (2 * (1 + 4 * c * M) / ((n : ℝ) * ρ)) * #T := by + classical + have h := card_filter_heavyCountEvent_mul_le Y T y ha hρ hc hd hmass hpair n + have hn' : (0 : ℝ) < n := by exact_mod_cast hn + rw [div_mul_eq_mul_div, le_div_iff₀ (mul_pos hn' hρ)] + calc + _ = (#{σ ∈ T | heavyCountEvent Y d ρ n σ} : ℝ) * n * ρ := by ring + _ ≤ #T * (2 * (ρ + 4 * c * M)) := h + _ ≤ #T * (2 * (1 + 4 * c * M)) := + mul_le_mul_of_nonneg_left + (mul_le_mul_of_nonneg_left (add_le_add hρ1 le_rfl) (by norm_num)) (by positivity) + _ = _ := by ring + +end Cslib.Probability diff --git a/Complexity/Foundations/Probability/HeavyCountRarity.lean b/Complexity/Foundations/Probability/HeavyCountRarity.lean new file mode 100644 index 000000000..e1891c7a3 --- /dev/null +++ b/Complexity/Foundations/Probability/HeavyCountRarity.lean @@ -0,0 +1,181 @@ +/- +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.HeavyCount +import Mathlib.Algebra.Order.BigOperators.Expect +import Mathlib.Algebra.BigOperators.Field +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Conditional rarity and deterministic mean errors + +A rare row event reduces the integrated contribution of a deterministic endpoint error +by its conditional probability, even when endpoint retention events are dependent. +The conditioning slice includes both the source and the endpoint. Empty slices and empty +environments are allowed: the hypotheses use cardinalities instead of conditional division. + +The error table `b x y` is independent of the environment. The row quantity may depend on +which endpoints were retained, provided its power is bounded by the sum of endpoint error +powers. This includes the retained-row supremum used in the compression argument. +Arbitrary random noise cannot use the same rarity factor, since it may be concentrated on +the rare event. + +These are the integrated, exponent-parametric assertions in the proof of +[OpenAI2026LogSpace, Lemma 8.4, Section 8.4], at revision `7ef5c0cc`. They apply in particular +to fourth moments. They do not assert the recursive estimator's induction or space bound. + +## Main results + +* `Cslib.rowNormPow_event_le`: conditional rarity contracts deterministic endpoint errors. +* `Cslib.vertexNormPow_event_le_rowNormPow`: the corresponding bound for a row error dominated + by the endpoint error powers. +* `Cslib.vertexNormPow_kthLargest_event_le`: rarity bounds the actual retained-row maximum. +* `Cslib.vertexNormPow_heavyCountEvent_le`: the bound with the concrete heavy-count event and + its explicit factor derived from the row-mass and conditional pair estimates. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.4, Lemma 8.4, revision `7ef5c0cc` (preprint, not peer reviewed). +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Cslib + +variable {Ω V : Type*} [Fintype Ω] [Fintype V] + +private theorem sum_masked_const_le {ι : Type*} [Fintype ι] + (E F : Ω → ι → Prop) [∀ σ i, Decidable (E σ i)] [∀ σ i, Decidable (F σ i)] + (w : ι → ℝ) (hw : ∀ i, 0 ≤ w i) {q : ℝ} + (h : ∀ i, (#{σ | E σ i} : ℝ) ≤ q * #{σ | F σ i}) : + (∑ σ, ∑ i, if E σ i then w i else 0) ≤ + q * ∑ σ, ∑ i, if F σ i then w i else 0 := by + rw [sum_comm, sum_comm (f := fun σ i => if F σ i then w i else 0), mul_sum] + refine sum_le_sum fun i _ => ?_ + simp only [← sum_filter, sum_const, nsmul_eq_mul] + exact (mul_le_mul_of_nonneg_right (h i) (hw i)).trans_eq (by ring) + +variable {s : ℕ} {N u : ℝ} {X Y Θ : Ω → V → Prop} + [∀ σ x, Decidable (X σ x)] [∀ σ y, Decidable (Y σ y)] + [∀ σ x, Decidable (Θ σ x)] + +/-- Conditional rarity on each source/endpoint slice contracts the integrated power norm of +a deterministic error table. The exponent is positive; zero powers do not preserve masking. +No independence between the two masks or the row event is required. -/ +theorem rowNormPow_event_le (hs : s ≠ 0) (hNu : 0 ≤ N * u) {q : ℝ} + (hrare : ∀ x y, (#{σ | X σ x ∧ Y σ y ∧ Θ σ x} : ℝ) ≤ + q * #{σ | X σ x ∧ Y σ y}) (b : V → V → ℝ) : + rowNormPow s N u X Y (fun σ x y => if Θ σ x then b x y else 0) ≤ + q * rowNormPow s N u X Y (fun _ x y => b x y) := by + have hsum := sum_masked_const_le + (fun σ (i : V × V) => X σ i.1 ∧ Y σ i.2 ∧ Θ σ i.1) + (fun σ (i : V × V) => X σ i.1 ∧ Y σ i.2) + (fun i => |b i.1 i.2| ^ s) (fun _ => by positivity) (fun i => hrare i.1 i.2) + have hpoint (σ : Ω) : + (∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), + |if Θ σ x then b x y else 0| ^ s) = + ∑ i : V × V, if X σ i.1 ∧ Y σ i.2 ∧ Θ σ i.1 then |b i.1 i.2| ^ s else 0 := by + rw [Fintype.sum_prod_type, sum_filter] + refine sum_congr rfl fun x _ => ?_ + by_cases hx : X σ x <;> by_cases hΘ : Θ σ x <;> simp [hx, hΘ, sum_filter, hs] + have hpoint' (σ : Ω) : + (∑ x ∈ ({x | X σ x} : Finset V), ∑ y ∈ ({y | Y σ y} : Finset V), |b x y| ^ s) = + ∑ i : V × V, if X σ i.1 ∧ Y σ i.2 then |b i.1 i.2| ^ s else 0 := by + rw [Fintype.sum_prod_type, sum_filter] + refine sum_congr rfl fun x _ => ?_ + by_cases hx : X σ x <;> simp [hx, sum_filter] + simp only [rowNormPow, expect_eq_sum_div_card, card_univ, hpoint, hpoint'] + calc + _ ≤ (N * u)⁻¹ * + ((q * ∑ σ, ∑ i : V × V, + if X σ i.1 ∧ Y σ i.2 then |b i.1 i.2| ^ s else 0) / Fintype.card Ω) := + mul_le_mul_of_nonneg_left + (div_le_div_of_nonneg_right hsum (Nat.cast_nonneg _)) (inv_nonneg.mpr hNu) + _ = _ := by ring + +/-- A retained-row supremum, or any row error dominated by the sum of deterministic endpoint +error powers, gains the same conditional rarity factor. Dependence of the row quantity on the +retained set is allowed; the endpoint magnitudes `b x y` are fixed. -/ +theorem vertexNormPow_event_le_rowNormPow (hs : s ≠ 0) (hNu : 0 ≤ N * u) {q : ℝ} + (hrare : ∀ x y, (#{σ | X σ x ∧ Y σ y ∧ Θ σ x} : ℝ) ≤ + q * #{σ | X σ x ∧ Y σ y}) (b : V → V → ℝ) (v : Ω → V → ℝ) + (hv : ∀ σ x, X σ x → |v σ x| ^ s ≤ + ∑ y ∈ ({y | Y σ y} : Finset V), |b x y| ^ s) : + vertexNormPow s N u X (fun σ x => if Θ σ x then v σ x else 0) ≤ + q * rowNormPow s N u X Y (fun _ x y => b x y) := by + calc + _ ≤ rowNormPow s N u X Y (fun σ x y => if Θ σ x then b x y else 0) := by + unfold vertexNormPow rowNormPow + refine mul_le_mul_of_nonneg_left (expect_le_expect fun σ _ => ?_) (inv_nonneg.mpr hNu) + refine sum_le_sum fun x hx => ?_ + by_cases hΘ : Θ σ x + · simp only [hΘ, ↓reduceIte] + exact hv σ x (mem_filter.mp hx).2 + · simp [hΘ, hs] + _ ≤ _ := rowNormPow_event_le hs hNu hrare b + +omit [Fintype V] in +private theorem abs_kthLargest_pow_le_sum (S : Finset V) (b : V → ℝ) + (hs : s ≠ 0) : |kthLargest 1 S (fun y => |b y|)| ^ s ≤ ∑ y ∈ S, |b y| ^ s := by + classical + have hmem : kthLargest 1 S (fun y => |b y|) ∈ + insert 0 ((S.filter fun y => 1 ≤ #{w ∈ S | |b y| ≤ |b w|}).image fun y => |b y|) := + max'_mem _ _ + rcases mem_insert.mp hmem with hz | hmem + · rw [hz, abs_zero, zero_pow hs] + positivity + · obtain ⟨y, hy, heq⟩ := mem_image.mp hmem + rw [← heq, abs_abs] + exact single_le_sum (f := fun y => |b y| ^ s) + (fun _ _ => by positivity) (mem_filter.mp hy).1 + +/-- Conditional rarity controls the maximum deterministic error magnitude among retained +endpoints, with zero as the maximum of an empty row. -/ +theorem vertexNormPow_kthLargest_event_le (hs : s ≠ 0) (hNu : 0 ≤ N * u) {q : ℝ} + (hrare : ∀ x y, (#{σ | X σ x ∧ Y σ y ∧ Θ σ x} : ℝ) ≤ + q * #{σ | X σ x ∧ Y σ y}) (b : V → V → ℝ) : + vertexNormPow s N u X (fun σ x => + if Θ σ x then kthLargest 1 {y | Y σ y} (fun y => |b x y|) else 0) ≤ + q * rowNormPow s N u X Y (fun _ x y => b x y) := + vertexNormPow_event_le_rowNormPow hs hNu hrare b _ + (fun _ _ _ => abs_kthLargest_pow_le_sum _ _ hs) + +open Classical in +/-- **The heavy-count rarity gain for a retained-row mean error.** The pair bound is stated on +the actual source/usage-endpoint slice. The rank channel `Y` may have a wider rate than `Yt`; +only the explicit conditional bound is used. This is the mean-error portion of +[OpenAI2026LogSpace, Lemma 8.4], with an explicit constant and arbitrary positive exponent. -/ +theorem vertexNormPow_heavyCountEvent_le (hs : s ≠ 0) (hNu : 0 ≤ N * u) + (X Y Yt : Ω → V → Prop) [∀ σ x, Decidable (X σ x)] [∀ σ y, Decidable (Yt σ y)] + {a ρ c M : ℝ} {n : ℕ} (ha : 0 < a) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) + (hc : 0 ≤ c) (hn : 0 < n) (d : V → V → ℝ) (hd : ∀ x y, 0 ≤ d x y) + (hmass : ∀ x, a * ∑ y, d x y ≤ M) + (hpair : ∀ x y w, w ≠ y → + (#{σ | X σ x ∧ Yt σ y ∧ Y σ w} : ℝ) ≤ + c * a * #{σ | X σ x ∧ Yt σ y}) (b : V → V → ℝ) : + vertexNormPow s N u X (fun σ x => + if Probability.heavyCountEvent Y (d x) ρ n σ then + kthLargest 1 {y | Yt σ y} (fun y => |b x y|) else 0) ≤ + (2 * (1 + 4 * c * M) / ((n : ℝ) * ρ)) * + rowNormPow s N u X Yt (fun _ x y => b x y) := by + classical + refine vertexNormPow_kthLargest_event_le hs hNu (fun x y => ?_) b + have h := Probability.card_filter_heavyCountEvent_le Y + ({σ | X σ x ∧ Yt σ y} : Finset Ω) y ha hρ hρ1 hc (hd x) (hmass x) + (fun w hwy => ?_) hn + · simpa only [filter_filter, and_assoc] using h + · simpa only [filter_filter, and_assoc] using hpair x y w hwy + +end Cslib 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/Probability/PairwiseIndependentHash/HeavyCount.lean b/Complexity/Probability/PairwiseIndependentHash/HeavyCount.lean new file mode 100644 index 000000000..65235d660 --- /dev/null +++ b/Complexity/Probability/PairwiseIndependentHash/HeavyCount.lean @@ -0,0 +1,74 @@ +/- +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.HeavyCount +public import Complexity.Probability.PairwiseIndependentHash.AtomChannels +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# Heavy-count rarity for affine retention channels + +The conditional heavy-count bound applies to the actual affine retention channels with nominal +rate `a ^ H` and box side `⌈P * a⌉`. Conditioning on a specified endpoint retained by any narrower +box of side `L_t` preserves the off-diagonal pair bound `2 ^ H * a ^ H`. Thus a nonnegative row +of nominal mass at most `M` retains at least half of a positive capacity `n` above floor `ρ / 4` +on at most a `2 * (1 + 4 * 2 ^ H * M) / (n * ρ)` fraction of these conditional draws. + +The result concerns the true heavy-count event on the actual shared seed. It assumes neither +independence among retained endpoints nor a rarity hypothesis. An empty conditioning slice is +allowed. This supplies the affine-channel instance of [OpenAI2026LogSpace, Lemma 8.4]. + +## Main results + +* `Cslib.Probability.card_heavyCountEvent_affineRetains_le`: rarity after a narrower endpoint hit. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.4, Lemma 8.4 (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Cslib.Probability + +open Classical in +/-- The true heavy count for the actual affine channel is rare even after conditioning on +a hit at a narrower rate. Its nominal row-mass scale is `a ^ H`, not the box side `a`. -/ +theorem card_heavyCountEvent_affineRetains_le {V : Type*} [Fintype V] {P H : ℕ} + [Fact P.Prime] {ident : V → ZMod P} (hident : Function.Injective ident) + {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) {Lt : ℕ} (hLt : Lt ≤ ⌈P * a⌉₊) + {d : V → ℝ} {ρ M : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) + (hd : ∀ w, 0 ≤ d w) (hmass : a ^ H * ∑ w, d w ≤ M) {n : ℕ} (hn : 0 < n) (y : V) : + (#{s | affineRetains P H Lt s (ident y) ∧ + heavyCountEvent (fun s w => affineRetains P H ⌈P * a⌉₊ s (ident w)) d ρ n s} : ℝ) ≤ + (2 * (1 + 4 * (2 : ℝ) ^ H * M) / ((n : ℝ) * ρ)) * + #{s | affineRetains P H Lt s (ident y)} := by + classical + have ha0 : 0 < a := by + by_contra h + have := mul_nonpos_of_nonneg_of_nonpos (Nat.cast_nonneg P) (not_lt.mp h) + linarith + have hLtP : Lt ≤ P := hLt.trans (affineRetains_rates (H := H) hPa ha).1 + simpa only [filter_filter] using card_filter_heavyCountEvent_le + (fun s w => affineRetains P H ⌈P * a⌉₊ s (ident w)) + ({s | affineRetains P H Lt s (ident y)} : Finset _) y + (pow_pos ha0 H) hρ hρ1 (by positivity : 0 ≤ (2 : ℝ) ^ H) hd hmass + (fun w hwy => by + have h := card_affineRetains_and_affineRetains_le (H := H) hident hPa ha hLtP hwy + convert h using 2 + congr 1 + ext s + simp only [mem_filter, mem_univ, true_and]) hn + +end Cslib.Probability diff --git a/ComplexityTests/HeavyCountRarity.lean b/ComplexityTests/HeavyCountRarity.lean new file mode 100644 index 000000000..123f9aed2 --- /dev/null +++ b/ComplexityTests/HeavyCountRarity.lean @@ -0,0 +1,237 @@ +/- +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.HeavyCount +import Complexity.Foundations.Probability.HeavyCountRarity +import Complexity.Probability.PairwiseIndependentHash.HeavyCount +import Mathlib.Tactic.NormNum + +/-! +# Tests for heavy-count rarity and deterministic mean errors + +The heavy endpoints in the first example are perfectly correlated except for one always-kept +endpoint. The integrated examples use a separate event coordinate, correlated source/endpoint +masks, and nonzero signed fourth-moment errors. A noise counterexample records why the mean +error must be independent of the environment after fixing the source and endpoint. +-/ + +namespace ComplexityTests.HeavyCountRarity + +open Finset Cslib Cslib.Probability +open scoped BigOperators + +private abbrev correlated (σ y : Fin 5) : Prop := y = 0 ∨ σ = 0 + +-- All four non-forced endpoints appear together with probability `1/5`. +example : ({σ | correlated σ 1 ∧ correlated σ 2} : Finset (Fin 5)) = {0} := by + decide + +private theorem heavy_iff (σ : Fin 5) : + heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ ↔ σ = 0 := by + classical + by_cases hσ : σ = 0 + · subst σ + norm_num [heavyCountEvent, correlated] + · have hsingle : ({y : Fin 5 | y = 0} : Finset (Fin 5)) = {0} := by + ext y + simp + norm_num [heavyCountEvent, correlated, hσ, hsingle] + +-- The rare event has positive probability, and the explicit upper bound is below one. +open scoped Classical in +example : (dens {σ | heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ} : ℝ) = 1 / 5 := by + classical + have hevent : ({σ | heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ} : + Finset (Fin 5)) = {0} := by + ext σ + simp only [mem_filter, mem_univ, true_and, mem_singleton] + exact heavy_iff σ + rw [hevent, dens_eq_card_div_card] + norm_num + +open scoped Classical in +example : (#{σ : Fin 5 | heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ} : ℝ) ≤ + (7 / 12) * Fintype.card (Fin 5) := by + classical + have hpair : ∀ y : Fin 5, y ≠ 0 → + (#{σ ∈ (univ : Finset (Fin 5)) | correlated σ y} : ℝ) ≤ + (1 : ℝ) * (1 / 5) * #(univ : Finset (Fin 5)) := by + intro y hy + have hs : ({σ : Fin 5 | correlated σ y} : Finset (Fin 5)) = {0} := by + ext σ + simp [correlated, hy] + norm_num [hs] + have h := @card_filter_heavyCountEvent_le (Fin 5) (Fin 5) (inferInstance : Fintype (Fin 5)) + correlated univ (0 : Fin 5) + (a := 1 / 5) (ρ := 1) (c := 1) (M := 1 / 3) (d := fun _ => 1 / 3) + (by norm_num) (by norm_num) (by norm_num) (by norm_num) + (fun _ => by norm_num) (by norm_num) + (by + intro w hw + convert hpair w hw using 1 + congr 2 + ext σ + simp) (n := 8) (by decide) + norm_num at h ⊢ + exact h + +-- An odd capacity requires rounding up; equality with the heavy threshold is excluded. +example : ¬ heavyCountEvent (fun (_ : Unit) (y : Fin 3) => y = 0) + (fun _ => 1) 1 3 () := by + classical + norm_num [heavyCountEvent, show ({y : Fin 3 | y = 0} : Finset (Fin 3)) = {0} by decide] + +example : heavyCountEvent (fun (_ : Unit) (y : Fin 3) => y ≠ 2) + (fun _ => 1) 1 3 () := by + classical + norm_num [heavyCountEvent, show ({y : Fin 3 | y ≠ 2} : Finset (Fin 3)) = {0, 1} by decide] + +example : ¬ heavyCountEvent (fun (_ : Unit) (_ : Fin 3) => True) + (fun _ => 1 / 4) 1 1 () := by + classical + norm_num [heavyCountEvent] + +private abbrev kept (σ : Fin 2 × Fin 2) (x : Fin 2) : Prop := σ.1 = x +private abbrev rare (σ : Fin 2 × Fin 2) (_ : Fin 2) : Prop := σ.2 = 0 +private def meanError (x _ : Fin 2) : ℝ := if x = 0 then -2 else 3 + +private theorem rare_on_slice (x y : Fin 2) : + (#{σ | kept σ x ∧ kept σ y ∧ rare σ x} : ℝ) ≤ + (1 / 2) * #{σ | kept σ x ∧ kept σ y} := by + have hn : ∀ x y : Fin 2, #{σ | kept σ x ∧ kept σ y ∧ rare σ x} = + if x = y then 1 else 0 := by decide + have hd : ∀ x y : Fin 2, #{σ | kept σ x ∧ kept σ y} = + if x = y then 2 else 0 := by decide + rw [hn, hd] + split_ifs <;> norm_num + +example : + rowNormPow 4 2 (1 / 2) kept kept + (fun σ x y => if rare σ x then meanError x y else 0) ≤ + (1 / 2) * rowNormPow 4 2 (1 / 2) kept kept (fun _ x y => meanError x y) := + rowNormPow_event_le (by decide) (by norm_num) rare_on_slice meanError + +example : + vertexNormPow 4 2 (1 / 2) kept (fun σ x => + if rare σ x then kthLargest 1 {y | kept σ y} (fun y => |meanError x y|) else 0) ≤ + (1 / 2) * rowNormPow 4 2 (1 / 2) kept kept (fun _ x y => meanError x y) := + vertexNormPow_kthLargest_event_le (by decide) (by norm_num) rare_on_slice meanError + +example : + vertexNormPow 4 2 (1 / 2) kept + (fun σ x => if rare σ x then meanError x x else 0) ≤ + (1 / 2) * rowNormPow 4 2 (1 / 2) kept kept (fun _ x y => meanError x y) := by + apply vertexNormPow_event_le_rowNormPow (by decide) (by norm_num) rare_on_slice meanError + (fun _ x => meanError x x) + intro σ x hx + have hY : ({y | kept σ y} : Finset (Fin 2)) = {x} := by + ext y + simp only [mem_filter, mem_univ, true_and, mem_singleton, kept] + rw [show σ.1 = x from hx] + exact eq_comm + rw [hY, sum_singleton] + +private theorem card_kept (x : Fin 2) : #{y : Fin 2 | x = y} = 1 := by + have h : ({y : Fin 2 | x = y} : Finset (Fin 2)) = {x} := by + ext y + simp [eq_comm] + rw [h, card_singleton] + +private theorem full_mean_power : + rowNormPow 4 2 (1 / 2) kept kept (fun _ x y => meanError x y) = 97 / 2 := by + norm_num [rowNormPow, kept, meanError, sum_filter, expect_eq_sum_div_card, + Fintype.sum_prod_type, Fin.sum_univ_two, card_kept] + +private theorem masked_mean_power : + rowNormPow 4 2 (1 / 2) kept kept + (fun σ x y => if rare σ x then meanError x y else 0) = 97 / 4 := by + norm_num [rowNormPow, kept, rare, meanError, sum_filter, expect_eq_sum_div_card, + Fintype.sum_prod_type, Fin.sum_univ_two, card_kept] + +-- Both means are nonzero, and masking halves the integrated fourth moment exactly. +example : + rowNormPow 4 2 (1 / 2) kept kept + (fun σ x y => if rare σ x then meanError x y else 0) = + (1 / 2) * rowNormPow 4 2 (1 / 2) kept kept (fun _ x y => meanError x y) := by + rw [masked_mean_power, full_mean_power] + norm_num + +private def noise (σ : Fin 2 × Fin 2) (x y : Fin 2) : ℝ := + if rare σ x then meanError x y else 0 + +-- Environment-dependent noise concentrated on the rare event receives no rarity gain. +example : + ¬ rowNormPow 4 2 (1 / 2) kept kept + (fun σ x y => if rare σ x then noise σ x y else 0) ≤ + (1 / 2) * rowNormPow 4 2 (1 / 2) kept kept noise := by + norm_num [rowNormPow, kept, rare, noise, meanError, sum_filter, expect_eq_sum_div_card, + Fintype.sum_prod_type, Fin.sum_univ_two, card_kept] + +-- Empty conditioning slices and an empty environment have zero integrated contribution. +example : rowNormPow 4 2 (1 / 2) (fun (_ : Fin 2 × Fin 2) (_ : Fin 2) => False) + kept (fun _ x y => meanError x y) = 0 := by + simp [rowNormPow] + +example : rowNormPow 4 1 1 (fun (_ : Empty) (_ : Fin 1) => True) + (fun _ _ => True) (fun _ _ _ => 5) = 0 := by + simp [rowNormPow] + +private instance : Fact (Nat.Prime 5) := ⟨by decide⟩ + +-- The concrete affine channel has a conditional bound strictly below one. +open scoped Classical in +example : + (#{σ | affineRetains 5 1 1 σ 0 ∧ heavyCountEvent + (fun σ (y : ZMod 5) => affineRetains 5 1 1 σ y) (fun _ => 1 / 3) 1 8 σ} : ℝ) ≤ + (11 / 12) * #{σ | affineRetains 5 1 1 σ 0} := by + classical + have h := card_heavyCountEvent_affineRetains_le + (V := ZMod 5) (P := 5) (H := 1) (ident := id) Function.injective_id + (a := 1 / 5) (by norm_num) (by norm_num) (Lt := 1) (by norm_num) + (d := fun _ => 1 / 3) (ρ := 1) (M := 1 / 3) + (by norm_num) (by norm_num) (fun _ => by norm_num) (by norm_num) + (n := 8) (by decide) 0 + norm_num at h ⊢ + exact h + +private abbrev forced (_ : Fin 5) (y : Fin 5) : Prop := y = 0 + +-- The actual nonempty heavy event controls the retained maximum after narrowing the usage mask. +open scoped Classical in +example : + vertexNormPow 4 5 1 (fun (_ _ : Fin 5) => True) (fun σ _ => + if heavyCountEvent correlated (fun _ => 1 / 3) 1 8 σ then + kthLargest 1 {y | forced σ y} (fun _ => |(2 : ℝ)|) else 0) ≤ + (7 / 12) * rowNormPow 4 5 1 (fun (_ _ : Fin 5) => True) forced (fun _ _ _ => 2) := by + classical + have hpair : ∀ x y w : Fin 5, w ≠ y → + (#{σ | True ∧ forced σ y ∧ correlated σ w} : ℝ) ≤ + (1 : ℝ) * (1 / 5) * #{σ | True ∧ forced σ y} := by + intro _ y w hwy + by_cases hy : y = 0 + · subst y + have hs : ({σ : Fin 5 | correlated σ w} : Finset (Fin 5)) = {0} := by + ext σ + simp [correlated, hwy] + norm_num [forced, hs] + · simp [forced, hy] + have h := vertexNormPow_heavyCountEvent_le (Ω := Fin 5) (V := Fin 5) + (s := 4) (N := 5) (u := 1) + (by decide) (by norm_num) (fun (_ _ : Fin 5) => True) correlated forced + (a := 1 / 5) (ρ := 1) (c := 1) (M := 1 / 3) (n := 8) + (by norm_num) (by norm_num) (by norm_num) (by norm_num) (by decide) + (fun _ _ => 1 / 3) (fun _ _ => by norm_num) (fun _ => by norm_num) + (by + intro x y w hwy + convert hpair x y w hwy using 1 + congr 2 + ext σ + simp) (fun _ _ => 2) + have hfactor : (2 * (1 + 4 * (1 : ℝ) * (1 / 3)) / (((8 : ℕ) : ℝ) * 1)) = 7 / 12 := by + norm_num + rw [hfactor] at h + exact h + +end ComplexityTests.HeavyCountRarity