From 3c349e9bfeb52471252a2ddc02fa386b3c399408 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 10:25:03 +0000 Subject: [PATCH 1/2] feat(Foundations): dense stochastic atoms and their identity First slice of #1721 (Phase 4 of #1444, idea 6 of #474), following the OpenAI preprint (2026-09-23), Sections 5.1-5.2: the normalized dense atom 1{Yt(y)} k(d) R / c(q) has conditional mean exactly k(d) (Lemma 5.1), is bounded by 2|k(d)|, and has fewer than K nonzero entries per row on every draw (Lemma 5.5). The bin weights telescope to a partition of unity (5.6), (5.7). The row-gate failure bound is extracted from le_columnDetector as card_filter_rowGate_lt_one_mul_le and reused by both. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../Probability/ColumnDetector.lean | 121 +++--- .../Probability/StochasticAtom.lean | 344 ++++++++++++++++++ ComplexityTests/StochasticAtom.lean | 185 ++++++++++ 4 files changed, 599 insertions(+), 52 deletions(-) create mode 100644 Complexity/Foundations/Probability/StochasticAtom.lean create mode 100644 ComplexityTests/StochasticAtom.lean diff --git a/Complexity.lean b/Complexity.lean index 3b94e48ab..e70abcd64 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2721,6 +2721,7 @@ public import Complexity.Foundations.Probability.Gaussian.Multivariate public import Complexity.Foundations.Probability.Gaussian.Real public import Complexity.Foundations.Probability.Gaussian.Sheppard public import Complexity.Foundations.Probability.SecondMoment +public import Complexity.Foundations.Probability.StochasticAtom public import Complexity.Foundations.Quantum.Measurement public import Complexity.Foundations.Relation.InductiveCounting public import Complexity.Foundations.Relation.RelatesWithinSteps diff --git a/Complexity/Foundations/Probability/ColumnDetector.lean b/Complexity/Foundations/Probability/ColumnDetector.lean index 5756f4530..190bbaef9 100644 --- a/Complexity/Foundations/Probability/ColumnDetector.lean +++ b/Complexity/Foundations/Probability/ColumnDetector.lean @@ -68,6 +68,7 @@ Markov's inequality for the gate failures with the lower tail of the start chann ## Main results * `Matrix.columnDetector_nonneg`, `Matrix.columnDetector_le_one`: detector numbers lie in `[0, 1]`. +* `Matrix.card_filter_rowGate_lt_one_mul_le`: a row gate fails on few terminal draws. * `Matrix.le_columnDetector`: columns with many large entries are detected. * `Matrix.lt_card_of_lt_columnDetector`: detected columns have many substantial entries. @@ -171,6 +172,66 @@ theorem columnDetector_le_one (hϕ0 : ∀ t, 0 ≤ ϕ t) (hϕ1 : ∀ t, ϕ t ≤ _ = Fintype.card ι * #({t | Y t y} : Finset κ) := by simp only [sum_const, card_univ, nsmul_eq_mul, mul_one] +omit [Fintype κ] in +/-- **Row gates rarely fail** [OpenAI2026LogSpace, proofs of Lemmas 4.3 (1) and 5.1]. Let row `x` +of `G ≥ 0` sum to at most `k`, and let `ρ` be one through `η > 0`. Let `T` be a finite set of +terminal draws on which every vertex `w ≠ y` is retained at most a `c f` fraction of the time. +Then the row gate of `x` is below one on at most a `(1 + c k / η) / K` fraction of `T`. + +The gate can fail only if `K` retained entries exceed `η f`. At most `k / (η f)` entries do, and +the retention counts of these entries over `T` sum to at most `#T (1 + c k / η)`, counting `y` +itself once; this is Markov's inequality. No independence between rows is used. -/ +theorem card_filter_rowGate_lt_one_mul_le (T : Finset κ) (x : V) (hf : 0 < f) {η : ℝ} + (hη : 0 < η) (hρη : ∀ t, t ≤ η → ρ t = 1) (hG0 : ∀ w, 0 ≤ G x w) {k : ℝ} + (hGk : ∑ w, G x w ≤ k) (hK : 0 < K) {c : ℝ} (hc : 0 ≤ c) + (hpair : ∀ w, w ≠ y → (#{t ∈ T | Y t w} : ℝ) ≤ c * f * #T) : + (#{t ∈ T | rowGate ρ K f G {w | Y t w} x < 1} : ℝ) * K ≤ #T * (1 + c * k / η) := by + classical + set W : Finset V := {w | η * f < G x w} + have hW : (#W : ℝ) * (η * f) ≤ k := + (card_filter_mul_le_sum univ _ (fun w => G x w) (fun w _ => hG0 w) + fun _ _ hw => hw.le).trans hGk + have hbadK : ∀ t ∈ T, rowGate ρ K f G {w | Y t w} x < 1 → (K : ℝ) ≤ #{w ∈ W | Y t w} := by + intro t _ ht + have hlt : η < kthLargest K {w | Y t w} (fun w => G x w / f) := by + by_contra hle + rw [rowGate, hρη _ (not_lt.mp hle)] at ht + exact lt_irrefl _ ht + have hcard := (lt_kthLargest_iff hK hη.le).mp hlt + have hsub : ({w ∈ ({w | Y t w} : Finset V) | η < G x w / f} : Finset V) ⊆ + {w ∈ W | Y t w} := fun w hw => by + simp only [mem_filter, mem_univ, true_and, W] at hw ⊢ + exact ⟨by rw [lt_div_iff₀ hf] at hw; exact hw.2, hw.1⟩ + exact_mod_cast hcard.trans (card_le_card hsub) + have hMarkov : (#{t ∈ T | rowGate ρ K f G {w | Y t w} x < 1} : ℝ) * K ≤ + ∑ t ∈ T, (#{w ∈ W | Y t w} : ℝ) := + card_filter_mul_le_sum T _ _ (fun _ _ => by positivity) hbadK + have hswap : ∑ t ∈ T, (#{w ∈ W | Y t w} : ℝ) = ∑ w ∈ W, (#{t ∈ T | Y t w} : ℝ) := by + simp only [natCast_card_filter] + exact sum_comm + have hterm : ∀ w ∈ W, (#{t ∈ T | Y t w} : ℝ) ≤ (if y = w then (#T : ℝ) else 0) + + c * f * #T := by + intro w _ + by_cases hwy : y = w + · have hle : (#{t ∈ T | Y t w} : ℝ) ≤ #T := by exact_mod_cast card_filter_le _ _ + have : 0 ≤ c * f * #T := by positivity + simp only [hwy, ↓reduceIte] + linarith + · simp only [hwy, ↓reduceIte, zero_add] + exact hpair w (Ne.symm hwy) + have hWf : (#W : ℝ) * f ≤ k / η := by + rw [le_div_iff₀ hη]; linarith + calc (#{t ∈ T | rowGate ρ K f G {w | Y t w} x < 1} : ℝ) * K + ≤ ∑ w ∈ W, ((if y = w then (#T : ℝ) else 0) + c * f * #T) := + hMarkov.trans (hswap ▸ sum_le_sum hterm) + _ = (if y ∈ W then (#T : ℝ) else 0) + #W * (c * f * #T) := by + rw [sum_add_distrib, sum_ite_eq, sum_const, nsmul_eq_mul] + _ ≤ #T + #T * c * (#W * f) := by + have : (if y ∈ W then (#T : ℝ) else 0) ≤ #T := by split_ifs <;> [exact le_rfl; positivity] + nlinarith + _ ≤ #T + #T * c * (k / η) := by gcongr + _ = #T * (1 + c * k / η) := by ring + variable {π cπ Cπ Cpair Cvar : ℝ} omit [Fintype V] in @@ -316,58 +377,14 @@ theorem le_columnDetector (hch : RetentionChannels X Y f π cπ Cπ Cpair Cvar) have : (0 : ℝ) < K := by linarith exact_mod_cast this -- Markov's inequality for the row gates: each row fails its gate on few terminal draws - have hgate : ∀ x, (#{t ∈ T | gate t x < 1} : ℝ) * K ≤ #T * D := by - intro x - set W : Finset V := {w | η * f < G x w} - have hW : (#W : ℝ) * (η * f) ≤ k := - (card_filter_mul_le_sum univ _ (fun w => G x w) (fun w _ => hG0 x w) - fun _ _ hw => hw.le).trans (hGk x) - have hbadK : ∀ t ∈ T, gate t x < 1 → (K : ℝ) ≤ #{w ∈ W | Y t w} := by - intro t _ ht - have hlt : η < kthLargest K {w | Y t w} (fun w => G x w / f) := by - by_contra hle - have h1 := hρη _ (not_lt.mp hle) - simp only [gate, rowGate] at ht - rw [h1] at ht - exact lt_irrefl _ ht - have hcard := (lt_kthLargest_iff hKpos hη.le).mp hlt - have hsub : ({w ∈ ({w | Y t w} : Finset V) | η < G x w / f} : Finset V) ⊆ - {w ∈ W | Y t w} := fun w hw => by - simp only [mem_filter, mem_univ, true_and, W] at hw ⊢ - exact ⟨by rw [lt_div_iff₀ hf] at hw; exact hw.2, hw.1⟩ - exact_mod_cast hcard.trans (card_le_card hsub) - have hMarkov : (#{t ∈ T | gate t x < 1} : ℝ) * K ≤ ∑ t ∈ T, (#{w ∈ W | Y t w} : ℝ) := - card_filter_mul_le_sum T _ _ (fun _ _ => by positivity) hbadK - have hswap : ∑ t ∈ T, (#{w ∈ W | Y t w} : ℝ) = ∑ w ∈ W, (#{t ∈ T | Y t w} : ℝ) := by - simp only [natCast_card_filter] - exact sum_comm - have hterm : ∀ w ∈ W, (#{t ∈ T | Y t w} : ℝ) ≤ (if y = w then (#T : ℝ) else 0) + - Cpair * f * #T := by - intro w _ - have hle : (#{t ∈ T | Y t w} : ℝ) ≤ #T := by exact_mod_cast card_filter_le _ _ - by_cases hwy : y = w - · simp only [hwy, ↓reduceIte] - have : 0 ≤ Cpair * f * #T := by positivity - linarith - · simp only [hwy, ↓reduceIte, zero_add] - have hp := hch.pair w y (Ne.symm hwy) - rw [dens_cast, dens_cast, ← mul_div_assoc, div_le_div_iff_of_pos_right hκr] at hp - have hset : ({t ∈ T | Y t w} : Finset κ) = ({t | Y t w ∧ Y t y} : Finset κ) := by - ext t; simp only [T, mem_filter, mem_univ, true_and]; tauto - rw [hset] - exact hp - have hWf : (#W : ℝ) * f ≤ k / η := by - rw [le_div_iff₀ hη]; linarith - calc (#{t ∈ T | gate t x < 1} : ℝ) * K - ≤ ∑ w ∈ W, ((if y = w then (#T : ℝ) else 0) + Cpair * f * #T) := - hMarkov.trans (hswap ▸ sum_le_sum hterm) - _ = (if y ∈ W then (#T : ℝ) else 0) + #W * (Cpair * f * #T) := by - rw [sum_add_distrib, sum_ite_eq, sum_const, nsmul_eq_mul] - _ ≤ #T + #T * Cpair * (#W * f) := by - have : (if y ∈ W then (#T : ℝ) else 0) ≤ #T := by split_ifs <;> [exact le_rfl; positivity] - nlinarith - _ ≤ #T + #T * Cpair * (k / η) := by gcongr - _ = #T * D := by simp only [D]; ring + have hgate : ∀ x, (#{t ∈ T | gate t x < 1} : ℝ) * K ≤ #T * D := fun x => + card_filter_rowGate_lt_one_mul_le T x hf hη hρη (hG0 x) (hGk x) hKpos hCpair fun w hwy => by + have hp := hch.pair w y hwy + rw [dens_cast, dens_cast, ← mul_div_assoc, div_le_div_iff_of_pos_right hκr] at hp + have hset : ({t ∈ T | Y t w} : Finset κ) = ({t | Y t w ∧ Y t y} : Finset κ) := by + ext t; simp only [T, mem_filter, mem_univ, true_and]; tauto + rw [hset] + exact hp -- the expected number of retained large rows that fail their gate set N : ι → ℝ := fun s => #{x ∈ A | X s x} set L : ι → κ → ℝ := fun s t => #{x ∈ A | X s x ∧ gate t x < 1} diff --git a/Complexity/Foundations/Probability/StochasticAtom.lean b/Complexity/Foundations/Probability/StochasticAtom.lean new file mode 100644 index 000000000..a7e39eae5 --- /dev/null +++ b/Complexity/Foundations/Probability/StochasticAtom.lean @@ -0,0 +1,344 @@ +/- +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.ColumnDetector +import Mathlib.Algebra.Order.BigOperators.Expect +import Mathlib.Algebra.BigOperators.Field +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# Stochastic atoms + +A *stochastic atom* represents a deterministic number, such as a matrix entry, as the conditional +mean of a bounded table over a random retained set. The table has few nonzero entries in each +row on every draw. This is idea 6 in issue #474: the dense atoms of the OpenAI preprint +[OpenAI2026LogSpace, Section 5.1–5.2]. + +**The dense atom.** Fix a row `x` of a nonnegative matrix `G`, a scale `a > 0`, and two retention +channels on one seed space `κ`: a *rank channel* `Y`, over whose retained set the row gate ranks +the row, and a *usage channel* `Yt`, which masks the table. In the preprint, `Y` and `Yt` retain at +rates `a` and `t ≤ a`. For a draw `s`, the row gate is `R = ρ (rank_K {G x w / a : Y s w})` +(`Matrix.rowGate`). The *preparatory value* is `h (G x y / a) · R` (`Matrix.atomPrep`), and its +conditional mean given `Yt(y)` is the *normalizer* `q_y` (`Matrix.atomNormalizer`). The atom is +`1{Yt s y} · k (G x y / a) · R / c(q_y)`, with the clipped denominator `c(q) = max (1/2) (min 1 q)` +(`Matrix.denseAtom`) [OpenAI2026LogSpace, (5.10), (5.11)]. + +**The identity** [OpenAI2026LogSpace, Lemma 5.1]. Suppose `h = 1` wherever `k ≠ 0`, the row has +mass at most `M`, `ρ ∈ [0, 1]` is one through `η > 0`, each vertex `w ≠ y` is retained by `Y` +on at most a `c a` fraction of the draws with `Yt(y)`, and `K ≥ 2 (1 + c M / η)`. Then the gate +is full on at least half of these draws (`Matrix.card_filter_rowGate_lt_one_mul_le`), so +`q_y ≥ 1/2`. The clipping does nothing, and the conditional mean of the atom is exactly +`k (G x y / a)` (`Matrix.expect_denseAtom`). The atom is bounded by `2 |k (G x y / a)|` +(`Matrix.abs_denseAtom_le`). The preprint takes `K` larger, so that the gate fails with +probability at most `1/8` and `q_y ≥ 7/8`; the identity only needs `q_y ≥ 1/2`. + +**Row support** [OpenAI2026LogSpace, Lemma 5.5, first part]. If `k` vanishes through `e ≥ 0`, `ρ` +vanishes from `g ≤ e` on, and `Yt ⊆ Y`, then on every draw the row has fewer than `K` nonzero +atom entries (`Matrix.card_filter_denseAtom_ne_zero_lt`). The same holds for the preparatory +values and any other `m (G x y / a) · R` (`Matrix.card_filter_mul_rowGate_ne_zero_lt`). This +holds for every real matrix, with no sign or accuracy hypothesis. + +**Bins** [OpenAI2026LogSpace, (5.6), (5.7)]. For a switch `χ`, zero through `1/2` and one from +`1`, and decreasing scales `b`, the weights `ω₀(w) = χ (w / b₀)` and +`ω_{k+1}(w) = χ (w / b_{k+1}) − χ (w / b_k)` (`Cslib.binWeight`) telescope +(`Cslib.sum_range_binWeight`). So `w = ∑_{k ≤ n} w ω_k(w)` once `w ≥ b_n` +(`Cslib.sum_range_mul_binWeight`). The weight `ω_{k+1}` is supported in `(b_{k+1}/2, b_k)` +(`Cslib.binWeight_succ_ne_zero`). A dense entry is split into these bins before the atoms are +formed. + +## Main definitions + +* `Matrix.atomPrep`, `Matrix.atomNormalizer`, `Matrix.denseAtom`: the dense atom. +* `Cslib.binWeight`: the bin weights. + +## Main results + +* `Matrix.expect_denseAtom`, `Matrix.expect_denseAtom_of_retentionChannels`: the dense atom + identity. +* `Matrix.abs_denseAtom_le`: the atom is bounded. +* `Matrix.card_filter_mul_rowGate_ne_zero_lt`, `Matrix.card_filter_denseAtom_ne_zero_lt`: row + support. +* `Cslib.sum_range_binWeight`, `Cslib.sum_range_mul_binWeight`, `Cslib.binWeight_nonneg`, + `Cslib.binWeight_succ_ne_zero`: the bins. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Sections 5.1–5.2 (preprint, not peer reviewed) +-/ + +public section + +open Finset +open scoped BigOperators + +namespace Matrix + +variable {V κ : Type*} [Fintype V] + +section Support + +variable {ρ m : ℝ → ℝ} {K : ℕ} {a : ℝ} {G : Matrix V V ℝ} + +omit [Fintype V] in +/-- **Row support** [OpenAI2026LogSpace, Lemma 5.5]: if `m` vanishes through `e ≥ 0` and the +gate function `ρ` vanishes from `g ≤ e` on, then fewer than `K > 0` retained entries `y ∈ T` have +`m (G x y / a) · rowGate x ≠ 0`. Indeed `K` such entries would all exceed `e`, so the `K`-th +largest value would exceed `g` and close the gate. -/ +theorem card_filter_mul_rowGate_ne_zero_lt (T : Finset V) (x : V) (hK : 0 < K) {e g : ℝ} + (he : 0 ≤ e) (hm : ∀ d, d ≤ e → m d = 0) (hg : g ≤ e) (hρ : ∀ r, g ≤ r → ρ r = 0) : + #{y ∈ T | m (G x y / a) * rowGate ρ K a G T x ≠ 0} < K := by + by_contra hle + rw [not_lt] at hle + have hsub : ({y ∈ T | m (G x y / a) * rowGate ρ K a G T x ≠ 0} : Finset V) ⊆ + {y ∈ T | e < G x y / a} := fun y hy => by + rw [mem_filter] at hy ⊢ + refine ⟨hy.1, not_le.mp fun h => hy.2 ?_⟩ + rw [hm _ h, zero_mul] + have hrank : e < kthLargest K T (fun w => G x w / a) := + (lt_kthLargest_iff hK he).mpr (hle.trans (card_le_card hsub)) + have hgate : rowGate ρ K a G T x = 0 := hρ _ (hg.trans hrank.le) + have hne : ({y ∈ T | m (G x y / a) * rowGate ρ K a G T x ≠ 0} : Finset V).Nonempty := + card_pos.mp (hK.trans_le hle) + obtain ⟨y, hy⟩ := hne + rw [mem_filter, hgate, mul_zero] at hy + exact hy.2 rfl + +end Support + +section DenseAtom + +variable [Fintype κ] (Y Yt : κ → V → Prop) [∀ s v, Decidable (Y s v)] + [∀ s v, Decidable (Yt s v)] (k h ρ : ℝ → ℝ) (K : ℕ) (a : ℝ) (G : Matrix V V ℝ) + +/-- The **preparatory value** `h (G x y / a) · rowGate x` of a dense atom, for the retained set +`T` of the rank channel [OpenAI2026LogSpace, (5.10)]. -/ +@[expose] noncomputable def atomPrep (T : Finset V) (x y : V) : ℝ := + h (G x y / a) * rowGate ρ K a G T x + +/-- The **normalizer** `q_y` of a dense atom: the conditional mean of the preparatory value given +that the usage channel retains `y` [OpenAI2026LogSpace, (5.10)]. -/ +@[expose] noncomputable def atomNormalizer (x y : V) : ℝ := + 𝔼 s ∈ ({s | Yt s y} : Finset κ), atomPrep h ρ K a G {w | Y s w} x y + +/-- The **dense atom** at `(x, y)` on the draw `s`: +`1{Yt s y} · k (G x y / a) · rowGate x / c(q_y)`, with `c(q) = max (1/2) (min 1 q)` +[OpenAI2026LogSpace, (5.11)]. -/ +@[expose] noncomputable def denseAtom (s : κ) (x y : V) : ℝ := + if Yt s y then + k (G x y / a) * rowGate ρ K a G {w | Y s w} x / + max (1 / 2) (min 1 (atomNormalizer Y Yt h ρ K a G x y)) + else 0 + +variable {Y Yt k h ρ K a G} + +omit [Fintype κ] in +/-- The clipped denominator is at least `1/2`. -/ +private theorem half_le_clip (q : ℝ) : (1 / 2 : ℝ) ≤ max (1 / 2) (min 1 q) := le_max_left _ _ + +/-- **The dense atom is bounded**: `|B(x, y)| ≤ 2 |k (G x y / a)|` on every draw, when +`ρ ∈ [0, 1]` [OpenAI2026LogSpace, Lemma 5.1]. -/ +theorem abs_denseAtom_le (hρ0 : ∀ r, 0 ≤ ρ r) (hρ1 : ∀ r, ρ r ≤ 1) (s : κ) (x y : V) : + |denseAtom Y Yt k h ρ K a G s x y| ≤ 2 * |k (G x y / a)| := by + rw [denseAtom] + split_ifs + · have hR0 : 0 ≤ rowGate ρ K a G {w | Y s w} x := hρ0 _ + have hR1 : rowGate ρ K a G {w | Y s w} x ≤ 1 := hρ1 _ + have hc := half_le_clip (atomNormalizer Y Yt h ρ K a G x y) + have hc0 : 0 < max (1 / 2) (min 1 (atomNormalizer Y Yt h ρ K a G x y)) := + lt_of_lt_of_le (by norm_num) hc + rw [abs_div, abs_mul, abs_of_nonneg hR0, abs_of_pos hc0, div_le_iff₀ hc0] + calc |k (G x y / a)| * rowGate ρ K a G {w | Y s w} x ≤ |k (G x y / a)| * 1 := + mul_le_mul_of_nonneg_left hR1 (abs_nonneg _) + _ = 2 * |k (G x y / a)| * (1 / 2) := by ring + _ ≤ _ := mul_le_mul_of_nonneg_left hc (by positivity) + · simp + +/-- **Row support of the dense atom** [OpenAI2026LogSpace, Lemmas 5.1 and 5.5]: if `k` vanishes +through `e ≥ 0`, `ρ` vanishes from `g ≤ e` on, and the usage channel retains only vertices that +the rank channel retains, then on every draw fewer than `K > 0` atoms of a row are nonzero. -/ +theorem card_filter_denseAtom_ne_zero_lt (hYt : ∀ s v, Yt s v → Y s v) (hK : 0 < K) {e g : ℝ} + (he : 0 ≤ e) (hk : ∀ d, d ≤ e → k d = 0) (hg : g ≤ e) (hρ : ∀ r, g ≤ r → ρ r = 0) (s : κ) + (x : V) : #{y | denseAtom Y Yt k h ρ K a G s 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 := a) (G := G) {w | Y s w} x hK he hk hg hρ) + rw [mem_filter] at hy ⊢ + rw [denseAtom] at hy + split_ifs at hy with hy' + · refine ⟨by simpa using hYt s y hy', fun h0 => hy.2 ?_⟩ + rw [h0, zero_div] + · exact absurd rfl hy.2 + +/-- **The dense atom identity** [OpenAI2026LogSpace, Lemma 5.1]. Let `h = 1` wherever `k ≠ 0`, +let row `x` of `G ≥ 0` have mass at most `M`, let `ρ ∈ [0, 1]` be one through `η > 0`, and let +`K ≥ 2 (1 + c M / η)`. Suppose the usage channel retains `y` on some draw, and every vertex +`w ≠ y` is retained by the rank channel on at most a `c a` fraction of those draws. Then the +conditional mean of the dense atom given `Yt(y)` is exactly `k (G x y / a)`. -/ +theorem expect_denseAtom {x y : V} (hS : ({s | Yt s y} : Finset κ).Nonempty) + (hkh : ∀ d, k d ≠ 0 → h d = 1) (hρ0 : ∀ r, 0 ≤ ρ r) (hρ1 : ∀ r, ρ r ≤ 1) {η : ℝ} + (hη : 0 < η) (hρη : ∀ r, r ≤ η → ρ r = 1) (ha : 0 < a) (hG0 : ∀ w, 0 ≤ G x w) {M : ℝ} + (hGM : ∑ w, G x w ≤ M) {c : ℝ} (hc : 0 ≤ c) (hK : 2 * (1 + c * M / η) ≤ K) + (hpair : ∀ w, w ≠ y → (#{s | Yt s y ∧ Y s w} : ℝ) ≤ c * a * #{s | Yt s y}) : + 𝔼 s ∈ ({s | Yt s y} : Finset κ), denseAtom Y Yt k h ρ K a G s x y = k (G x y / a) := by + set S : Finset κ := {s | Yt s y} + set R : κ → ℝ := fun s => rowGate ρ K a G {w | Y s w} x + by_cases hk0 : k (G x y / a) = 0 + · rw [hk0] + refine expect_eq_zero fun s _ => ?_ + rw [denseAtom, hk0] + split_ifs <;> simp + have hh1 : h (G x y / a) = 1 := hkh _ hk0 + have hSr : (0 : ℝ) < #S := by exact_mod_cast hS.card_pos + have hKr : (0 : ℝ) < K := by + have : 0 ≤ c * M / η := by + have hM : 0 ≤ M := (sum_nonneg fun w _ => hG0 w).trans hGM + positivity + linarith + have hKpos : 0 < K := by exact_mod_cast hKr + -- the gate fails on at most half of the conditioning draws + have hfail : (#{s ∈ S | R s < 1} : ℝ) * K ≤ #S * (1 + c * M / η) := + card_filter_rowGate_lt_one_mul_le S x ha hη hρη hG0 hGM hKpos hc fun w hwy => by + have hset : ({s ∈ S | Y s w} : Finset κ) = ({s | Yt s y ∧ Y s w} : Finset κ) := by + ext s; simp only [S, mem_filter, mem_univ, true_and] + rw [hset] + exact hpair w hwy + have hhalf : (#{s ∈ S | R s < 1} : ℝ) ≤ #S / 2 := by + rw [le_div_iff₀ (by norm_num : (0 : ℝ) < 2)] + nlinarith + -- so the normalizer, the mean gate, lies in `[1/2, 1]` + have hq : atomNormalizer Y Yt h ρ K a G x y = 𝔼 s ∈ S, R s := by + simp only [atomNormalizer, atomPrep, hh1, one_mul, S, R] + have hR1 : ∀ s, 1 - (if R s < 1 then 1 else 0) ≤ R s := fun s => by + split_ifs with h + · simp only [sub_self]; exact hρ0 _ + · simpa using not_lt.mp h + have hq_lo : 1 / 2 ≤ 𝔼 s ∈ S, R s := by + rw [expect_eq_sum_div_card, le_div_iff₀ hSr] + calc 1 / 2 * (#S : ℝ) ≤ #S - #{s ∈ S | R s < 1} := by linarith + _ = ∑ s ∈ S, (1 - (if R s < 1 then 1 else 0)) := by + rw [sum_sub_distrib, sum_boole, sum_const, nsmul_eq_mul, mul_one] + _ ≤ ∑ s ∈ S, R s := sum_le_sum fun s _ => hR1 s + have hq_hi : 𝔼 s ∈ S, R s ≤ 1 := expect_le hS fun s _ => hρ1 _ + have hclip : max (1 / 2) (min 1 (atomNormalizer Y Yt h ρ K a G x y)) = 𝔼 s ∈ S, R s := by + rw [hq, min_eq_right hq_hi, max_eq_right hq_lo] + have hpos : 0 < 𝔼 s ∈ S, R s := lt_of_lt_of_le (by norm_num) hq_lo + -- the atom is `k · R / q` on the conditioning draws + have hterm : ∀ s ∈ S, denseAtom Y Yt k h ρ K a G s x y = + (k (G x y / a) / 𝔼 s ∈ S, R s) * R s := fun s hs => by + have hs' : Yt s y := by simpa [S] using hs + simp only [denseAtom, hs', ↓reduceIte, hclip, R] + ring + rw [expect_congr rfl hterm, ← mul_expect, div_mul_cancel₀ _ hpos.ne'] + +/-- **The dense atom identity for retention channels** [OpenAI2026LogSpace, Lemma 5.1], when the +usage channel is the rank channel `Y` at the atom's scale `f`, as for corrections and detector +scores. With `RetentionChannels` at rate `f > 0` and `c_π > 0`, the pair bound supplies the +retention hypothesis with `c = C_pair`. -/ +theorem expect_denseAtom_of_retentionChannels {ι : Type*} [Fintype ι] {X : ι → V → Prop} + [∀ s v, Decidable (X s v)] {π cπ Cπ Cpair Cvar : ℝ} + (hch : Cslib.Probability.RetentionChannels X Y a π cπ Cπ Cpair Cvar) (ha : 0 < a) + (hcπ : 0 < cπ) (hCpair : 0 ≤ Cpair) {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 + Cpair * M / η) ≤ K) : + 𝔼 s ∈ ({s | Y s y} : Finset κ), denseAtom Y Y k h ρ K a G s x y = k (G x y / a) := by + have hcard : ∀ T : Finset κ, ((dens T : ℚ≥0) : ℝ) = #T / Fintype.card κ := fun T => by + rw [dens_eq_card_div_card]; push_cast; rfl + have hπ : 0 < π := (mul_pos hcπ ha).trans_le hch.lower + have hκ : (0 : ℝ) < Fintype.card κ := by + have h := hch.dens_Y y + rw [hcard] at h + rcases (Fintype.card κ).eq_zero_or_pos with h0 | h0 + · rw [h0, Nat.cast_zero, div_zero] at h; linarith + · exact_mod_cast h0 + have hS : ({s | Y s y} : Finset κ).Nonempty := by + rw [← card_pos] + by_contra h0 + have h := hch.dens_Y y + rw [hcard, Nat.eq_zero_of_not_pos h0, Nat.cast_zero, zero_div] at h + linarith + refine expect_denseAtom hS hkh hρ0 hρ1 hη hρη ha hG0 hGM hCpair hK fun w hwy => ?_ + have hp := hch.pair w y hwy + rw [hcard, hcard, ← mul_div_assoc, div_le_div_iff_of_pos_right hκ] at hp + have hset : ({s | Y s y ∧ Y s w} : Finset κ) = ({s | Y s w ∧ Y s y} : Finset κ) := by + ext s; simp only [mem_filter, mem_univ, true_and]; tauto + rw [hset] + exact hp + +end DenseAtom + +end Matrix + +namespace Cslib + +/-- The **bin weights** for the scales `b`: `ω₀(w) = χ (w / b₀)` and +`ω_{k+1}(w) = χ (w / b_{k+1}) − χ (w / b_k)` [OpenAI2026LogSpace, (5.6)]. -/ +@[expose] noncomputable def binWeight (χ : ℝ → ℝ) (b : ℕ → ℝ) : ℕ → ℝ → ℝ + | 0, w => χ (w / b 0) + | k + 1, w => χ (w / b (k + 1)) - χ (w / b k) + +variable {χ : ℝ → ℝ} {b : ℕ → ℝ} + +/-- **The bin weights telescope**: `∑_{k ≤ n} ω_k(w) = χ (w / b_n)`. -/ +theorem sum_range_binWeight (n : ℕ) (w : ℝ) : + ∑ k ∈ range (n + 1), binWeight χ b k w = χ (w / b n) := by + induction n with + | zero => simp [binWeight] + | succ n ih => rw [sum_range_succ, ih, binWeight]; ring + +/-- **Bin decomposition** [OpenAI2026LogSpace, (5.7)]: if `χ` is one from `1` on and +`0 < b_n ≤ w`, then `w = ∑_{k ≤ n} w ω_k(w)`. -/ +theorem sum_range_mul_binWeight (hχ1 : ∀ t, 1 ≤ t → χ t = 1) {n : ℕ} (hb : 0 < b n) {w : ℝ} + (hw : b n ≤ w) : ∑ k ∈ range (n + 1), w * binWeight χ b k w = w := by + rw [← mul_sum, sum_range_binWeight, hχ1 _ ((one_le_div₀ hb).mpr hw), mul_one] + +/-- For `0 ≤ w`, the ratio `w / b` grows as the positive scale `b` shrinks. -/ +private theorem div_le_div_scale {w : ℝ} (hw : 0 ≤ w) {k : ℕ} (hb : ∀ k, 0 < b k) + (hanti : Antitone b) : w / b k ≤ w / b (k + 1) := + div_le_div_of_nonneg_left hw (hb _) (hanti (Nat.le_succ k)) + +/-- **The bin weights are nonnegative** for a monotone switch that vanishes at `0`, decreasing +positive scales and `0 ≤ w`. -/ +theorem binWeight_nonneg (hχ : Monotone χ) (hχ0 : χ 0 = 0) (hb : ∀ k, 0 < b k) + (hanti : Antitone b) {w : ℝ} (hw : 0 ≤ w) (k : ℕ) : 0 ≤ binWeight χ b k w := by + cases k with + | zero => + rw [binWeight, ← hχ0] + exact hχ (div_nonneg hw (hb 0).le) + | succ k => + rw [binWeight, sub_nonneg] + exact hχ (div_le_div_scale hw hb hanti) + +/-- **Bin support** [OpenAI2026LogSpace, (5.8)]: if `χ` is zero through `1/2` and one from `1` +on, then `ω_{k+1}(w) ≠ 0` forces `b_{k+1} / 2 < w < b_k`, for decreasing positive scales. -/ +theorem binWeight_succ_ne_zero (hχ0 : ∀ t, t ≤ 1 / 2 → χ t = 0) (hχ1 : ∀ t, 1 ≤ t → χ t = 1) + (hb : ∀ k, 0 < b k) (hanti : Antitone b) {k : ℕ} {w : ℝ} + (hω : binWeight χ b (k + 1) w ≠ 0) : b (k + 1) / 2 < w ∧ w < b k := by + rw [binWeight] at hω + rcases lt_or_ge w 0 with hw | hw + · exfalso + have h1 : w / b (k + 1) ≤ 1 / 2 := (div_neg_of_neg_of_pos hw (hb _)).le.trans (by norm_num) + have h2 : w / b k ≤ 1 / 2 := (div_neg_of_neg_of_pos hw (hb _)).le.trans (by norm_num) + rw [hχ0 _ h1, hχ0 _ h2, sub_zero] at hω + exact hω rfl + have hmono := div_le_div_scale hw hb hanti (k := k) + constructor + · by_contra h + have h1 : w / b (k + 1) ≤ 1 / 2 := by + rw [div_le_iff₀ (hb _)]; linarith + rw [hχ0 _ h1, hχ0 _ (hmono.trans h1), sub_zero] at hω + exact hω rfl + · by_contra h + have h1 : 1 ≤ w / b k := (one_le_div₀ (hb _)).mpr (not_lt.mp h) + rw [hχ1 _ h1, hχ1 _ (h1.trans hmono), sub_self] at hω + exact hω rfl + +end Cslib diff --git a/ComplexityTests/StochasticAtom.lean b/ComplexityTests/StochasticAtom.lean new file mode 100644 index 000000000..31b03f960 --- /dev/null +++ b/ComplexityTests/StochasticAtom.lean @@ -0,0 +1,185 @@ +/- +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.StochasticAtom +import Complexity.Probability.PairwiseIndependentHash.DetectorChannels +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Tests for the stochastic atoms + +* A computed two-draw atom: the row gate fails on half of the draws, the normalizer is `1/2`, and + the normalized atom still has the exact entry as its mean. +* The dense atom identity, with every hypothesis discharged, for a concrete matrix and for every + matrix under the affine retention channels over `𝔽_P`. +* Row support on every draw, and concrete bin weights. +-/ + +namespace ComplexityTests.StochasticAtom + +open Finset Matrix Cslib Cslib.Probability +open scoped BigOperators + +/-- Main function of the dense bins: zero through `1/2`. -/ +private noncomputable def k : ℝ → ℝ := fun d => if d ≤ 1 / 2 then 0 else d + +/-- Gate function: one below `1/1000`, zero from `1/1000` on. -/ +private noncomputable def ρ : ℝ → ℝ := fun r => if r < 1 / 1000 then 1 else 0 + +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_zero (r : ℝ) (hr : 1 / 1000 ≤ r) : ρ r = 0 := by + unfold ρ + split_ifs with h + · exact absurd hr (not_le.mpr h) + · rfl + +private theorem k_eq_zero (d : ℝ) (hd : d ≤ 1 / 2) : k d = 0 := by + simp only [k, ite_eq_left_iff] + exact fun h => absurd hd h + +/-! ### A computed atom: normalization compensates a failing gate -/ + +/-- Draw `false` retains `{1}`, draw `true` retains `{1, 2}`. -/ +private abbrev Y : Bool → Fin 3 → Prop := fun s v => v = 1 ∨ (s = true ∧ v = 2) + +/-- Row `0` has the two entries `G 0 1 = G 0 2 = 1`. -/ +private noncomputable def G : Matrix (Fin 3) (Fin 3) ℝ := !![0, 1, 1; 0, 0, 0; 0, 0, 0] + +private theorem retained_false : ({w | Y false w} : Finset (Fin 3)) = {1} := by decide + +private theorem retained_true : ({w | Y true w} : Finset (Fin 3)) = {1, 2} := by decide + +/-- On draw `false` only one entry is retained, so the second largest is the padding `0` and the +gate is open. -/ +private theorem rowGate_false : rowGate ρ 2 1 G {w | Y false w} 0 = 1 := by + have h : kthLargest 2 ({w | Y false w} : Finset (Fin 3)) (fun w => G 0 w / 1) = 0 := by + refine le_antisymm (not_lt.mp fun hlt => ?_) kthLargest_nonneg + have := (lt_kthLargest_iff (by norm_num) le_rfl).mp hlt + rw [retained_false] at this + exact absurd (this.trans (card_filter_le _ _)) (by simp) + rw [rowGate, h] + exact ρ_eq_one 0 (by norm_num) + +/-- On draw `true` two entries `1` are retained, so the second largest is `1` and the gate is +closed. -/ +private theorem rowGate_true : rowGate ρ 2 1 G {w | Y true w} 0 = 0 := by + have h : 1 ≤ kthLargest 2 ({w | Y true w} : Finset (Fin 3)) (fun w => G 0 w / 1) := by + rw [le_kthLargest_iff (by norm_num) (by norm_num), retained_true] + have : ({x ∈ ({1, 2} : Finset (Fin 3)) | (1 : ℝ) ≤ G 0 x / 1}) = {1, 2} := by + ext x; fin_cases x <;> simp [G] + rw [this]; rfl + rw [rowGate] + exact ρ_eq_zero _ (by linarith) + +private theorem draws_one : ({s | Y s 1} : Finset Bool) = univ := by decide + +/-- The normalizer is `1/2`: the gate is open on one of the two draws. -/ +private theorem atomNormalizer_eq : + atomNormalizer Y Y (fun _ => 1) ρ 2 1 G 0 1 = 1 / 2 := by + rw [atomNormalizer, draws_one] + simp only [atomPrep, one_mul, Fintype.expect_bool, rowGate_true, rowGate_false] + norm_num + +-- The atom doubles the entry on the open draw, vanishes on the closed one, and has mean +-- exactly `k (G 0 1) = 1`, although the gate fails half of the time. (Here `K = 2` is far below +-- the sufficient condition of `expect_denseAtom`; the normalizer still is at least `1/2`.) +example : denseAtom Y Y k (fun _ => 1) ρ 2 1 G false 0 1 = 2 ∧ + denseAtom Y Y k (fun _ => 1) ρ 2 1 G true 0 1 = 0 ∧ + 𝔼 s ∈ ({s | Y s 1} : Finset Bool), denseAtom Y Y k (fun _ => 1) ρ 2 1 G s 0 1 = k (G 0 1 / 1) + := by + have hY : ∀ s, Y s 1 := fun s => Or.inl rfl + have hk : k (G 0 1 / 1) = 1 := by norm_num [k, G] + have hfalse : denseAtom Y Y k (fun _ => 1) ρ 2 1 G false 0 1 = 2 := by + simp only [denseAtom, hY false, ↓reduceIte, atomNormalizer_eq, rowGate_false, hk] + norm_num + have htrue : denseAtom Y Y k (fun _ => 1) ρ 2 1 G true 0 1 = 0 := by + simp only [denseAtom, hY true, ↓reduceIte, rowGate_true] + simp + refine ⟨hfalse, htrue, ?_⟩ + rw [draws_one, Fintype.expect_bool, hfalse, htrue, hk] + norm_num + +-- Row support: on every draw, row `0` has fewer than `K = 2` nonzero atoms. +example (s : Bool) : #{y | denseAtom Y Y k (fun _ => 1) ρ 2 1 G s 0 y ≠ 0} < 2 := + card_filter_denseAtom_ne_zero_lt (fun _ _ h => h) (by norm_num) (by norm_num : (0 : ℝ) ≤ 1 / 2) + k_eq_zero (by norm_num : (1 / 1000 : ℝ) ≤ 1 / 2) ρ_eq_zero s 0 + +/-! ### 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] + +-- With a channel that retains everything (one seed), `K = 2002` satisfies +-- `K ≥ 2 (1 + c M / η)` for `c = 1`, `M = 1/2`, `η = 1/2000`. The main function `d ↦ d` and the +-- conditional mean recovers the entry `1/2`. +example : 𝔼 s ∈ (univ.filter fun _ => True : Finset Unit), + denseAtom (fun _ (_ : Fin 3) => True) (fun _ _ => True) (fun d => d) (fun _ => 1) ρ 2002 1 W + s 0 1 = 1 / 2 := by + have h := expect_denseAtom (Y := fun _ (_ : Fin 3) => True) (Yt := fun _ _ => True) + (k := fun d => d) (h := fun _ => 1) (K := 2002) (G := W) (x := 0) (y := 1) + ⟨(), by simp⟩ (fun _ _ => rfl) ρ_nonneg ρ_le_one (by norm_num : (0 : ℝ) < 1 / 2000) ρ_eq_one + 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) + rw [h] + norm_num [W] + +-- For every injective identification with `𝔽_P` and every rate `f = a ^ H` with `1 ≤ P a ≤ P`, +-- the affine retention channels give the identity for any nonnegative matrix with row mass at +-- most one, once `K ≥ 2 (1 + 2 ^ H · 2000)`. +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 : V} (hG0 : ∀ w, 0 ≤ G x w) (hG1 : ∑ w, G x w ≤ 1) {K : ℕ} + (hK : 2 * (1 + 2 ^ H * 2000) ≤ (K : ℝ)) (y : V) : + 𝔼 s ∈ ({s | affineRetains P H ⌈P * a⌉₊ s (ident y)} : Finset _), + denseAtom (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) + (fun s v => affineRetains P H ⌈P * a⌉₊ s (ident v)) k (fun _ => 1) ρ K (a ^ H) G s x y = + k (G x y / a ^ H) := + expect_denseAtom_of_retentionChannels (retentionChannels_affineRetains hident hPa ha) + (pow_pos ha0 H) one_pos (by positivity) (fun _ _ => rfl) ρ_nonneg ρ_le_one + (by norm_num : (0 : ℝ) < 1 / 2000) ρ_eq_one hG0 hG1 (by + have : (2 : ℝ) ^ H * 1 / (1 / 2000) = 2 ^ H * 2000 := by field_simp + rw [this]; exact hK) + +/-! ### Bins -/ + +/-- A switch: zero through `1/2`, one from `1`, linear in between. -/ +private noncomputable def χ : ℝ → ℝ := fun t => max 0 (min 1 (2 * t - 1)) + +/-- Dyadic scales `b_k = 2^{-k}`. -/ +private noncomputable def b : ℕ → ℝ := fun k => (1 / 2) ^ k + +-- At `w = 3/8`, with scales `1, 1/2, 1/4`: `ω₀ = 0`, `ω₁ = 1/2`, `ω₂ = 1/2`. +example : binWeight χ b 0 (3 / 8) = 0 ∧ binWeight χ b 1 (3 / 8) = 1 / 2 ∧ + binWeight χ b 2 (3 / 8) = 1 / 2 := by + refine ⟨?_, ?_, ?_⟩ <;> norm_num [binWeight, χ, b] + +-- The weights reproduce `w = 3/8` from scale `b₂ = 1/4` on. +example : ∑ k ∈ range 3, (3 / 8 : ℝ) * binWeight χ b k (3 / 8) = 3 / 8 := + sum_range_mul_binWeight (n := 2) (fun t ht => by simp only [χ]; rw [min_eq_left (by linarith), + max_eq_right zero_le_one]) (by norm_num [b]) (by norm_num [b]) + +-- `ω₂(w) ≠ 0` locates `w` in `(b₂ / 2, b₁) = (1/8, 1/2)`. +example {w : ℝ} (hω : binWeight χ b 2 w ≠ 0) : 1 / 8 < w ∧ w < 1 / 2 := by + have h := binWeight_succ_ne_zero (k := 1) (fun t ht => by + simp only [χ]; rw [max_eq_left (by have := min_le_right 1 (2 * t - 1); linarith)]) + (fun t ht => by simp only [χ]; rw [min_eq_left (by linarith), max_eq_right zero_le_one]) + (fun k => by positivity) (fun i j hij => pow_le_pow_of_le_one (by norm_num) (by norm_num) hij) + hω + norm_num [b] at h + exact h + +end ComplexityTests.StochasticAtom From 571d5b1e9bb2c2731980eb1e7d133665fd806e42 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 10:40:55 +0000 Subject: [PATCH 2/2] feat(Foundations): correction atoms with an incoming gate and the incoming cap Second slice of #1721 (Phase 4 of #1444, idea 6 of #474), following the OpenAI preprint (2026-09-23), Sections 5.1, 5.3 and 5.5: the correction atom 1{Yt(y)} Q(d) R T_y / c(q_y) g0(y) has conditional mean exactly Q(d) g0(y), including zero multipliers (Lemma 5.3); it is bounded, has fewer than K nonzero entries per row and fewer than K_c per column on every draw (the incoming cap, (5.18) and Lemma 5.6). Adds the normalization principle, a Markov bound for retained members of a sparse set, rank stability (5.4), nested affine boxes and the joint retention probability at two rates, and the dense atom identity for affine channels at two rates. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 2 + .../Foundations/Data/Finset/KthLargest.lean | 36 ++ .../Probability/CorrectionAtom.lean | 415 ++++++++++++++++++ .../PairwiseIndependentHash/AtomChannels.lean | 117 +++++ .../RetentionChannel.lean | 27 ++ ComplexityTests/AtomChannels.lean | 66 +++ ComplexityTests/CorrectionAtom.lean | 217 +++++++++ 7 files changed, 880 insertions(+) create mode 100644 Complexity/Foundations/Probability/CorrectionAtom.lean create mode 100644 Complexity/Probability/PairwiseIndependentHash/AtomChannels.lean create mode 100644 ComplexityTests/AtomChannels.lean create mode 100644 ComplexityTests/CorrectionAtom.lean diff --git a/Complexity.lean b/Complexity.lean index e70abcd64..1399373c4 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2716,6 +2716,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.DetectedStage public import Complexity.Foundations.Probability.Gaussian.Multivariate public import Complexity.Foundations.Probability.Gaussian.Real @@ -2985,6 +2986,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.Retention public import Complexity.Probability.PairwiseIndependentHash.RetentionChannel diff --git a/Complexity/Foundations/Data/Finset/KthLargest.lean b/Complexity/Foundations/Data/Finset/KthLargest.lean index b1198aef3..33b6107d3 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 000000000..80776f529 --- /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 000000000..f62d31ce6 --- /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 7b243567c..1efd0065f 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 000000000..87a60bb42 --- /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 000000000..4db52159a --- /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