From 3c349e9bfeb52471252a2ddc02fa386b3c399408 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 10:25:03 +0000 Subject: [PATCH] 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