feat(logspace): bound heavy-count rarity and masked mean errors

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

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

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

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