diff --git a/Complexity.lean b/Complexity.lean index ced41512e6..2355a1ec49 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2720,6 +2720,7 @@ public import Complexity.Foundations.Order.BooleanSubalgebra public import Complexity.Foundations.Order.Changes public import Complexity.Foundations.Order.UpperLower public import Complexity.Foundations.Probability.ColumnDetector +public import Complexity.Foundations.Probability.CorrectionAtom public import Complexity.Foundations.Probability.DetectedHierarchy public import Complexity.Foundations.Probability.DetectedStage public import Complexity.Foundations.Probability.Gaussian.Multivariate @@ -2991,6 +2992,7 @@ public import Complexity.Probability.PMF.UniformSubset public import Complexity.Probability.PairwiseIndependent 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.HierarchyChannels public import Complexity.Probability.PairwiseIndependentHash.Retention diff --git a/Complexity/Foundations/Data/Finset/KthLargest.lean b/Complexity/Foundations/Data/Finset/KthLargest.lean index b1198aef36..33b6107d35 100644 --- a/Complexity/Foundations/Data/Finset/KthLargest.lean +++ b/Complexity/Foundations/Data/Finset/KthLargest.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Init +public import Mathlib.Algebra.Order.Group.Abs public import Mathlib.Data.Finset.Max /-! @@ -31,6 +32,8 @@ is at least `t` exactly when at least `k` values are at least `t` (`Finset.le_kt * `Finset.kthLargest_nonneg`, `Finset.kthLargest_le`: bounds. * `Finset.lt_kthLargest_iff`, `Finset.le_kthLargest_iff`: the threshold characterizations. +* `Finset.kthLargest_le_kthLargest_add`, `Finset.abs_kthLargest_sub_kthLargest_le`: stability + under perturbation of the values. ## References @@ -113,4 +116,37 @@ theorem le_kthLargest_iff (hk : 0 < k) (ht : 0 < t) : obtain ⟨x, hxs, htx, hkx⟩ := exists_le_card hk (t ≤ ·) hcard exact htx.trans (le_kthLargest_of_le_card hxs hkx) +section Stability + +variable {R : Type*} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] {k : ℕ} + {s : Finset α} {h₁ h₂ : α → R} {ε : R} + +/-- **Rank stability, one side** [OpenAI2026LogSpace, (5.4)]: if every value of `h₁` exceeds the +corresponding value of `h₂` by at most `ε ≥ 0`, so does the `k`-th largest value. -/ +theorem kthLargest_le_kthLargest_add (hk : 0 < k) (hε : 0 ≤ ε) (h : ∀ x ∈ s, h₁ x ≤ h₂ x + ε) : + kthLargest k s h₁ ≤ kthLargest k s h₂ + ε := by + set r := kthLargest k s h₁ + rcases le_or_gt r ε with hr | hr + · exact hr.trans (le_add_of_nonneg_left kthLargest_nonneg) + have hr0 : 0 < r := hε.trans_lt hr + have hcard := (le_kthLargest_iff hk hr0).mp le_rfl + have hlo : r - ε ≤ kthLargest k s h₂ := by + refine (le_kthLargest_iff hk (sub_pos.mpr hr)).mpr (hcard.trans (card_le_card fun x hx => ?_)) + rw [mem_filter] at hx ⊢ + exact ⟨hx.1, sub_le_iff_le_add.mpr (hx.2.trans (h x hx.1))⟩ + exact sub_le_iff_le_add.mp hlo + +/-- **Rank stability** [OpenAI2026LogSpace, (5.4)]: `|rank_k h₁ − rank_k h₂| ≤ sup |h₁ − h₂|`. +If the values differ by at most `ε ≥ 0` everywhere on `s`, so do their `k`-th largest values. -/ +theorem abs_kthLargest_sub_kthLargest_le (hk : 0 < k) (hε : 0 ≤ ε) + (h : ∀ x ∈ s, |h₁ x - h₂ x| ≤ ε) : |kthLargest k s h₁ - kthLargest k s h₂| ≤ ε := by + rw [abs_sub_le_iff] + constructor + · exact sub_le_iff_le_add'.mpr (kthLargest_le_kthLargest_add hk hε fun x hx => + sub_le_iff_le_add'.mp (le_of_abs_le (h x hx))) + · exact sub_le_iff_le_add'.mpr (kthLargest_le_kthLargest_add hk hε fun x hx => + sub_le_iff_le_add'.mp (le_of_abs_le ((abs_sub_comm _ _).trans_le (h x hx)))) + +end Stability + end Finset diff --git a/Complexity/Foundations/Probability/CorrectionAtom.lean b/Complexity/Foundations/Probability/CorrectionAtom.lean new file mode 100644 index 0000000000..80776f5293 --- /dev/null +++ b/Complexity/Foundations/Probability/CorrectionAtom.lean @@ -0,0 +1,415 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Probability.StochasticAtom +import Complexity.Foundations.Data.Finset.Markov +import Mathlib.Algebra.Order.BigOperators.Expect +import Mathlib.Algebra.BigOperators.Field +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# Correction atoms with an incoming gate + +A *correction atom* represents an entry `Q (G x y / f) · g₀(y)` of a correction matrix as the +conditional mean of a bounded table, like the dense atoms of +`Complexity.Foundations.Probability.StochasticAtom`. Its table also has few nonzero entries in each +*column*. That bound is what lets later error estimates sum over the sources of a column. This is +idea 6 in issue #474, following the OpenAI preprint [OpenAI2026LogSpace, Sections 5.3 and 5.5]. + +**The incoming gate.** A draw is a pair `(s, t)` of independent seeds: `s` for the start channel +`X`, which retains sources, and `t` for the terminal channel (rank channel `Y`, usage channel +`Yt`). The *auxiliary score* of a source `x'` at column `y` is `I (G x' y / f, rank_K {G x' w / f : +Y t w})` (`Matrix.auxScore`). The *incoming gate* of column `y` is +`τ (rank_{K_c} {aux x' y : X s x'})` (`Matrix.incomingGate`) [OpenAI2026LogSpace, (5.12)]. The atom +is +`1{Yt t y} · Q (G x y / f) · R · T_y / c(q_y) · g₀(y)` (`Matrix.correctionAtom`), where `R` is the +row gate of `x`, `T_y` the incoming gate, `c(q) = max (1/2) (min 1 q)`, and `q_y` the conditional +mean of the preparatory value `h (G x y / f) · R · T_y` given `X(x)` and `Yt(y)` +(`Matrix.correctionPrep`, `Matrix.correctionNormalizer`) [OpenAI2026LogSpace, (5.13), (5.14)]. + +**The identity** [OpenAI2026LogSpace, Lemma 5.3]. The conditional mean of the atom is exactly +`Q (G x y / f) · g₀(y)` (`Matrix.expect_correctionAtom`). The row gate fails on at most a quarter +of the conditioning draws, by `Matrix.card_filter_rowGate_lt_one_mul_le`. The auxiliary score can +exceed the gate's threshold only on a fixed set `D` of sources, and the incoming gate fails only +if `K_c` members of `D` are retained (`Matrix.card_filter_incomingGate_lt_one_mul_le`). When +`g₀(y) ≠ 0`, the hypothesis `p · #D ≤ B` (the preprint's column bound (5.2)) makes this rare too. +When `g₀(y) = 0` both sides vanish and no bound on `D` is needed. Both gates are then full on half +of the draws, and the normalization principle (`Finset.expect_mul_div_clip_eq`) applies. The +failure bounds use no independence between gates. + +**The incoming cap** [OpenAI2026LogSpace, (5.18), Lemma 5.6]. If `I = 1` wherever `Q` and `ρ` are +both nonzero, and `τ` vanishes from `g ≤ 1` on, then on every draw a column has fewer than `K_c` +retained sources with a nonzero atom (`Matrix.card_filter_correctionAtom_col_ne_zero_lt`). `K_c` +such sources would all have score one, which closes the incoming gate +(`Matrix.incomingGate_eq_zero`). Rows have fewer than `K` nonzero atoms, as for dense atoms +(`Matrix.card_filter_correctionAtom_row_ne_zero_lt`). + +## Main definitions + +* `Matrix.auxScore`, `Matrix.incomingGate`: the auxiliary score and the incoming gate. +* `Matrix.correctionPrep`, `Matrix.correctionNormalizer`, `Matrix.correctionAtom`: the atom. + +## Main results + +* `Finset.expect_mul_div_clip_eq`: the normalization principle. +* `Finset.card_filter_le_card_filter_mul_le`: few draws retain many members of a sparse set. +* `Matrix.card_filter_incomingGate_lt_one_mul_le`: the incoming gate rarely fails. +* `Matrix.expect_correctionAtom`: the correction atom identity. +* `Matrix.abs_correctionAtom_le`: the atom is bounded. +* `Matrix.incomingGate_eq_zero`, `Matrix.card_filter_correctionAtom_col_ne_zero_lt`, + `Matrix.card_filter_correctionAtom_row_ne_zero_lt`: the incoming cap and the support bounds. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Sections 5.1, 5.3 and 5.5 (preprint, not peer reviewed) +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Finset + +variable {Ω : Type*} + +/-- **The normalization principle** [OpenAI2026LogSpace, Section 5.1]. Let a gate `γ` take values +in `[0, 1]` on a nonempty finite set `S` of draws, and be below one on at most half of them. Then +dividing by its clipped mean `c(q) = max (1/2) (min 1 q)` removes the gate's bias: +`𝔼_S [m · γ / c(𝔼_S γ)] = m`. -/ +theorem expect_mul_div_clip_eq {S : Finset Ω} (hS : S.Nonempty) {γ : Ω → ℝ} + (hγ0 : ∀ s ∈ S, 0 ≤ γ s) (hγ1 : ∀ s ∈ S, γ s ≤ 1) (hfail : 2 * (#{s ∈ S | γ s < 1} : ℝ) ≤ #S) + (m : ℝ) : 𝔼 s ∈ S, m * γ s / max (1 / 2) (min 1 (𝔼 s ∈ S, γ s)) = m := by + have hSr : (0 : ℝ) < #S := by exact_mod_cast hS.card_pos + have hγ : ∀ s ∈ S, 1 - (if γ s < 1 then 1 else 0) ≤ γ s := fun s hs => by + split_ifs with h + · rw [sub_self]; exact hγ0 s hs + · simpa using not_lt.mp h + have hlo : 1 / 2 ≤ 𝔼 s ∈ S, γ s := by + rw [expect_eq_sum_div_card, le_div_iff₀ hSr] + calc 1 / 2 * (#S : ℝ) ≤ #S - #{s ∈ S | γ s < 1} := by linarith + _ = ∑ s ∈ S, (1 - (if γ s < 1 then 1 else 0)) := by + rw [sum_sub_distrib, sum_boole, sum_const, nsmul_eq_mul, mul_one] + _ ≤ ∑ s ∈ S, γ s := sum_le_sum hγ + have hhi : 𝔼 s ∈ S, γ s ≤ 1 := expect_le hS hγ1 + have hpos : 0 < 𝔼 s ∈ S, γ s := lt_of_lt_of_le (by norm_num) hlo + rw [min_eq_right hhi, max_eq_right hlo] + simp only [mul_div_assoc] + rw [← mul_expect, ← expect_div, div_self hpos.ne', mul_one] + +variable {V : Type*} + +/-- **Few draws retain many members of a sparse set** (Markov's inequality). Let every member +`w ≠ x` of `D` be retained on at most a `p` fraction of the draws in `S`. Then at most a +`(1 + p #D) / K` fraction of the draws retain `K > 0` members of `D`. The vertex `x` itself +contributes at most one per draw. -/ +theorem card_filter_le_card_filter_mul_le {ι : Type*} (X : ι → V → Prop) [∀ s v, Decidable (X s v)] + (S : Finset ι) (D : Finset V) (x : V) {p : ℝ} (hp : 0 ≤ p) + (hpair : ∀ w ∈ D, w ≠ x → (#{s ∈ S | X s w} : ℝ) ≤ p * #S) (K : ℕ) : + (#{s ∈ S | K ≤ #{w ∈ D | X s w}} : ℝ) * K ≤ #S * (1 + p * #D) := by + classical + have hMarkov : (#{s ∈ S | K ≤ #{w ∈ D | X s w}} : ℝ) * K ≤ ∑ s ∈ S, (#{w ∈ D | X s w} : ℝ) := + card_filter_mul_le_sum S _ _ (fun _ _ => by positivity) fun s _ hs => by exact_mod_cast hs + have hswap : ∑ s ∈ S, (#{w ∈ D | X s w} : ℝ) = ∑ w ∈ D, (#{s ∈ S | X s w} : ℝ) := by + simp only [natCast_card_filter] + exact sum_comm + have hterm : ∀ w ∈ D, (#{s ∈ S | X s w} : ℝ) ≤ (if x = w then (#S : ℝ) else 0) + p * #S := by + intro w hw + by_cases hxw : x = w + · have hle : (#{s ∈ S | X s w} : ℝ) ≤ #S := by exact_mod_cast card_filter_le _ _ + have : 0 ≤ p * #S := by positivity + simp only [hxw, ↓reduceIte] + linarith + · simp only [hxw, ↓reduceIte, zero_add] + exact hpair w hw (Ne.symm hxw) + calc (#{s ∈ S | K ≤ #{w ∈ D | X s w}} : ℝ) * K + ≤ ∑ w ∈ D, ((if x = w then (#S : ℝ) else 0) + p * #S) := + hMarkov.trans (hswap ▸ sum_le_sum hterm) + _ = (if x ∈ D then (#S : ℝ) else 0) + #D * (p * #S) := by + rw [sum_add_distrib, sum_ite_eq, sum_const, nsmul_eq_mul] + _ ≤ #S * (1 + p * #D) := by + have : (if x ∈ D then (#S : ℝ) else 0) ≤ #S := by split_ifs <;> [exact le_rfl; positivity] + nlinarith + +end Finset + +namespace Matrix + +variable {V ι κ : Type*} [Fintype V] + +section Definitions + +variable (I : ℝ → ℝ → ℝ) (τ : ℝ → ℝ) (K Kc : ℕ) (f : ℝ) (G : Matrix V V ℝ) + +/-- The **auxiliary score** of the entry `(x, y)` for the retained set `T` of the rank channel: +`I (G x y / f, rank_K {G x w / f : w ∈ T})` [OpenAI2026LogSpace, (5.5)]. -/ +@[expose] noncomputable def auxScore (T : Finset V) (x y : V) : ℝ := + I (G x y / f) (kthLargest K T fun w => G x w / f) + +/-- The **incoming gate** of column `y`: `τ (rank_{K_c} {auxScore x y : x ∈ S})` over the retained +set `S` of sources [OpenAI2026LogSpace, (5.12)]. -/ +@[expose] noncomputable def incomingGate (S T : Finset V) (y : V) : ℝ := + τ (kthLargest Kc S fun x => auxScore I K f G T x y) + +variable {ι κ : Type*} [Fintype ι] [Fintype κ] (X : ι → V → Prop) (Y Yt : κ → V → Prop) + [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Y t v)] [∀ t v, Decidable (Yt t v)] + (Q h ρ : ℝ → ℝ) (g₀ : V → ℝ) + +/-- The **preparatory value** of a correction atom: `h (G x y / f) · R · T_y`, with the row gate +`R` and the incoming gate `T_y` [OpenAI2026LogSpace, (5.13)]. -/ +@[expose] noncomputable def correctionPrep (S T : Finset V) (x y : V) : ℝ := + h (G x y / f) * rowGate ρ K f G T x * incomingGate I τ K Kc f G S T y + +/-- The **normalizer** `q_y` of a correction atom: the mean of the preparatory value over the +draws that retain `x` in the start channel and `y` in the usage channel +[OpenAI2026LogSpace, (5.13)]. -/ +@[expose] noncomputable def correctionNormalizer (x y : V) : ℝ := + 𝔼 d ∈ ({s | X s x} : Finset ι) ×ˢ ({t | Yt t y} : Finset κ), + correctionPrep I τ K Kc f G h ρ {w | X d.1 w} {w | Y d.2 w} x y + +/-- The **correction atom** at `(x, y)` on the draw `d = (s, t)`: +`1{Yt t y} · Q (G x y / f) · R · T_y / c(q_y) · g₀(y)` [OpenAI2026LogSpace, (5.14)]. -/ +@[expose] noncomputable def correctionAtom (d : ι × κ) (x y : V) : ℝ := + if Yt d.2 y then + Q (G x y / f) * (rowGate ρ K f G {w | Y d.2 w} x * + incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y) / + max (1 / 2) (min 1 (correctionNormalizer I τ K Kc f G X Y Yt h ρ x y)) * g₀ y + else 0 + +end Definitions + +variable {I : ℝ → ℝ → ℝ} {τ : ℝ → ℝ} {K Kc : ℕ} {f : ℝ} {G : Matrix V V ℝ} + +omit [Fintype V] in +/-- **The incoming cap** [OpenAI2026LogSpace, Lemma 5.6]: if `τ` vanishes from `g ≤ 1` on and at +least `K_c > 0` retained sources have auxiliary score at least one at column `y`, the incoming +gate of `y` is closed. -/ +theorem incomingGate_eq_zero {S T : Finset V} {y : V} (hKc : 0 < Kc) {g : ℝ} (hg : g ≤ 1) + (hτ : ∀ r, g ≤ r → τ r = 0) (hcard : Kc ≤ #{x ∈ S | 1 ≤ auxScore I K f G T x y}) : + incomingGate I τ K Kc f G S T y = 0 := + hτ _ (hg.trans ((le_kthLargest_iff hKc one_pos).mpr hcard)) + +/-- **The incoming gate rarely fails** [OpenAI2026LogSpace, proof of Lemma 5.3]. Let `τ` be one +through `τ₀ ≥ 0` and `I` vanish when its first argument is at most `e`, so a score above `τ₀` +needs a source in `D = {x' | e < G x' y / f}`. If every member `w ≠ x` of `D` is retained on at +most a `p` fraction of the draws in `S`, then for every terminal set `T` the incoming gate is +below one on at most a `(1 + p #D) / K_c` fraction of `S`. -/ +theorem card_filter_incomingGate_lt_one_mul_le (X : ι → V → Prop) + [∀ s v, Decidable (X s v)] (S : Finset ι) (T : Finset V) (x y : V) (hKc : 0 < Kc) + {τ₀ : ℝ} (hτ₀ : 0 ≤ τ₀) (hττ : ∀ r, r ≤ τ₀ → τ r = 1) {e : ℝ} + (hI : ∀ v r, v ≤ e → I v r = 0) {p : ℝ} (hp : 0 ≤ p) + (hpair : ∀ w, e < G w y / f → w ≠ x → (#{s ∈ S | X s w} : ℝ) ≤ p * #S) : + (#{s ∈ S | incomingGate I τ K Kc f G {w | X s w} T y < 1} : ℝ) * Kc ≤ + #S * (1 + p * #({w | e < G w y / f} : Finset V)) := by + set D : Finset V := {w | e < G w y / f} + refine le_trans ?_ (card_filter_le_card_filter_mul_le X S D x hp + (fun w hw hwx => hpair w (by simpa [D] using hw) hwx) Kc) + refine mul_le_mul_of_nonneg_right ?_ (by positivity) + refine Nat.cast_le.mpr (card_le_card fun s hs => ?_) + rw [mem_filter] at hs ⊢ + refine ⟨hs.1, ?_⟩ + have hlt : τ₀ < kthLargest Kc {w | X s w} fun w => auxScore I K f G T w y := by + by_contra hle + rw [incomingGate, hττ _ (not_lt.mp hle)] at hs + exact lt_irrefl _ hs.2 + refine ((lt_kthLargest_iff hKc hτ₀).mp hlt).trans (card_le_card fun w hw => ?_) + rw [mem_filter] at hw ⊢ + refine ⟨?_, by simpa using hw.1⟩ + simp only [D, mem_filter, mem_univ, true_and] + by_contra hle + rw [auxScore, hI _ _ (not_lt.mp hle)] at hw + exact absurd hw.2 (not_lt.mpr hτ₀) + +omit [Fintype V] in +/-- A product of two gates with values in `[0, 1]` is at most one. -/ +private theorem mul_le_one_of_gate {r t : ℝ} (hr : r ≤ 1) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : + r * t ≤ 1 := + (mul_le_mul_of_nonneg_right hr ht0).trans (by rw [one_mul]; exact ht1) + +variable [Fintype ι] [Fintype κ] {X : ι → V → Prop} {Y Yt : κ → V → Prop} + [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Y t v)] [∀ t v, Decidable (Yt t v)] + {Q h ρ : ℝ → ℝ} {g₀ : V → ℝ} + +/-- **The correction atom is bounded**: `|F(x, y)| ≤ 2 |Q (G x y / f)| |g₀(y)|` on every draw, +when the row and incoming gate functions take values in `[0, 1]`. -/ +theorem abs_correctionAtom_le (hρ0 : ∀ r, 0 ≤ ρ r) (hρ1 : ∀ r, ρ r ≤ 1) (hτ0 : ∀ r, 0 ≤ τ r) + (hτ1 : ∀ r, τ r ≤ 1) (d : ι × κ) (x y : V) : + |correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ d x y| ≤ 2 * |Q (G x y / f)| * |g₀ y| := by + rw [correctionAtom] + split_ifs + · set γ := rowGate ρ K f G {w | Y d.2 w} x * + incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y + have hγ0 : 0 ≤ γ := mul_nonneg (hρ0 _) (hτ0 _) + have hγ1 : γ ≤ 1 := mul_le_one_of_gate (hρ1 _) (hτ0 _) (hτ1 _) + set c := max (1 / 2) (min 1 (correctionNormalizer I τ K Kc f G X Y Yt h ρ x y)) + have hc : (1 / 2 : ℝ) ≤ c := le_max_left _ _ + have hc0 : 0 < c := lt_of_lt_of_le (by norm_num) hc + rw [abs_mul, abs_div, abs_mul, abs_of_nonneg hγ0, abs_of_pos hc0] + refine mul_le_mul_of_nonneg_right ?_ (abs_nonneg _) + rw [div_le_iff₀ hc0] + calc |Q (G x y / f)| * γ ≤ |Q (G x y / f)| * 1 := mul_le_mul_of_nonneg_left hγ1 (abs_nonneg _) + _ = 2 * |Q (G x y / f)| * (1 / 2) := by ring + _ ≤ _ := mul_le_mul_of_nonneg_left hc (by positivity) + · rw [abs_zero]; positivity + +/-- **Row support** [OpenAI2026LogSpace, Lemma 5.6]: if `Q` vanishes through `e ≥ 0` and `ρ` +vanishes from `g ≤ e` on, then on every draw fewer than `K > 0` correction atoms of a row are +nonzero among the vertices the rank channel retains. -/ +theorem card_filter_correctionAtom_row_ne_zero_lt (hK : 0 < K) {e g : ℝ} (he : 0 ≤ e) + (hQ : ∀ v, v ≤ e → Q v = 0) (hg : g ≤ e) (hρ : ∀ r, g ≤ r → ρ r = 0) (d : ι × κ) (x : V) : + #{y ∈ ({w | Y d.2 w} : Finset V) | correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ d x y ≠ 0} < + K := by + refine lt_of_le_of_lt (card_le_card fun y hy => ?_) + (card_filter_mul_rowGate_ne_zero_lt (a := f) (G := G) {w | Y d.2 w} x hK he hQ hg hρ) + rw [mem_filter] at hy ⊢ + refine ⟨hy.1, fun h0 => hy.2 ?_⟩ + rw [correctionAtom] + split_ifs + · rw [← mul_assoc, h0, zero_mul, zero_div, zero_mul] + · rfl + +/-- **Column support: the incoming cap** [OpenAI2026LogSpace, (5.18), Lemma 5.6]. Suppose the +auxiliary score is one wherever `Q` and `ρ` are both nonzero, and `τ` vanishes from `g ≤ 1` on. +Then on every draw fewer than `K_c > 0` retained sources have a nonzero atom in column `y`: +`K_c` of them would close the incoming gate, which makes the whole column zero. -/ +theorem card_filter_correctionAtom_col_ne_zero_lt (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) (d : ι × κ) (y : V) : + #{x ∈ ({w | X d.1 w} : Finset V) | correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ d x y ≠ 0} < + Kc := by + by_contra hle + rw [not_lt] at hle + have hgate : incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y = 0 := by + refine incomingGate_eq_zero hKc hg hτ (hle.trans (card_le_card fun x hx => ?_)) + rw [mem_filter] at hx ⊢ + refine ⟨hx.1, le_of_eq (hIQ _ _ (fun hQ => hx.2 ?_) (fun hρ => hx.2 ?_)).symm⟩ + · rw [correctionAtom]; split_ifs <;> simp [hQ] + · rw [correctionAtom]; split_ifs <;> simp [rowGate, hρ] + obtain ⟨x, hx⟩ := card_pos.mp (hKc.trans_le hle) + rw [mem_filter, correctionAtom, hgate] at hx + split_ifs at hx <;> simp at hx + +/-- **The correction atom identity, including zero multipliers** [OpenAI2026LogSpace, Lemma 5.3]. +Let `h = 1` wherever `Q ≠ 0`; let `ρ, τ ∈ [0, 1]`, with `ρ` one through `η > 0` and `τ` one +through `τ₀ ≥ 0`; and let `I` vanish when its first argument is at most `e`. Let row `x` of +`G ≥ 0` have mass at most `M`. Suppose the draws retaining `x` in `X` and `y` in `Yt` are +nonempty, and two pair bounds hold. Every `w ≠ y` is retained by `Y` on at most a `c f` fraction +of the draws with `Yt(y)`. Every `w ≠ x` is retained by `X` on at most a `p` fraction of the draws +with `X(x)`. If `g₀(y) ≠ 0`, let the sources that can score satisfy +`p · #{w | e < G w y / f} ≤ B`. Then, for `K ≥ 4 (1 + c M / η)` and `K_c ≥ 4 (1 + B)`, the +conditional mean of the atom is exactly `Q (G x y / f) · g₀(y)`. -/ +theorem expect_correctionAtom {x y : V} (hSx : ({s | X s x} : Finset ι).Nonempty) + (hSy : ({t | Yt t y} : 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) + (hpairY : ∀ w, w ≠ y → (#{t | Yt t y ∧ Y t w} : ℝ) ≤ c * f * #{t | Yt t y}) {p : ℝ} + (hp : 0 ≤ p) (hpairX : ∀ w, w ≠ x → (#{s | X s x ∧ X s w} : ℝ) ≤ p * #{s | X s x}) {B : ℝ} + (hB : g₀ y ≠ 0 → p * #({w | e < G w y / f} : Finset V) ≤ B) (hKc : 4 * (1 + B) ≤ Kc) : + 𝔼 d ∈ ({s | X s x} : Finset ι) ×ˢ ({t | Yt t y} : Finset κ), + correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ d x y = Q (G x y / f) * g₀ y := by + set Sx : Finset ι := {s | X s x} + set Sy : Finset κ := {t | Yt t y} + set C := Sx ×ˢ Sy + set γ : ι × κ → ℝ := fun d => rowGate ρ K f G {w | Y d.2 w} x * + incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y + -- trivial cases: a zero entry or a zero multiplier + by_cases hz : Q (G x y / f) * g₀ y = 0 + · rw [hz] + refine expect_eq_zero fun d _ => ?_ + rw [correctionAtom] + split_ifs + · rcases mul_eq_zero.mp hz with h0 | h0 <;> simp [h0] + · rfl + obtain ⟨hQ0, hg0⟩ := mul_ne_zero_iff.mp hz + have hh1 : h (G x y / f) = 1 := hQh _ hQ0 + have hSxr : (0 : ℝ) < #Sx := by exact_mod_cast hSx.card_pos + have hSyr : (0 : ℝ) < #Sy := by exact_mod_cast hSy.card_pos + have hM : 0 ≤ M := (sum_nonneg fun w _ => hG0 w).trans hGM + have hKr : (0 : ℝ) < K := by + have : 0 ≤ c * M / η := by positivity + linarith + have hBnn : 0 ≤ B := (by positivity : (0 : ℝ) ≤ p * #({w | e < G w y / f} : Finset V)).trans + (hB hg0) + have hKcr : (0 : ℝ) < Kc := by linarith + -- the row gate fails on at most a quarter of the terminal draws + have hR : (#{t ∈ Sy | rowGate ρ K f G {w | Y t w} x < 1} : ℝ) * 4 ≤ #Sy := by + have h := card_filter_rowGate_lt_one_mul_le Sy x hf hη hρη hG0 hGM (by exact_mod_cast hKr) hc + fun w hwy => by + have hset : ({t ∈ Sy | Y t w} : Finset κ) = ({t | Yt t y ∧ Y t w} : Finset κ) := by + ext t; simp only [Sy, mem_filter, mem_univ, true_and] + rw [hset] + exact hpairY w hwy + nlinarith + -- the incoming gate fails on at most a quarter of the start draws, for every terminal set + have hT : ∀ T : Finset V, + (#{s ∈ Sx | incomingGate I τ K Kc f G {w | X s w} T y < 1} : ℝ) * 4 ≤ #Sx := by + intro T + have h := card_filter_incomingGate_lt_one_mul_le (τ := τ) (K := K) (f := f) (G := G) X Sx T x + y (by exact_mod_cast hKcr) hτ₀ hττ + hI hp fun w _ hwx => by + have hset : ({s ∈ Sx | X s w} : Finset ι) = ({s | X s x ∧ X s w} : Finset ι) := by + ext s; simp only [Sx, mem_filter, mem_univ, true_and] + rw [hset] + exact hpairX w hwx + have h1 : #Sx * (1 + p * #({w | e < G w y / f} : Finset V)) ≤ #Sx * (1 + B) := by + have := hB hg0 + gcongr + nlinarith + -- so the product gate fails on at most half of the conditioning draws + have hfail : 2 * (#{d ∈ C | γ d < 1} : ℝ) ≤ #C := by + have hsplit : ∀ d, (if γ d < 1 then (1 : ℝ) else 0) ≤ + (if rowGate ρ K f G {w | Y d.2 w} x < 1 then 1 else 0) + + (if incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y < 1 then 1 else 0) := by + intro d + by_cases h1 : rowGate ρ K f G {w | Y d.2 w} x < 1 + · split_ifs <;> norm_num + by_cases h2 : incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y < 1 + · split_ifs <;> norm_num + have hr : rowGate ρ K f G {w | Y d.2 w} x = 1 := le_antisymm (hρ1 _) (not_lt.mp h1) + have ht : incomingGate I τ K Kc f G {w | X d.1 w} {w | Y d.2 w} y = 1 := + le_antisymm (hτ1 _) (not_lt.mp h2) + simp only [γ, hr, ht, mul_one, lt_irrefl, ↓reduceIte] + norm_num + have hcount : (#{d ∈ C | γ d < 1} : ℝ) ≤ + #Sx * #{t ∈ Sy | rowGate ρ K f G {w | Y t w} x < 1} + + ∑ t ∈ Sy, (#{s ∈ Sx | incomingGate I τ K Kc f G {w | X s w} {w | Y t w} y < 1} : ℝ) := by + rw [natCast_card_filter] + refine (sum_le_sum fun d _ => hsplit d).trans_eq ?_ + rw [sum_add_distrib, sum_product, sum_product_right] + simp only [sum_const, nsmul_eq_mul, ← natCast_card_filter] + have hsum : (∑ t ∈ Sy, + (#{s ∈ Sx | incomingGate I τ K Kc f G {w | X s w} {w | Y t w} y < 1} : ℝ)) * 4 ≤ + #Sy * #Sx := by + rw [sum_mul] + calc ∑ t ∈ Sy, (#{s ∈ Sx | incomingGate I τ K Kc f G {w | X s w} {w | Y t w} y < 1} : + ℝ) * 4 ≤ ∑ _t ∈ Sy, (#Sx : ℝ) := sum_le_sum fun t _ => hT _ + _ = #Sy * #Sx := by rw [sum_const, nsmul_eq_mul] + have hC : (#C : ℝ) = #Sx * #Sy := by rw [card_product]; push_cast; ring + rw [hC] + nlinarith [mul_le_mul_of_nonneg_left hR hSxr.le] + -- the normalizer is the mean of the product gate, and the normalization principle applies + have hq : correctionNormalizer I τ K Kc f G X Y Yt h ρ x y = 𝔼 d ∈ C, γ d := by + simp only [correctionNormalizer, correctionPrep, hh1, one_mul, γ, C, Sx, Sy] + have hterm : ∀ d ∈ C, correctionAtom I τ K Kc f G X Y Yt Q h ρ g₀ d x y = + Q (G x y / f) * γ d / max (1 / 2) (min 1 (𝔼 d ∈ C, γ d)) * g₀ y := fun d hd => by + have hd' : Yt d.2 y := by simpa [C, Sy] using (mem_product.mp hd).2 + simp only [correctionAtom, hd', ↓reduceIte, hq, γ] + have key : 𝔼 d ∈ C, Q (G x y / f) * γ d / max (1 / 2) (min 1 (𝔼 d ∈ C, γ d)) = + Q (G x y / f) := + expect_mul_div_clip_eq (hSx.product hSy) (fun d _ => mul_nonneg (hρ0 _) (hτ0 _)) + (fun d _ => mul_le_one_of_gate (hρ1 _) (hτ0 _) (hτ1 _)) hfail _ + rw [expect_congr rfl hterm, ← expect_mul, key] + +end Matrix diff --git a/Complexity/Probability/PairwiseIndependentHash/AtomChannels.lean b/Complexity/Probability/PairwiseIndependentHash/AtomChannels.lean new file mode 100644 index 0000000000..f62d31ce64 --- /dev/null +++ b/Complexity/Probability/PairwiseIndependentHash/AtomChannels.lean @@ -0,0 +1,117 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Probability.StochasticAtom +public import Complexity.Probability.PairwiseIndependentHash.RetentionChannel + +/-! +# Dense atoms over affine channels at two rates + +A dense atom (`Matrix.denseAtom`) ranks its row over a channel at the atom's scale `f` and is +masked by a *usage* channel at a lower rate `t ≤ f` [OpenAI2026LogSpace, (5.11)]. For the affine +retention channels over `𝔽_P` both are one seed with two boxes: the usage channel has a smaller +side `L_t ≤ ⌈P a⌉`. So it retains a subset (`Cslib.Probability.affineRetains_of_le`). Given that +the usage channel retains `y`, another identifier `w` is retained at rate `f = a ^ H` with +probability at most `2 ^ H f`, by pairwise independence at two rates +(`Cslib.Probability.card_affineRetains_and_affineRetains_le`). This is the cross-rate pair bound +of [OpenAI2026LogSpace, Lemma 3.1] used in the proof of Lemma 5.1. With it, the dense atom +identity holds for these channels at two rates (`Cslib.Probability.expect_denseAtom_affineRetains`). + +## Main results + +* `Cslib.Probability.card_filter_and_le_of_dens_le`: a conditional probability bound as a count. +* `Cslib.Probability.card_affineRetains_and_affineRetains_le`: the cross-rate pair bound. +* `Cslib.Probability.expect_denseAtom_affineRetains`: the dense atom identity at two rates. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Lemma 3.1 and Lemma 5.1 (preprint, not peer reviewed) +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Cslib.Probability + +variable {V : Type*} {P H : ℕ} [Fact P.Prime] + +omit [Fact P.Prime] in +/-- A **conditional probability bound as a count**: if `Pr[B ∧ A] ≤ q Pr[A]` for uniform seeds, +then among the seeds satisfying `A`, at most a `q` fraction also satisfy `B`. -/ +theorem card_filter_and_le_of_dens_le {Ω : Type*} [Fintype Ω] {A B : Ω → Prop} [DecidablePred A] + [DecidablePred B] {q : ℝ} (h : (dens {t | B t ∧ A t} : ℝ) ≤ q * dens {t | A t}) : + (#{t | A t ∧ B t} : ℝ) ≤ q * #{t | A t} := by + have hcard : ∀ T : Finset Ω, ((dens T : ℚ≥0) : ℝ) = #T / Fintype.card Ω := fun T => by + rw [dens_eq_card_div_card]; push_cast; rfl + rw [hcard, hcard, ← mul_div_assoc] at h + have hset : ({t | A t ∧ B t} : Finset Ω) = ({t | B t ∧ A t} : Finset Ω) := + filter_congr fun _ _ => and_comm + rw [hset] + rcases (Fintype.card Ω).eq_zero_or_pos with h0 | h0 + · have : (univ : Finset Ω) = ∅ := univ_eq_empty_iff.mpr (Fintype.card_eq_zero_iff.mp h0) + simp [this] + · exact (div_le_div_iff_of_pos_right (by exact_mod_cast h0)).mp h + +/-- **The cross-rate pair bound for affine channels.** Let `ident : V → ZMod P` be injective, +`1 ≤ P a`, `a ≤ 1`, and `L_t ≤ P`. Among the seeds whose box of side `L_t` retains `y`, those +whose box of side `⌈P a⌉` also retains `w ≠ y` form at most a `2 ^ H a ^ H` fraction. -/ +theorem card_affineRetains_and_affineRetains_le {ident : V → ZMod P} + (hident : Function.Injective ident) {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) {Lt : ℕ} + (hLt : Lt ≤ P) {w y : V} (hwy : w ≠ y) : + (#{s | affineRetains P H Lt s (ident y) ∧ affineRetains P H ⌈P * a⌉₊ s (ident w)} : ℝ) ≤ + 2 ^ H * a ^ H * #{s | affineRetains P H Lt s (ident y)} := by + obtain ⟨hL, -, hup, -, -⟩ := affineRetains_rates (H := H) hPa ha + refine card_filter_and_le_of_dens_le ?_ + rw [dens_affineRetains_and_affineRetains hL hLt (hident.ne hwy), dens_affineRetains hLt] + push_cast + exact mul_le_mul_of_nonneg_right hup (by positivity) + +/-- **The dense atom identity for affine channels at two rates** [OpenAI2026LogSpace, Lemma 5.1]. +The rank channel retains with side `⌈P a⌉` (rate `f = a ^ H`), the usage channel with a side +`0 < L_t ≤ ⌈P a⌉`. For every nonnegative row of mass at most `M`, the conditional mean of the +dense atom given the usage channel is `k (G x y / f)`, once `K ≥ 2 (1 + 2 ^ H M / η)`. -/ +theorem expect_denseAtom_affineRetains [Fintype V] {ident : V → ZMod P} + (hident : Function.Injective ident) {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) {Lt : ℕ} + (hLt0 : 0 < Lt) (hLt : Lt ≤ ⌈P * a⌉₊) {k h ρ : ℝ → ℝ} {K : ℕ} {G : Matrix V V ℝ} {x y : V} + (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) (hG0 : ∀ w, 0 ≤ G x w) {M : ℝ} + (hGM : ∑ w, G x w ≤ M) (hK : 2 * (1 + 2 ^ H * M / η) ≤ K) : + 𝔼 s ∈ ({s | affineRetains P H Lt s (ident y)} : + Finset (Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P))), + Matrix.denseAtom (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) + (fun s v => affineRetains P H Lt s (ident v)) k h ρ K (a ^ H) G s x y = + k (G x y / a ^ H) := by + obtain ⟨hL, -, -, -, -⟩ := affineRetains_rates (H := H) hPa ha + have hLtP : Lt ≤ P := hLt.trans hL + have ha0 : 0 < a := by + by_contra h0 + have hP : (0 : ℝ) ≤ P := Nat.cast_nonneg _ + nlinarith [mul_nonpos_of_nonneg_of_nonpos hP (not_lt.mp h0)] + have hS : ({s | affineRetains P H Lt s (ident y)} : + Finset (Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P))).Nonempty := by + rw [← card_pos] + by_contra h0 + have h := dens_affineRetains (H := H) hLtP (ident y) + rw [dens_eq_card_div_card, Nat.eq_zero_of_not_pos h0, Nat.cast_zero, zero_div] at h + have : (0 : ℚ≥0) < ((Lt : ℚ≥0) / P) ^ H := by + have : (0 : ℚ≥0) < P := by exact_mod_cast (Fact.out : P.Prime).pos + positivity + exact absurd h this.ne + have hp : ∀ w, w ≠ y → (#{s | affineRetains P H Lt s (ident y) ∧ + affineRetains P H ⌈P * a⌉₊ s (ident w)} : ℝ) ≤ + 2 ^ H * a ^ H * #{s | affineRetains P H Lt s (ident y)} := fun w hwy => + card_affineRetains_and_affineRetains_le hident hPa ha hLtP hwy + exact Matrix.expect_denseAtom (Y := fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) + (Yt := fun s v => affineRetains P H Lt s (ident v)) (c := 2 ^ H) hS hkh hρ0 hρ1 hη hρη + (pow_pos ha0 H) hG0 hGM (by positivity) hK hp + +end Cslib.Probability diff --git a/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean b/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean index 7b243567c8..1efd0065f3 100644 --- a/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean +++ b/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean @@ -53,6 +53,8 @@ only for the later averaging walks, so they are not needed here. * `Cslib.Probability.card_retentionBox`: the box has `L ^ H` points. * `Cslib.Probability.dens_affineRetains`, `Cslib.Probability.dens_affineRetains_and`: exact retention probabilities of one identifier and of two distinct ones. +* `Cslib.Probability.affineRetains_of_le`, `Cslib.Probability.dens_affineRetains_and_affineRetains`: + nested boxes and the joint retention probability at two rates. * `Cslib.Probability.dens_two_mul_card_filter_affineRetains_lt_le`: the lower tail of the number of retained identifiers of a set. * `Cslib.Probability.dens_filter_fst_and_snd`: events about independent seeds are independent. @@ -150,6 +152,31 @@ theorem dens_affineRetains_and (hL : L ≤ P) {w y : ZMod P} (hwy : w ≠ y) : push_cast rfl +omit [Fact P.Prime] in +/-- **Nested boxes**: an identifier retained with side `L₂` is retained with every side +`L₁ ≥ L₂`, by the same seed. So a channel at a lower rate retains a subset. -/ +theorem affineRetains_of_le {L₁ L₂ : ℕ} (hL : L₂ ≤ L₁) {s} {y : ZMod P} + (h : affineRetains P H L₂ s y) : affineRetains P H L₁ s y := by + simp only [affineRetains, retentionBox, Fintype.mem_piFinset, mem_filter, mem_univ, + true_and] at h ⊢ + exact fun j => (h j).trans_le hL + +/-- **Pairwise independent retention at two rates**: for distinct identifiers `w ≠ y`, the seed +retains `w` with side `L₁` and `y` with side `L₂` with probability +`(L₁ / P) ^ H * (L₂ / P) ^ H`. -/ +theorem dens_affineRetains_and_affineRetains {L₁ L₂ : ℕ} (hL₁ : L₁ ≤ P) (hL₂ : L₂ ≤ P) + {w y : ZMod P} (hwy : w ≠ y) : + dens {s | affineRetains P H L₁ s w ∧ affineRetains P H L₂ s y} = + ((L₁ : ℚ≥0) / P) ^ H * ((L₂ : ℚ≥0) / P) ^ H := by + have h := isPairwiseIndependentHash_affineIdentifier.dens_filter_apply_mem_and_apply_mem hwy + (retentionBox P H L₁) (retentionBox P H L₂) + rw [card_retentionBox hL₁, card_retentionBox hL₂, Fintype.card_fun, Fintype.card_fin, + ZMod.card] at h + unfold affineRetains + rw [h, div_pow, div_pow] + push_cast + rfl + /-- **Lower tail of the retained count**: a set `A` of identifiers retains fewer than half of its expected number `#A π`, with `π = (L / P) ^ H`, with probability at most `4 / (#A π)`. -/ theorem dens_two_mul_card_filter_affineRetains_lt_le (hL : L ≤ P) (A : Finset (ZMod P)) diff --git a/ComplexityTests/AtomChannels.lean b/ComplexityTests/AtomChannels.lean new file mode 100644 index 0000000000..87a60bb427 --- /dev/null +++ b/ComplexityTests/AtomChannels.lean @@ -0,0 +1,66 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexity.Probability.PairwiseIndependentHash.AtomChannels +import Mathlib.Tactic.NormNum.Prime + +/-! +# Tests for dense atoms over affine channels at two rates + +* The joint retention probability at two rates over `𝔽₃`, exactly. +* Nested boxes. +* The dense atom identity at two rates for a concrete walk over `𝔽₅`. +-/ + +namespace ComplexityTests.AtomChannels + +open Finset Cslib.Probability +open scoped BigOperators + +instance : Fact (Nat.Prime 3) := ⟨by norm_num⟩ +instance : Fact (Nat.Prime 5) := ⟨by norm_num⟩ + +-- Over `𝔽₃` in one coordinate, `0` lands in the box of side `2` and `1` in the box of side `1` +-- with probability `2/3 · 1/3 = 2/9`. +example : dens {s | affineRetains 3 1 2 s 0 ∧ affineRetains 3 1 1 s 1} = 2 / 9 := by + rw [dens_affineRetains_and_affineRetains (by norm_num) (by norm_num) (by decide)] + norm_num + +-- A seed that retains `y` with side `1` retains it with side `2`. +example (s : Matrix (Fin 2) (Fin 1) (ZMod 5) × (Fin 2 → ZMod 5)) (y : ZMod 5) + (h : affineRetains 5 2 1 s y) : affineRetains 5 2 2 s y := + affineRetains_of_le (by norm_num) h + +/-- The `½`-walk `x → x + 1` on `ZMod 5`. -/ +private noncomputable def W : Matrix (ZMod 5) (ZMod 5) ℝ := + fun x w => if w = x + 1 then 1 / 2 else 0 + +/-- Main function zero through `1/2`. -/ +private noncomputable def k : ℝ → ℝ := fun d => if d ≤ 1 / 2 then 0 else d + +/-- Gate function: one below `1/1000`. -/ +private noncomputable def ρ : ℝ → ℝ := fun r => if r < 1 / 1000 then 1 else 0 + +private theorem row_mass (x : ZMod 5) : ∑ w, W x w ≤ 1 / 2 := by + simp [W, Finset.sum_ite_eq'] + +-- Rank channel of side `⌈5 · 1/2⌉ = 3` in `𝔽₅²` (rate `f = 1/4`), usage channel of side `1`: +-- the atom at `(0, 1)` has conditional mean `k (W 0 1 / f) = k 2 = 2`, for `K = 8002`. +example : 𝔼 s ∈ ({s | affineRetains 5 2 1 s (id 1)} : + Finset (Matrix (Fin 2) (Fin 1) (ZMod 5) × (Fin 2 → ZMod 5))), + Matrix.denseAtom (fun s v => affineRetains 5 2 ⌈(5 : ℕ) * (1 / 2 : ℝ)⌉₊ s (id v)) + (fun s v => affineRetains 5 2 1 s (id v)) k (fun _ => 1) ρ 8002 ((1 / 2 : ℝ) ^ 2) W s 0 1 = + 2 := by + have hceil : ⌈(5 : ℕ) * (1 / 2 : ℝ)⌉₊ = 3 := by + rw [Nat.ceil_eq_iff (by norm_num)]; norm_num + rw [expect_denseAtom_affineRetains (V := ZMod 5) (ident := id) Function.injective_id + (by norm_num) (by norm_num) (Lt := 1) (by norm_num) (by rw [hceil]; norm_num) + (fun _ _ => rfl) (fun r => by unfold ρ; split_ifs <;> norm_num) + (fun r => by unfold ρ; split_ifs <;> norm_num) (by norm_num : (0 : ℝ) < 1 / 2000) + (fun r hr => by unfold ρ; rw [ite_eq_left_iff]; exact fun h => absurd (by linarith) h) + (fun w => by unfold W; split_ifs <;> norm_num) (row_mass 0) (by norm_num)] + norm_num [k, W] + +end ComplexityTests.AtomChannels diff --git a/ComplexityTests/CorrectionAtom.lean b/ComplexityTests/CorrectionAtom.lean new file mode 100644 index 0000000000..4db52159a4 --- /dev/null +++ b/ComplexityTests/CorrectionAtom.lean @@ -0,0 +1,217 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexity.Foundations.Probability.CorrectionAtom +import Complexity.Probability.PairwiseIndependentHash.DetectorChannels +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Tests for the correction atoms + +* The normalization principle on a concrete gate. +* The incoming cap on a concrete column, and the column and row support bounds. +* The correction atom identity with every hypothesis discharged, for a concrete matrix and for every + matrix under the affine retention channels over `𝔽_P`. +* Rank stability on concrete values. +-/ + +namespace ComplexityTests.CorrectionAtom + +open Finset Matrix Cslib Cslib.Probability +open scoped BigOperators + +/-- Correction cutoff: zero through `1/4`. -/ +private noncomputable def Q : ℝ → ℝ := fun v => if v ≤ 1 / 4 then 0 else v + +/-- Row gate: one below `1/1000`. -/ +private noncomputable def ρ : ℝ → ℝ := fun r => if r < 1 / 1000 then 1 else 0 + +/-- Incoming gate: one below `1/4`. -/ +private noncomputable def τ : ℝ → ℝ := fun r => if r < 1 / 4 then 1 else 0 + +/-- Auxiliary score: one above entry `1/8`, ignoring the rank. -/ +private noncomputable def I : ℝ → ℝ → ℝ := fun v _ => if v ≤ 1 / 8 then 0 else 1 + +private theorem ρ_nonneg (r : ℝ) : 0 ≤ ρ r := by unfold ρ; split_ifs <;> norm_num +private theorem ρ_le_one (r : ℝ) : ρ r ≤ 1 := by unfold ρ; split_ifs <;> norm_num +private theorem τ_nonneg (r : ℝ) : 0 ≤ τ r := by unfold τ; split_ifs <;> norm_num +private theorem τ_le_one (r : ℝ) : τ r ≤ 1 := by unfold τ; split_ifs <;> norm_num + +private theorem ρ_eq_one (r : ℝ) (hr : r ≤ 1 / 2000) : ρ r = 1 := by + unfold ρ + split_ifs with h + · rfl + · exact absurd (by linarith) h + +private theorem τ_eq_one (r : ℝ) (hr : r ≤ 1 / 8) : τ r = 1 := by + unfold τ + split_ifs with h + · rfl + · exact absurd (by linarith) h + +private theorem τ_eq_zero (r : ℝ) (hr : 1 / 4 ≤ r) : τ r = 0 := by + unfold τ + split_ifs with h + · exact absurd hr (not_le.mpr h) + · rfl + +private theorem I_eq_zero (v r : ℝ) (hv : v ≤ 1 / 8) : I v r = 0 := by + simp only [I, ite_eq_left_iff] + exact fun h => absurd hv h + +private theorem Q_eq_zero (v : ℝ) (hv : v ≤ 1 / 4) : Q v = 0 := by + simp only [Q, ite_eq_left_iff] + exact fun h => absurd hv h + +private theorem I_eq_one (v r : ℝ) (hQ : Q v ≠ 0) (_ : ρ r ≠ 0) : I v r = 1 := by + unfold I + split_ifs with h + · exact absurd (Q_eq_zero v (by linarith)) hQ + · rfl + +/-! ### The normalization principle -/ + +-- A gate that is closed on one of three draws: dividing by its mean `2/3` removes the bias. +example (m : ℝ) : + 𝔼 s ∈ (univ : Finset (Fin 3)), m * ![1, 1, 0] s / max (1 / 2) (min 1 + (𝔼 s ∈ (univ : Finset (Fin 3)), (![1, 1, 0] : Fin 3 → ℝ) s)) = m := + expect_mul_div_clip_eq univ_nonempty (fun s _ => by fin_cases s <;> norm_num) + (fun s _ => by fin_cases s <;> norm_num) (by + have : (univ.filter fun s : Fin 3 => (![1, 1, 0] : Fin 3 → ℝ) s < 1) = {2} := by + ext s; fin_cases s <;> norm_num + rw [this]; norm_num) m + +/-! ### The incoming cap -/ + +/-- Every source has entry `1` in every column. -/ +private noncomputable def J : Matrix (Fin 3) (Fin 3) ℝ := fun _ _ => 1 + +-- All three retained sources score one at column `0`, so with `K_c = 2` the incoming gate is +-- closed. +example (T : Finset (Fin 3)) : incomingGate I τ 5 2 1 J univ T 0 = 0 := by + refine incomingGate_eq_zero (by norm_num) (by norm_num : (1 / 4 : ℝ) ≤ 1) τ_eq_zero ?_ + have : (univ.filter fun x : Fin 3 => (1 : ℝ) ≤ auxScore I 5 1 J T x 0) = univ := by + ext x + simp only [mem_filter, mem_univ, true_and, auxScore, J, div_one, I] + norm_num + rw [this] + decide + +-- Column and row support on every draw of any channels, with `K_c = 2` and `K = 3`. +example {ι κ : Type*} [Fintype ι] [Fintype κ] (X : ι → Fin 3 → Prop) (Y Yt : κ → Fin 3 → Prop) + [∀ s v, Decidable (X s v)] [∀ t v, Decidable (Y t v)] [∀ t v, Decidable (Yt t v)] + (G : Matrix (Fin 3) (Fin 3) ℝ) (g₀ : Fin 3 → ℝ) (d : ι × κ) (x y : Fin 3) : + #{x ∈ ({w | X d.1 w} : Finset (Fin 3)) | + correctionAtom I τ 3 2 1 G X Y Yt Q (fun _ => 1) ρ g₀ d x y ≠ 0} < 2 ∧ + #{y ∈ ({w | Y d.2 w} : Finset (Fin 3)) | + correctionAtom I τ 3 2 1 G X Y Yt Q (fun _ => 1) ρ g₀ d x y ≠ 0} < 3 := by + refine ⟨card_filter_correctionAtom_col_ne_zero_lt (by norm_num) I_eq_one + (by norm_num : (1 / 4 : ℝ) ≤ 1) τ_eq_zero d y, + card_filter_correctionAtom_row_ne_zero_lt (by norm_num) (by norm_num : (0 : ℝ) ≤ 1 / 4) + Q_eq_zero (by norm_num : (1 / 1000 : ℝ) ≤ 1 / 4) + (fun r hr => ?_) d x⟩ + unfold ρ + split_ifs with h + · exact absurd hr (not_le.mpr h) + · rfl + +/-! ### The identity with all hypotheses discharged -/ + +/-- The `½`-walk `0 → 1 → 2` on three vertices. -/ +private noncomputable def W : Matrix (Fin 3) (Fin 3) ℝ := !![0, 1 / 2, 0; 0, 0, 1 / 2; 0, 0, 0] + +private theorem filter_W : (univ.filter fun w : Fin 3 => (1 / 8 : ℝ) < W w 1 / 1) = {0} := by + ext w; fin_cases w <;> norm_num [W] + +-- With channels that retain everything, `K = 4004` and `K_c = 8`, the correction atom at +-- `(0, 1)` with multiplier `3` has conditional mean `Q (1/2) · 3 = 3/2`. +example : 𝔼 d ∈ (univ.filter fun _ : Unit => True) ×ˢ (univ.filter fun _ : Unit => True), + correctionAtom I τ 4004 8 1 W (fun _ _ => True) (fun _ _ => True) (fun _ _ => True) Q + (fun _ => 1) ρ (fun _ => 3) d 0 1 = 3 / 2 := by + have h := expect_correctionAtom (I := I) (τ := τ) (K := 4004) (Kc := 8) (f := 1) (G := W) + (X := fun (_ : Unit) (_ : Fin 3) => True) (Y := fun (_ : Unit) (_ : Fin 3) => True) + (Yt := fun _ _ => True) (Q := Q) (h := fun _ => 1) (ρ := ρ) (g₀ := fun _ => 3) (x := 0) + (y := 1) ⟨(), by simp⟩ ⟨(), by simp⟩ (fun _ _ => rfl) ρ_nonneg ρ_le_one + (by norm_num : (0 : ℝ) < 1 / 2000) ρ_eq_one τ_nonneg τ_le_one + (by norm_num : (0 : ℝ) ≤ 1 / 8) τ_eq_one I_eq_zero one_pos + (fun w => by fin_cases w <;> norm_num [W]) (M := 1 / 2) (by simp [W, Fin.sum_univ_three]) + (c := 1) zero_le_one (by norm_num) (fun w _ => by simp) (p := 1) zero_le_one + (fun w _ => by simp) (B := 1) (fun _ => by rw [filter_W]; norm_num) (by norm_num) + rw [h] + norm_num [Q, W] + +/-- The pair bound of a retention channel, as a count over the draws retaining `y`. -/ +private theorem card_pair_le {κ V : Type*} [Fintype κ] {Y : κ → V → Prop} + [∀ t v, Decidable (Y t v)] {q : ℝ} {w y : V} + (h : (dens {t | Y t w ∧ Y t y} : ℝ) ≤ q * dens {t | Y t y}) : + (#{t | Y t y ∧ Y t w} : ℝ) ≤ q * #{t | Y t y} := by + have hcard : ∀ T : Finset κ, ((dens T : ℚ≥0) : ℝ) = #T / Fintype.card κ := fun T => by + rw [dens_eq_card_div_card]; push_cast; rfl + rw [hcard, hcard, ← mul_div_assoc] at h + have hset : ({t | Y t y ∧ Y t w} : Finset κ) = ({t | Y t w ∧ Y t y} : Finset κ) := by + ext t; simp only [mem_filter, mem_univ, true_and]; tauto + rw [hset] + rcases (Fintype.card κ).eq_zero_or_pos with h0 | h0 + · have : (univ : Finset κ) = ∅ := univ_eq_empty_iff.mpr (Fintype.card_eq_zero_iff.mp h0) + simp [this] + · exact (div_le_div_iff_of_pos_right (by exact_mod_cast h0)).mp h + +/-- The identity for one retention channel `C` used on both sides, at rate `f`, for every +nonnegative `G` with row mass at most one and at most `R / f` sources above `f / 8` in column +`y`, once `K ≥ 4 (1 + C_pair · 2000)` and `K_c ≥ 4 (1 + C_pair R)`. -/ +private theorem expect_correctionAtom_channel {V κ : Type*} [Fintype V] [Fintype κ] + {C : κ → V → Prop} [∀ t v, Decidable (C t v)] {f π Cπ Cpair Cvar : ℝ} + (hch : RetentionChannels C C f π 1 Cπ Cpair Cvar) (hf : 0 < f) (hCpair : 0 ≤ Cpair) + (G : Matrix V V ℝ) {x y : V} (hG0 : ∀ w, 0 ≤ G x w) (hG1 : ∑ w, G x w ≤ 1) {R : ℝ} + (hD : (#({w | 1 / 8 < G w y / f} : Finset V) : ℝ) * f ≤ R) {K Kc : ℕ} + (hK : 4 * (1 + Cpair * 2000) ≤ (K : ℝ)) (hKc : 4 * (1 + Cpair * R) ≤ (Kc : ℝ)) + (g₀ : V → ℝ) : + 𝔼 d ∈ ({s | C s x} : Finset κ) ×ˢ ({t | C t y} : Finset κ), + correctionAtom I τ K Kc f G C C C Q (fun _ => 1) ρ g₀ d x y = Q (G x y / f) * g₀ y := by + have hπ := (mul_pos one_pos hf).trans_le hch.lower + have hne : ∀ v, ({s | C s v} : Finset κ).Nonempty := fun v => by + by_contra hv + rw [not_nonempty_iff_eq_empty] at hv + have h := hch.dens_Y v + rw [hv, dens_empty, NNRat.cast_zero] at h + linarith + refine expect_correctionAtom (hne x) (hne y) (fun _ _ => rfl) ρ_nonneg ρ_le_one + (by norm_num : (0 : ℝ) < 1 / 2000) ρ_eq_one τ_nonneg τ_le_one + (by norm_num : (0 : ℝ) ≤ 1 / 8) τ_eq_one I_eq_zero hf hG0 hG1 (c := Cpair) hCpair + (by rw [show Cpair * 1 / (1 / 2000) = Cpair * 2000 by field_simp]; exact hK) + (fun w hwy => card_pair_le (hch.pair w y hwy)) (p := Cpair * f) (by positivity) + (fun w hwx => card_pair_le (hch.pair w x hwx)) (B := Cpair * R) (fun _ => ?_) hKc + calc Cpair * f * (#({w | 1 / 8 < G w y / f} : Finset V) : ℝ) + = Cpair * ((#({w | 1 / 8 < G w y / f} : Finset V) : ℝ) * f) := by ring + _ ≤ Cpair * R := by gcongr + +-- Affine retention channels over `𝔽_P` for both the start and the terminal side, at rate +-- `f = a ^ H` (`C_pair = 2 ^ H`). +example {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) (ha0 : 0 < a) + (G : Matrix V V ℝ) {x y : V} (hG0 : ∀ w, 0 ≤ G x w) (hG1 : ∑ w, G x w ≤ 1) {R : ℝ} + (hD : (#({w | 1 / 8 < G w y / a ^ H} : Finset V) : ℝ) * a ^ H ≤ R) {K Kc : ℕ} + (hK : 4 * (1 + 2 ^ H * 2000) ≤ (K : ℝ)) (hKc : 4 * (1 + 2 ^ H * R) ≤ (Kc : ℝ)) + (g₀ : V → ℝ) : + 𝔼 d ∈ ({s | affineRetains P H ⌈P * a⌉₊ s (ident x)} : Finset _) ×ˢ + ({t | affineRetains P H ⌈P * a⌉₊ t (ident y)} : Finset _), + correctionAtom I τ K Kc (a ^ H) G (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) + (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) + (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) Q (fun _ => 1) ρ g₀ d x y = + Q (G x y / a ^ H) * g₀ y := + expect_correctionAtom_channel (retentionChannels_affineRetains hident hPa ha) (pow_pos ha0 H) + (by positivity) G hG0 hG1 hD hK hKc g₀ + +/-! ### Rank stability -/ + +-- Perturbing `3, 1, 2, 0` by at most `1/2` moves its second largest value `2` by at most `1/2`. +example : |kthLargest 2 univ (![3, 1, 2, 0] : Fin 4 → ℚ) - + kthLargest 2 univ (![5 / 2, 1, 5 / 2, 1 / 2] : Fin 4 → ℚ)| ≤ 1 / 2 := + abs_kthLargest_sub_kthLargest_le (by norm_num) (by norm_num) fun x _ => by + fin_cases x <;> norm_num + +end ComplexityTests.CorrectionAtom