diff --git a/Complexity.lean b/Complexity.lean index 4a3ea89215..5562155c9a 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -3053,7 +3053,9 @@ 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.ConditionalAveraging public import Complexity.Probability.PairwiseIndependentHash.DetectorChannels +public import Complexity.Probability.PairwiseIndependentHash.FrameChannel public import Complexity.Probability.PairwiseIndependentHash.HeavyCount public import Complexity.Probability.PairwiseIndependentHash.HierarchyChannels public import Complexity.Probability.PairwiseIndependentHash.Retention diff --git a/Complexity/Foundations/Combinatorics/Expander/Mixing.lean b/Complexity/Foundations/Combinatorics/Expander/Mixing.lean index 6d46c3c8a5..1addd0108d 100644 --- a/Complexity/Foundations/Combinatorics/Expander/Mixing.lean +++ b/Complexity/Foundations/Combinatorics/Expander/Mixing.lean @@ -48,6 +48,8 @@ says that spectral expanders are edge expanders [Arora and Barak, Section 21.2][ expectations plus the correlation of the centered functions. * `Cslib.RotationMap.sq_expect_mul_walk_pow_sub_le`: the mixing lemma for functions and walks of any length. +* `Cslib.RotationMap.expect_walk_pow_sub_expect_sq_le`: walks of length `t` contract the + variance by `λ(G) ^ (2 t)`. * `Cslib.RotationMap.abs_card_interedges_sub_le`, `Cslib.RotationMap.abs_card_interedges_sub_le_mul_sqrt`: the expander mixing lemma. * `Cslib.RotationMap.le_card_interedges_compl_of_expect_mul_walk_le`, @@ -105,6 +107,18 @@ theorem expect_mul_walk_pow_eq (t : ℕ) (f g : V → ℝ) : Fintype.expect_const] ring +/-- **Variance decay along walks**: a walk of length `t` multiplies the variance of a function, +its second moment about the mean, by at most `λ(G) ^ (2 t)`; the mean is preserved by +`expect_walk_pow`. -/ +theorem expect_walk_pow_sub_expect_sq_le (t : ℕ) (f : V → ℝ) : + 𝔼 v, ((G.walk ^ t) f v - 𝔼 w, f w) ^ 2 ≤ + G.spectralExpansion ^ (2 * t) * 𝔼 v, (f v - 𝔼 w, f w) ^ 2 := by + have hf : (G.walk ^ t) (fun w ↦ f w - 𝔼 u, f u) = fun v ↦ (G.walk ^ t) f v - 𝔼 u, f u := by + rw [show (fun w ↦ f w - 𝔼 u, f u) = f - fun _ ↦ 𝔼 u, f u from rfl, map_sub, walk_pow_const] + rfl + have h := G.expect_walk_pow_sq_le_spectralExpansion_pow_mul (expect_sub_expect f) t + rwa [hf] at h + /-- **The mixing lemma for functions**: the correlation `𝔼 v, f v * (G.walk ^ t) g v` of `f` with `g` along walks of length `t` differs from the product of their expectations by at most `λ(G) ^ t` times their standard deviations. Squared: the square of the difference is at most diff --git a/Complexity/Probability/PairwiseIndependentHash/ConditionalAveraging.lean b/Complexity/Probability/PairwiseIndependentHash/ConditionalAveraging.lean new file mode 100644 index 0000000000..04001ee813 --- /dev/null +++ b/Complexity/Probability/PairwiseIndependentHash/ConditionalAveraging.lean @@ -0,0 +1,336 @@ +/- +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.Combinatorics.Expander.Mixing +public import Complexity.Foundations.Combinatorics.Expander.Perm +public import Complexity.Foundations.Combinatorics.Expander.Reindex +public import Complexity.Probability.PairwiseIndependentHash.FrameChannel + +/-! +# Conditional averaging on retention slices + +A *retention slice* (`Cslib.Probability.RetentionSlice`) is the set of frame-conditioned channels +`A = (a₀, F)` that retain a fixed identifier `y`; its uniform law is the channel law conditioned on +retaining `y`. In the coordinates `(F, w)` of `sliceEquiv`, with `w ∈ ZMod L ^ H` the value at `y`, +an integer matrix `g` of determinant one and an integer vector `c` act by the **affine move** + +`coordMove g c (F, w) = (g F mod P, g w + c mod L)`. + +Any regular multigraph `G` on the coordinates transports to a walk on every slice +(`sliceGraph`), with the same spectral expansion (`spectralExpansion_sliceGraph`). Hence a single +spectral-gap bound for `G`, independent of `y`, gives **conditional averaging**: on every slice, the +walk of length `t` contracts the conditional variance by `λ(G) ^ (2 t)` +(`expect_walk_pow_sliceGraph_sub_expect_sq_le`). The bound for the walk of the preprint's affine +moves on frames (the frame-lifted gap) is a hypothesis here; later work supplies it. + +**Validated variants.** The move on a slice refers to `y`, but it is realized by permutations of +the full channel space that do not: + +`variantMove L g c z (a₀, F) = (g a₀ + c + L z, g F) mod P`, + +one for each integer *wrap* vector `z`. Each variant is a bijection of all channels. Computing +`x = g w + c` over the integers from the representatives `w` of `A.eval y`, the *wrap test* +`IsValidWrap L g c z (A.eval y)` checks that `x + L z` lies in `{0, …, L - 1} ^ H`. Exactly one +`z` passes, namely `wrap L g c (A.eval y) = -⌊x / L⌋` (`isValidWrap_iff`), and it lies in the +fixed box `|z i| ≤ ∑ j, |g i j| + |c i|` for every side length (`abs_wrap_le`). On a channel +retaining `y`, that variant is the affine move (`variantMove_wrap_eq`). So the sum of the passing +variants over any candidate set of wraps is the move (`sum_ite_isValidWrap`), and the walk of a +family of moves on a slice is the average over moves of these sums +(`walk_sliceGraph_ofPerms_eq`). + +This formalizes ideas of Section 6 of the OpenAI preprint [OpenAI2026LogSpace]: the +coordinates and the action `(F, w) ↦ (MF, Mw + c)` in the proof of Lemma 6.2, and the variants +`A' = MA + (c + Lz) e₁ᵀ (mod P)` with their unique valid wrap `zᵢ = -⌊(Mw + c)ᵢ / L⌋` in the +proof of Lemma 6.3 (items 1–4 for a single step). The preprint's walk uses the elementary +generators of `SL_H(ℤ) ⋉ ℤ^H` and its gap comes from property (T) (Lemma 6.1); here the walk and +its gap are left abstract. Transitivity of the action, the product over several channels, and +`L^s` bounds for `s > 2` are not part of this module. + +## Main definitions + +* `Cslib.Probability.affineSL`: the affine permutation `v ↦ g v + c` of `R ^ n`, for `g` an integer + matrix of determinant one. +* `Cslib.Probability.coordMove`: the affine move on slice coordinates. +* `Cslib.Probability.sliceGraph`: a graph on the coordinates, transported to a retention slice. +* `Cslib.Probability.variantMove`: a variant, a permutation of all channels. +* `Cslib.Probability.IsValidWrap`, `Cslib.Probability.wrap`: the wrap test and its solution. + +## Main results + +* `Cslib.Probability.coordMove_symm`: the inverse move is the move of the inverse. +* `Cslib.Probability.spectralExpansion_sliceGraph`: the transported walk keeps its gap. +* `Cslib.Probability.expect_walk_pow_sliceGraph_sub_expect_sq_le`: conditional averaging. +* `Cslib.Probability.eval_variantMove`: a variant acts affinely on every evaluation. +* `Cslib.Probability.isValidWrap_iff`, `Cslib.Probability.abs_wrap_le`: the valid wrap is unique + and bounded independently of `L` and `P`. +* `Cslib.Probability.variantMove_wrap_eq`: on a slice, the valid variant is the affine move. +* `Cslib.Probability.sum_ite_isValidWrap`, `Cslib.Probability.walk_sliceGraph_ofPerms_eq`: the + sum of the valid variants is the conditional move, and averages to the conditional walk. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace] +-/ + +public section + +namespace Cslib.Probability + +open Finset Matrix +open scoped BigOperators + +section Affine + +variable {n : Type*} [Fintype n] [DecidableEq n] (R : Type*) [CommRing R] + +/-- The affine permutation `v ↦ g v + c` of `R ^ n`, for an integer matrix `g` of determinant one +reduced into `R`. -/ +@[expose] def affineSL (g : SpecialLinearGroup n ℤ) (c : n → R) : Equiv.Perm (n → R) := + (SpecialLinearGroup.toLin' (SpecialLinearGroup.map (Int.castRingHom R) g)).toEquiv.trans + (Equiv.addRight c) + +@[simp] +theorem affineSL_apply (g : SpecialLinearGroup n ℤ) (c : n → R) (v : n → R) : + affineSL R g c v = (SpecialLinearGroup.map (Int.castRingHom R) g : Matrix n n R) *ᵥ v + c := + rfl + +end Affine + +variable {P H r L : ℕ} [NeZero P] + +/-- The **affine move** `(F, w) ↦ (g F, g w + c)` on slice coordinates: `g` acts on the frame +modulo `P` and on the box coordinate modulo `L`. -/ +@[expose] def coordMove (g : SpecialLinearGroup (Fin H) ℤ) (c : Fin H → ℤ) : + Equiv.Perm (Frame P H r × (Fin H → ZMod L)) := + (Frame.mapSL g).prodCongr (affineSL (ZMod L) g fun i ↦ (c i : ZMod L)) + +omit [NeZero P] in +/-- The inverse of the move by `(g, c)` is the move by `(g⁻¹, -g⁻¹ c)`. -/ +theorem coordMove_symm (g : SpecialLinearGroup (Fin H) ℤ) (c : Fin H → ℤ) : + (coordMove (P := P) (r := r) (L := L) g c).symm = + coordMove g⁻¹ + (-(((g⁻¹ : SpecialLinearGroup (Fin H) ℤ) : Matrix (Fin H) (Fin H) ℤ) *ᵥ c)) := by + refine Equiv.ext fun p ↦ (coordMove (P := P) (r := r) (L := L) g c).injective ?_ + rw [Equiv.apply_symm_apply] + obtain ⟨F, w⟩ := p + ext j i + · simp only [coordMove, Equiv.prodCongr_apply, Prod.map_fst, Frame.mapSL_apply, mulVec_mulVec, + ← SpecialLinearGroup.coe_mul, ← map_mul, mul_inv_cancel, map_one, SpecialLinearGroup.coe_one, + one_mulVec] + · have hc : (fun i ↦ (((-(((g⁻¹ : SpecialLinearGroup (Fin H) ℤ) : Matrix (Fin H) (Fin H) ℤ) *ᵥ + c)) i : ℤ) : ZMod L)) = -((SpecialLinearGroup.map (Int.castRingHom (ZMod L)) g⁻¹ : + Matrix (Fin H) (Fin H) (ZMod L)) *ᵥ fun i ↦ (c i : ZMod L)) := by + ext i + rw [Pi.neg_apply, Pi.neg_apply, Int.cast_neg, SpecialLinearGroup.map_apply_coe, + RingHom.mapMatrix_apply] + exact congrArg Neg.neg (RingHom.map_mulVec (Int.castRingHom (ZMod L)) _ c i) + simp only [coordMove, Equiv.prodCongr_apply, Prod.map_snd, affineSL_apply, hc, mulVec_add, + mulVec_neg, mulVec_mulVec, ← SpecialLinearGroup.coe_mul, ← map_mul, mul_inv_cancel, map_one, + SpecialLinearGroup.coe_one, one_mulVec] + simp + +variable (L) in +/-- A graph `G` on slice coordinates, transported to the retention slice of `y`. -/ +@[expose] def sliceGraph [NeZero L] (hL : L ≤ P) (y : ZMod P) {D : Type*} + (G : RotationMap (Frame P H r × (Fin H → ZMod L)) D) : + RotationMap (RetentionSlice P H r L y) D := + G.reindex (sliceEquiv hL y).symm + +/-- The walk on a slice has the spectral expansion of the walk on coordinates, for every +identifier `y`. -/ +@[simp] +theorem spectralExpansion_sliceGraph [NeZero L] (hL : L ≤ P) (y : ZMod P) {D : Type*} [Fintype D] + (G : RotationMap (Frame P H r × (Fin H → ZMod L)) D) : + (sliceGraph L hL y G).spectralExpansion = G.spectralExpansion := + G.spectralExpansion_reindex _ + +/-- **Conditional averaging.** Let `G` be any regular multigraph on the slice coordinates, for +example the walk of affine moves, whose spectral expansion is at most `λ`. Then on the retention +slice of every identifier `y`, the walk of length `t` contracts the conditional variance by +`λ ^ (2 t)`, uniformly in `y`; the conditional mean is preserved (`expect_walk_pow`). The bound +`λ` is the hypothesis that the frame-lifted gap must supply. -/ +theorem expect_walk_pow_sliceGraph_sub_expect_sq_le [NeZero L] (hL : L ≤ P) {D : Type*} + [Fintype D] [Nonempty D] (G : RotationMap (Frame P H r × (Fin H → ZMod L)) D) {lam : ℝ} + (hG : G.spectralExpansion ≤ lam) (y : ZMod P) (f : RetentionSlice P H r L y → ℝ) (t : ℕ) : + 𝔼 A, (((sliceGraph L hL y G).walk ^ t) f A - 𝔼 B, f B) ^ 2 ≤ + lam ^ (2 * t) * 𝔼 A, (f A - 𝔼 B, f B) ^ 2 := by + refine ((sliceGraph L hL y G).expect_walk_pow_sub_expect_sq_le t f).trans ?_ + rw [spectralExpansion_sliceGraph] + exact mul_le_mul_of_nonneg_right (pow_le_pow_left₀ G.spectralExpansion_nonneg hG _) + (expect_nonneg fun _ _ ↦ sq_nonneg _) + +/-! ### Validated variants -/ + +variable (L) in +/-- A **validated-walk variant**: the permutation `(a₀, F) ↦ (g a₀ + c + L z, g F)` of all +channels, modulo `P`. It does not depend on any identifier. -/ +@[expose] def variantMove (g : SpecialLinearGroup (Fin H) ℤ) (c z : Fin H → ℤ) : + Equiv.Perm (FrameChannel P H r) := + (affineSL (ZMod P) g fun i ↦ ((c i + L * z i : ℤ) : ZMod P)).prodCongr (Frame.mapSL g) + +omit [NeZero P] in +/-- A variant acts on the value at every identifier by the same affine map. -/ +theorem eval_variantMove (g : SpecialLinearGroup (Fin H) ℤ) (c z : Fin H → ℤ) + (A : FrameChannel P H r) (y : ZMod P) : + (variantMove L g c z A).eval y = + (SpecialLinearGroup.map (Int.castRingHom (ZMod P)) g : Matrix _ _ (ZMod P)) *ᵥ A.eval y + + fun i ↦ ((c i + L * z i : ℤ) : ZMod P) := by + simp only [variantMove, FrameChannel.eval, Equiv.prodCongr_apply, Prod.map_fst, Prod.map_snd, + affineSL_apply, Frame.mapSL_apply, mulVec_add, mulVec_sum, mulVec_smul] + abel + +/-- The integer vector `g w + c`, computed from the representatives `w` of a value. -/ +@[expose] def wrapTarget (g : SpecialLinearGroup (Fin H) ℤ) (c : Fin H → ℤ) (w : Fin H → ZMod P) : + Fin H → ℤ := + (g : Matrix (Fin H) (Fin H) ℤ) *ᵥ (fun j ↦ ((w j).val : ℤ)) + c + +variable (L) in +/-- The **wrap test** for a variant: `g w + c + L z`, computed over the integers from the +representatives `w` of the value, lies in `{0, …, L - 1} ^ H`. -/ +@[expose] def IsValidWrap (g : SpecialLinearGroup (Fin H) ℤ) (c z : Fin H → ℤ) + (w : Fin H → ZMod P) : Prop := + ∀ i, 0 ≤ wrapTarget g c w i + L * z i ∧ wrapTarget g c w i + L * z i < L + +instance (g : SpecialLinearGroup (Fin H) ℤ) (c z : Fin H → ℤ) (w : Fin H → ZMod P) : + Decidable (IsValidWrap L g c z w) := + inferInstanceAs (Decidable (∀ _, _)) + +variable (L) in +/-- The valid wrap `z = -⌊(g w + c) / L⌋`. -/ +@[expose] def wrap (g : SpecialLinearGroup (Fin H) ℤ) (c : Fin H → ℤ) (w : Fin H → ZMod P) : + Fin H → ℤ := + fun i ↦ -(wrapTarget g c w i / L) + +omit [NeZero P] in +/-- **Uniqueness of the valid wrap**: exactly one wrap vector passes the test. -/ +theorem isValidWrap_iff [NeZero L] {g : SpecialLinearGroup (Fin H) ℤ} {c z : Fin H → ℤ} + {w : Fin H → ZMod P} : IsValidWrap L g c z w ↔ z = wrap L g c w := by + have hL : (0 : ℤ) < L := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne L) + refine ⟨fun h ↦ funext fun i ↦ ?_, fun h i ↦ ?_⟩ + · have := (Int.ediv_emod_unique hL).2 + ⟨show wrapTarget g c w i + L * z i + L * -z i = wrapTarget g c w i by ring, h i⟩ + simp only [wrap, this.1, neg_neg] + · have hmod := Int.emod_def (wrapTarget g c w i) L + simp only [h, wrap, mul_neg, ← sub_eq_add_neg, ← hmod] + exact ⟨Int.emod_nonneg _ hL.ne', Int.emod_lt_of_pos _ hL⟩ + +/-- **The wrap box**: for a value in the retention box, the valid wrap satisfies +`|z i| ≤ ∑ j, |g i j| + |c i|`, a bound independent of `L` and `P`. So finitely many variants per +move suffice for every side length. -/ +theorem abs_wrap_le [NeZero L] (g : SpecialLinearGroup (Fin H) ℤ) (c : Fin H → ℤ) + {w : Fin H → ZMod P} (hw : w ∈ retentionBox P H L) (i : Fin H) : + |wrap L g c w i| ≤ ∑ j, |g i j| + |c i| := by + have hL : (0 : ℤ) < L := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne L) + simp only [wrap, abs_neg] + have hterm (j : Fin H) : |g i j * ((w j).val : ℤ)| ≤ |g i j| * L := by + rw [abs_mul, abs_of_nonneg (Int.natCast_nonneg _)] + have : ((w j).val : ℤ) ≤ L := by exact_mod_cast (mem_retentionBox.1 hw j).le + exact mul_le_mul_of_nonneg_left this (abs_nonneg _) + have hx : |wrapTarget g c w i| ≤ L * (∑ j, |g i j| + |c i|) := by + have h1 : |∑ j, g i j * ((w j).val : ℤ)| ≤ ∑ j, |g i j| * L := + (abs_sum_le_sum_abs _ _).trans (sum_le_sum fun j _ ↦ hterm j) + have h2 : |c i| ≤ |c i| * L := le_mul_of_one_le_right (abs_nonneg _) hL + calc |wrapTarget g c w i| = |∑ j, g i j * ((w j).val : ℤ) + c i| := rfl + _ ≤ |∑ j, g i j * ((w j).val : ℤ)| + |c i| := abs_add_le _ _ + _ ≤ ∑ j, |g i j| * L + |c i| * L := add_le_add h1 h2 + _ = L * (∑ j, |g i j| + |c i|) := by rw [← sum_mul]; ring + generalize wrapTarget g c w i = x at hx ⊢ + generalize ∑ j, |g i j| + |c i| = S at hx ⊢ + have hlo := Int.mul_ediv_self_le (x := x) hL.ne' + have hhi := Int.lt_ediv_add_one_mul_self x hL + rw [abs_le] at hx ⊢ + constructor + · by_contra h + have : x / L + 1 ≤ -S := by omega + nlinarith + · by_contra h + have : S + 1 ≤ x / L := by omega + nlinarith + +/-- **The valid variant is the conditional move.** On a channel retaining `y`, the variant with the +valid wrap maps it to the channel with coordinates `coordMove g c (F, w)`. In particular it +retains `y` again. -/ +theorem variantMove_wrap_eq [NeZero L] (hL : L ≤ P) {y : ZMod P} + (g : SpecialLinearGroup (Fin H) ℤ) (c : Fin H → ℤ) (A : RetentionSlice P H r L y) : + variantMove L g c (wrap L g c (A.1.eval y)) A.1 = + ((sliceEquiv hL y).symm (coordMove g c (sliceEquiv hL y A))).1 := by + refine (FrameChannel.evalEquiv y).injective (Prod.ext (funext fun i ↦ ?_) ?_) + · have hrep : A.1.eval y = fun j ↦ (((A.1.eval y j).val : ℤ) : ZMod P) := by + ext j + simp + have hP : ((SpecialLinearGroup.map (Int.castRingHom (ZMod P)) g : Matrix _ _ (ZMod P)) *ᵥ + A.1.eval y) i = ((((g : Matrix _ _ ℤ) *ᵥ fun j ↦ ((A.1.eval y j).val : ℤ)) i : ℤ) : + ZMod P) := by + conv_lhs => rw [hrep] + rw [SpecialLinearGroup.map_apply_coe, RingHom.mapMatrix_apply] + exact (RingHom.map_mulVec (Int.castRingHom (ZMod P)) _ _ i).symm + have hLmod : (((SpecialLinearGroup.map (Int.castRingHom (ZMod L)) g : Matrix _ _ (ZMod L)) *ᵥ + fun j ↦ (((A.1.eval y j).val : ℕ) : ZMod L)) i + (c i : ZMod L)) = + ((wrapTarget g c (A.1.eval y) i : ℤ) : ZMod L) := by + have hcast : (fun j ↦ (((A.1.eval y j).val : ℕ) : ZMod L)) = + Int.castRingHom (ZMod L) ∘ fun j ↦ ((A.1.eval y j).val : ℤ) := by + ext j + simp + rw [wrapTarget, Pi.add_apply, Int.cast_add, SpecialLinearGroup.map_apply_coe, + RingHom.mapMatrix_apply, hcast] + exact congrArg (· + (c i : ZMod L)) + (RingHom.map_mulVec (Int.castRingHom (ZMod L)) _ _ i).symm + have hval : ((((wrapTarget g c (A.1.eval y) i : ℤ) : ZMod L).val : ℕ) : ZMod P) = + ((wrapTarget g c (A.1.eval y) i % L : ℤ) : ZMod P) := by + rw [← ZMod.val_intCast, Int.cast_natCast] + simp only [FrameChannel.evalEquiv_apply, eval_variantMove, Pi.add_apply, hP, + eval_sliceEquiv_symm, sliceEquiv_apply, coordMove, Equiv.prodCongr_apply, Prod.map_snd, + affineSL_apply, hLmod, hval] + rw [Int.emod_def] + simp only [wrap, wrapTarget, Pi.add_apply] + push_cast + ring + · rfl + +/-- **Exactly one variant survives** (Lemma 6.3, items 3 and 4, for one step). For a channel +retaining `y` and any candidate set `Z` of wraps containing the valid one, the sum over `Z` of +the variants passing the wrap test is the value at the conditional move. -/ +theorem sum_ite_isValidWrap [NeZero L] (hL : L ≤ P) {y : ZMod P} {M : Type*} [AddCommMonoid M] + (g : SpecialLinearGroup (Fin H) ℤ) (c : Fin H → ℤ) (A : RetentionSlice P H r L y) + {Z : Finset (Fin H → ℤ)} (hZ : wrap L g c (A.1.eval y) ∈ Z) (f : FrameChannel P H r → M) : + ∑ z ∈ Z, (if IsValidWrap L g c z (A.1.eval y) then f (variantMove L g c z A.1) else 0) = + f ((sliceEquiv hL y).symm (coordMove g c (sliceEquiv hL y A))).1 := by + simp only [isValidWrap_iff, sum_ite_eq', hZ, ite_true] + rw [variantMove_wrap_eq hL] + +/-- The forward move of a generator `(g, c)` for `b = false`, and its inverse for `b = true`. -/ +@[expose] def signedMove {H : ℕ} (m : SpecialLinearGroup (Fin H) ℤ × (Fin H → ℤ)) (b : Bool) : + SpecialLinearGroup (Fin H) ℤ × (Fin H → ℤ) := + bif b then (m.1⁻¹, -(((m.1⁻¹ : SpecialLinearGroup (Fin H) ℤ) : Matrix (Fin H) (Fin H) ℤ) *ᵥ m.2)) + else m + +/-- **The conditional walk as an average of valid variants.** For a family `σ` of affine +generators, the walk of `ofPerms` of their moves, transported to the slice of `y`, applied to a +function `f` of the channel, is the average over generators and directions of the sums of the +valid variants. -/ +theorem walk_sliceGraph_ofPerms_eq [NeZero L] (hL : L ≤ P) {y : ZMod P} {K : Type*} [Fintype K] + (σ : K → SpecialLinearGroup (Fin H) ℤ × (Fin H → ℤ)) {Z : Finset (Fin H → ℤ)} + (hZ : ∀ k b, ∀ w ∈ retentionBox P H L, + wrap L (signedMove (σ k) b).1 (signedMove (σ k) b).2 w ∈ Z) + (f : FrameChannel P H r → ℝ) (A : RetentionSlice P H r L y) : + (sliceGraph L hL y (RotationMap.ofPerms fun k ↦ coordMove (σ k).1 (σ k).2)).walk + (fun B ↦ f B.1) A = + 𝔼 kb : K × Bool, ∑ z ∈ Z, + (if IsValidWrap L (signedMove (σ kb.1) kb.2).1 (signedMove (σ kb.1) kb.2).2 z (A.1.eval y) + then f (variantMove L (signedMove (σ kb.1) kb.2).1 (signedMove (σ kb.1) kb.2).2 z A.1) + else 0) := by + rw [RotationMap.walk_apply] + refine expect_congr rfl fun ⟨k, b⟩ _ ↦ ?_ + rw [sum_ite_isValidWrap hL _ _ A (hZ k b _ A.2)] + cases b + · rfl + · simp only [sliceGraph, RotationMap.neighbor_reindex, RotationMap.neighbor_ofPerms_true, + Equiv.symm_symm, signedMove, Bool.cond_true, coordMove_symm] + +end Cslib.Probability diff --git a/Complexity/Probability/PairwiseIndependentHash/FrameChannel.lean b/Complexity/Probability/PairwiseIndependentHash/FrameChannel.lean new file mode 100644 index 0000000000..c42f9dad82 --- /dev/null +++ b/Complexity/Probability/PairwiseIndependentHash/FrameChannel.lean @@ -0,0 +1,231 @@ +/- +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.Probability.PairwiseIndependentHash.RetentionChannel +public import Mathlib.LinearAlgebra.LinearIndependent.Defs +public import Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup +import Mathlib.LinearAlgebra.StdBasis + +/-! +# Frame-conditioned retention channels and their retention slices + +A *frame* is an ordered linearly independent family `F : Fin r → (Fin H → ZMod P)`. A +*frame-conditioned channel* is a pair `A = (a₀, F)` of a constant column `a₀ : Fin H → ZMod P` +and a frame `F`. It evaluates an identifier `y : ZMod P` as the polynomial + +`A.eval y = a₀ + ∑ j, y ^ (j + 1) • F j`, + +and retains `y` when `A.eval y` lies in the retention box `retentionBox P H L`. Drawing a +uniformly random frame-conditioned channel is drawing a uniformly random `H × (r + 1)` matrix +conditioned on its last `r` columns being linearly independent. + +For a fixed identifier `y`, the map `A ↦ (F, A.eval y)` is a bijection, since `a₀` is recovered +from the value and the frame (`evalEquiv`). Hence the frame and the evaluation are independent, +the evaluation is uniform, and `y` is retained with probability exactly `(L / P) ^ H` for every +`y` and every `r ≤ H` (`dens_eval_mem_retentionBox`), as without frame conditioning. On the +*retention slice* of `y`, the channels retaining `y`, the same bijection gives coordinates +`(F, w)` with `w` in the box `{0, …, L - 1} ^ H`, which we identify with `ZMod L ^ H` +(`sliceEquiv`). Conditional averaging on the slice is done in these coordinates +(`Complexity.Probability.PairwiseIndependentHash.ConditionalAveraging`). + +This follows the rank channels of Section 3 of the OpenAI preprint [OpenAI2026LogSpace] +(channel matrices conditioned on their non-constant columns forming a frame), the exact marginal +in the proof of its Lemma 3.1, and the coordinates `(F, w)` of the proof of its Lemma 6.2. + +## Main definitions + +* `Cslib.Probability.Frame`: ordered linearly independent `r`-tuples in `ZMod P ^ H`. +* `Cslib.Probability.Frame.mapSL`: an integer matrix of determinant one acting on frames. +* `Cslib.Probability.FrameChannel`, `Cslib.Probability.FrameChannel.eval`: frame-conditioned + channels and their evaluation at an identifier. +* `Cslib.Probability.FrameChannel.evalEquiv`: a channel is its value at `y` and its frame. +* `Cslib.Probability.retentionBoxEquiv`: the retention box as `ZMod L ^ H`. +* `Cslib.Probability.RetentionSlice`, `Cslib.Probability.sliceEquiv`: the channels retaining + `y`, and their coordinates `(F, w)`. + +## Main results + +* `Cslib.Probability.dens_eval_mem_retentionBox`: under frame conditioning, every identifier is + retained with probability exactly `(L / P) ^ H`. +* `Cslib.Probability.card_retentionSlice`: the slice has `#frames · L ^ H` channels. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace] +-/ + +public section + +namespace Cslib.Probability + +open Finset Matrix +open scoped BigOperators + +variable (P H r : ℕ) + +/-- A **frame**: an ordered linearly independent family of `r` vectors in `ZMod P ^ H`. -/ +abbrev Frame : Type := + {F : Fin r → Fin H → ZMod P // LinearIndependent (ZMod P) F} + +/-- Linear independence of a finite family over `ZMod P` is decided by testing all +coefficient vectors. -/ +instance [NeZero P] : Fintype (Frame P H r) := + haveI : DecidablePred fun F : Fin r → Fin H → ZMod P ↦ LinearIndependent (ZMod P) F := fun F ↦ + decidable_of_iff (∀ g : Fin r → ZMod P, ∑ i, g i • F i = 0 → ∀ i, g i = 0) + Fintype.linearIndependent_iff.symm + Subtype.fintype _ + +variable {P H r} + +/-- For `r ≤ H` the first `r` standard basis vectors form a frame. -/ +theorem Frame.nonempty (hr : r ≤ H) : Nonempty (Frame P H r) := + ⟨⟨Pi.basisFun (ZMod P) (Fin H) ∘ Fin.castLE hr, + (Pi.basisFun (ZMod P) (Fin H)).linearIndependent.comp _ (Fin.castLE_injective hr)⟩⟩ + +/-- An integer matrix of determinant one, reduced modulo `P`, maps frames to frames, column by +column. -/ +@[expose] def Frame.mapSL (g : SpecialLinearGroup (Fin H) ℤ) : Frame P H r ≃ Frame P H r := + let e := SpecialLinearGroup.toLin' (SpecialLinearGroup.map (Int.castRingHom (ZMod P)) g) + Equiv.subtypeEquiv (Equiv.piCongrRight fun _ ↦ e.toEquiv) fun _ ↦ + (e.toLinearMap.linearIndependent_iff e.ker).symm + +@[simp] +theorem Frame.mapSL_apply (g : SpecialLinearGroup (Fin H) ℤ) (F : Frame P H r) (j : Fin r) : + (Frame.mapSL g F).1 j = (SpecialLinearGroup.map (Int.castRingHom (ZMod P)) g : Matrix _ _ _) + *ᵥ F.1 j := + rfl + +variable (P H r) + +/-- A **frame-conditioned channel**: a constant column and a frame. -/ +abbrev FrameChannel : Type := + (Fin H → ZMod P) × Frame P H r + +variable {P H r} + +/-- The value `a₀ + ∑ j, y ^ (j + 1) • F j` of the channel `A = (a₀, F)` at the identifier +`y`. -/ +@[expose] def FrameChannel.eval (A : FrameChannel P H r) (y : ZMod P) : Fin H → ZMod P := + A.1 + ∑ j : Fin r, y ^ (j.val + 1) • A.2.1 j + +/-- **Coordinates of a channel at `y`**: its value at `y` and its frame. The constant column is +recovered as the value minus the frame part. -/ +@[expose] def FrameChannel.evalEquiv (y : ZMod P) : + FrameChannel P H r ≃ (Fin H → ZMod P) × Frame P H r where + toFun A := (A.eval y, A.2) + invFun p := (p.1 - ∑ j : Fin r, y ^ (j.val + 1) • p.2.1 j, p.2) + left_inv A := by simp [FrameChannel.eval] + right_inv p := by simp [FrameChannel.eval] + +@[simp] +theorem FrameChannel.evalEquiv_apply (y : ZMod P) (A : FrameChannel P H r) : + FrameChannel.evalEquiv y A = (A.eval y, A.2) := + rfl + +variable {L : ℕ} [NeZero P] + +/-- **Frame-conditioned retention rate**: for `r ≤ H` and `L ≤ P`, a uniformly random +frame-conditioned channel retains every identifier `y` with probability exactly +`(L / P) ^ H`. -/ +theorem dens_eval_mem_retentionBox (hr : r ≤ H) (hL : L ≤ P) (y : ZMod P) : + dens {A : FrameChannel P H r | A.eval y ∈ retentionBox P H L} = ((L : ℚ≥0) / P) ^ H := by + have := Frame.nonempty (P := P) hr + have hcard : #{A : FrameChannel P H r | A.eval y ∈ retentionBox P H L} = + L ^ H * Fintype.card (Frame P H r) := by + rw [← card_retentionBox (H := H) hL, ← card_univ (α := Frame P H r), ← card_product] + refine card_bij (fun A _ ↦ FrameChannel.evalEquiv y A) (fun A hA ↦ ?_) + (fun _ _ _ _ h ↦ (FrameChannel.evalEquiv y).injective h) fun p hp ↦ ?_ + · simpa using hA + · refine ⟨(FrameChannel.evalEquiv y).symm p, ?_, by simp⟩ + have : ((FrameChannel.evalEquiv y).symm p).eval y = p.1 := by + simp [FrameChannel.evalEquiv, FrameChannel.eval] + simpa [this] using (mem_product.1 hp).1 + have hpos : (0 : ℚ≥0) < Fintype.card (Frame P H r) := by exact_mod_cast Fintype.card_pos + rw [dens, hcard, Fintype.card_prod, Fintype.card_fun, Fintype.card_fin, ZMod.card, div_pow] + push_cast + rw [mul_div_mul_right _ _ hpos.ne'] + +variable (P H r L) + +/-- The **retention slice** of `y`: the frame-conditioned channels retaining `y`. -/ +abbrev RetentionSlice (y : ZMod P) : Type := + {A : FrameChannel P H r // A.eval y ∈ retentionBox P H L} + +variable {P H r L} + +/-- The retention box `{0, …, L - 1} ^ H` in `ZMod P ^ H` is `ZMod L ^ H` for `L ≤ P`, by +reading representatives. -/ +@[expose] def retentionBoxEquiv [NeZero L] (hL : L ≤ P) : + {w : Fin H → ZMod P // w ∈ retentionBox P H L} ≃ (Fin H → ZMod L) where + toFun w i := ((w.1 i).val : ZMod L) + invFun u := ⟨fun i ↦ ((u i).val : ZMod P), by + simp only [mem_retentionBox] + intro i + rw [ZMod.val_cast_of_lt ((ZMod.val_lt _).trans_le hL)] + exact ZMod.val_lt _⟩ + left_inv w := by + have hw := w.2 + simp only [mem_retentionBox] at hw + ext i + simp only + rw [ZMod.val_cast_of_lt (hw i), ZMod.natCast_zmod_val] + right_inv u := by + ext i + simp only + rw [ZMod.val_cast_of_lt ((ZMod.val_lt _).trans_le hL), ZMod.natCast_zmod_val] + +@[simp] +theorem retentionBoxEquiv_apply [NeZero L] (hL : L ≤ P) + (w : {w : Fin H → ZMod P // w ∈ retentionBox P H L}) (i : Fin H) : + retentionBoxEquiv hL w i = ((w.1 i).val : ZMod L) := + rfl + +@[simp] +theorem retentionBoxEquiv_symm_apply [NeZero L] (hL : L ≤ P) (u : Fin H → ZMod L) (i : Fin H) : + ((retentionBoxEquiv hL).symm u).1 i = ((u i).val : ZMod P) := + rfl + +/-- **Coordinates on a retention slice**: a channel retaining `y` is its frame together with its +value at `y`, which ranges over the whole box `ZMod L ^ H`. -/ +@[expose] def sliceEquiv [NeZero L] (hL : L ≤ P) (y : ZMod P) : + RetentionSlice P H r L y ≃ Frame P H r × (Fin H → ZMod L) := + ((FrameChannel.evalEquiv y).subtypeEquiv (p := fun A ↦ A.eval y ∈ retentionBox P H L) + (q := fun p ↦ p.1 ∈ retentionBox P H L) fun _ ↦ Iff.rfl).trans <| + (Equiv.prodSubtypeFstEquivSubtypeProd (p := (· ∈ retentionBox P H L))).trans <| + ((retentionBoxEquiv hL).prodCongr (Equiv.refl _)).trans (Equiv.prodComm _ _) + +@[simp] +theorem sliceEquiv_apply [NeZero L] (hL : L ≤ P) (y : ZMod P) (A : RetentionSlice P H r L y) : + sliceEquiv hL y A = (A.1.2, fun i ↦ ((A.1.eval y i).val : ZMod L)) := + rfl + +/-- The frame of a channel is its frame coordinate on the slice. -/ +@[simp] +theorem sliceEquiv_symm_apply_snd [NeZero L] (hL : L ≤ P) (y : ZMod P) + (p : Frame P H r × (Fin H → ZMod L)) : ((sliceEquiv hL y).symm p).1.2 = p.1 := by + have h := congrArg Prod.fst ((sliceEquiv hL y).apply_symm_apply p) + rwa [sliceEquiv_apply] at h + +/-- The value at `y` of the channel with coordinates `(F, w)` is `w`, read in `ZMod P`. -/ +@[simp] +theorem eval_sliceEquiv_symm [NeZero L] (hL : L ≤ P) (y : ZMod P) + (p : Frame P H r × (Fin H → ZMod L)) (i : Fin H) : + ((sliceEquiv hL y).symm p).1.eval y i = ((p.2 i).val : ZMod P) := by + have h := congrArg (fun q ↦ q.2 i) ((sliceEquiv hL y).apply_symm_apply p) + simp only [sliceEquiv_apply] at h + rw [← h, ZMod.val_cast_of_lt (mem_retentionBox.1 ((sliceEquiv hL y).symm p).2 i), + ZMod.natCast_zmod_val] + +/-- A retention slice has `#frames · L ^ H` channels. -/ +theorem card_retentionSlice [NeZero L] (hL : L ≤ P) (y : ZMod P) : + Fintype.card (RetentionSlice P H r L y) = Fintype.card (Frame P H r) * L ^ H := by + rw [Fintype.card_congr (sliceEquiv hL y), Fintype.card_prod, Fintype.card_fun, + Fintype.card_fin, ZMod.card] + +end Cslib.Probability diff --git a/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean b/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean index 1efd0065f3..aa0d08fb48 100644 --- a/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean +++ b/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean @@ -50,6 +50,7 @@ only for the later averaging walks, so they are not needed here. ## Main results +* `Cslib.Probability.mem_retentionBox`: membership in the box, coordinatewise. * `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. @@ -94,6 +95,11 @@ def retentionBox : Finset (Fin H → ZMod P) := variable {P H L} +/-- A vector lies in the retention box when each coordinate has representative less than `L`. -/ +@[simp] +theorem mem_retentionBox {v : Fin H → ZMod P} : v ∈ retentionBox P H L ↔ ∀ j, (v j).val < L := by + simp [retentionBox] + /-- `L` residues of `ZMod P` have representatives less than `L ≤ P`. -/ private theorem card_filter_val_lt (hL : L ≤ P) : #{a : ZMod P | a.val < L} = L := by have himage : ({a : ZMod P | a.val < L} : Finset (ZMod P)).image ZMod.val = range L := by diff --git a/ComplexityTests/ConditionalAveraging.lean b/ComplexityTests/ConditionalAveraging.lean new file mode 100644 index 0000000000..72e7b8b5c7 --- /dev/null +++ b/ComplexityTests/ConditionalAveraging.lean @@ -0,0 +1,91 @@ +/- +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.ConditionalAveraging +import Complexity.Foundations.Combinatorics.Expander.AffinePlane + +/-! +# Frame-conditioned channels and conditional averaging + +Frames over `𝔽₃` are counted directly, and a frame-conditioned channel over `𝔽₃` retains an +identifier at rate `2 / 3`, confirmed by a direct count of its six channels. + +Over `𝔽₅` with side `L = 3`, the shear `g = [[1, 1], [0, 1]]` and translation `c = (1, 0)` move +the value `w = (2, 2)` to `g w + c = (5, 2)`. The unique valid wrap is `z = (-1, 0)`, and the +variant it selects is the affine move `(5, 2) mod 3 = (2, 2)`. The wrap `z = 0` fails the integer +test even though its variant also lands in the retention box (`5 mod 5 = 0`): the retention test +alone does not identify the move. + +The conditional-averaging bound is applied to the affine-plane expander over `𝔽₃`, transported +to slice coordinates, which discharges its spectral hypothesis on every slice. +-/ + +namespace ComplexityTests.ConditionalAveraging + +open Cslib Cslib.Probability Finset Matrix +open scoped BigOperators + +private instance : Fact (Nat.Prime 3) := ⟨Nat.prime_three⟩ +private instance : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩ + +-- The nonzero vectors of `𝔽₃ ^ 2` are its frames of length one. +example : Fintype.card (Frame 3 2 1) = 8 := by decide + +-- Frame conditioning keeps the exact rate: `2 / 3` over `𝔽₃` with side `2`. +example (y : ZMod 3) : dens {A : FrameChannel 3 1 1 | A.eval y ∈ retentionBox 3 1 2} = 2 / 3 := by + rw [dens_eval_mem_retentionBox le_rfl (by norm_num)] + norm_num + +-- A direct count: `4` of the `6` channels retain the identifier `2`. +example : #{A : FrameChannel 3 1 1 | A.eval 2 ∈ retentionBox 3 1 2} = 4 := by decide + +/-- The shear `[[1, 1], [0, 1]]`. -/ +private def shear : SpecialLinearGroup (Fin 2) ℤ := + ⟨!![1, 1; 0, 1], by simp [det_fin_two]⟩ + +/-- A frame-conditioned channel over `𝔽₅` with value `(2, 2)` at `y = 1`. -/ +private def chan : FrameChannel 5 2 1 := + (![1, 2], ⟨![![1, 0]], linearIndependent_unique_iff.2 (by decide)⟩) + +example : chan.eval 1 = ![2, 2] := by decide + +-- The valid wrap is `-⌊(5, 2) / 3⌋ = (-1, 0)`; it passes the integer test, and `0` does not. +example : wrap 3 shear ![1, 0] (chan.eval 1) = ![-1, 0] := by decide +example : IsValidWrap 3 shear ![1, 0] ![-1, 0] (chan.eval 1) := by decide +example : ¬ IsValidWrap 3 shear ![1, 0] 0 (chan.eval 1) := by decide + +-- The valid variant gives the affine move `(5, 2) mod 3 = (2, 2)`. +example : (variantMove 3 shear ![1, 0] ![-1, 0] chan).eval 1 = ![2, 2] := by decide + +-- The wrap `0` also lands in the retention box, at the wrong value `(0, 2)`. +example : (variantMove 3 shear ![1, 0] 0 chan).eval 1 = ![0, 2] := by decide +example : (variantMove 3 shear ![1, 0] 0 chan).eval 1 ∈ retentionBox 5 2 3 := by decide + +-- Wraps of every side length lie in the box `|zᵢ| ≤ ∑ⱼ |gᵢⱼ| + |cᵢ|`. +example : |wrap 3 shear ![1, 0] (chan.eval 1) 0| ≤ 3 := + (abs_wrap_le shear ![1, 0] (by decide) 0).trans (by decide) + +/-- With no frame coordinates, slice coordinates in `𝔽₃ ^ 2` are the affine plane over `𝔽₃`. -/ +private def planeEquiv : Frame 5 2 0 × (Fin 2 → ZMod 3) ≃ ZMod 3 × ZMod 3 := + haveI : Unique (Frame 5 2 0) := + { default := ⟨![], linearIndependent_empty_type⟩ + uniq := fun _ ↦ Subsingleton.elim _ _ } + (Equiv.uniqueProd _ _).trans (finTwoArrowEquiv _) + +-- Conditional averaging with the affine-plane gap `√(1 / 3)`: on the slice of every identifier, +-- `t` steps contract the conditional variance by `(1 / 3) ^ t`. +example (y : ZMod 5) (f : RetentionSlice 5 2 0 3 y → ℝ) (t : ℕ) : + 𝔼 A, (((sliceGraph 3 (by norm_num) y + ((RotationMap.affinePlane (ZMod 3)).reindex planeEquiv.symm)).walk ^ t) f A - + 𝔼 B, f B) ^ 2 ≤ (1 / 3) ^ t * 𝔼 A, (f A - 𝔼 B, f B) ^ 2 := by + have hG : ((RotationMap.affinePlane (ZMod 3)).reindex planeEquiv.symm).spectralExpansion ≤ + Real.sqrt (1 / 3) := by + rw [RotationMap.spectralExpansion_reindex] + simpa using RotationMap.spectralExpansion_affinePlane_le (ZMod 3) + have h := expect_walk_pow_sliceGraph_sub_expect_sq_le (by norm_num) _ hG y f t + rwa [pow_mul, Real.sq_sqrt (by norm_num)] at h + +end ComplexityTests.ConditionalAveraging