feat(Probability): fourth-moment conditional averaging and validated words of every length

Complexity.lean

@@ -3170,9 +3170,11 @@ public import Complexity.Probability.PairwiseIndependentHash.HierarchyChannels
 public import Complexity.Probability.PairwiseIndependentHash.Retention
 public import Complexity.Probability.PairwiseIndependentHash.RetentionChannel
 public import Complexity.Probability.PairwiseIndependentHash.Shift
+public import Complexity.Probability.PairwiseIndependentHash.SliceFourthMoment
 public import Complexity.Probability.PairwiseIndependentHash.SliceGap
 public import Complexity.Probability.PairwiseIndependentHash.Toeplitz
 public import Complexity.Probability.PairwiseIndependentHash.Universal
+public import Complexity.Probability.PairwiseIndependentHash.ValidatedWords
 public import Complexity.Probability.Pinsker
 public import Complexity.Probability.Product
 public import Complexity.Probability.ProductConditioning

Complexity/Probability/PairwiseIndependentHash/SliceFourthMoment.lean

@@ -0,0 +1,98 @@
+/-
+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.FourthMoment
+public import Complexity.Probability.PairwiseIndependentHash.ComponentGap
+
+/-!
+# Fourth-moment conditional averaging on retention slices
+
+The conditional averaging walks of the sampler contract fourth moments as well as second moments.
+On the retention slice of an identifier `y`, and on a product of retention slices of `J` channels
+together with free bits, `2 t` steps of the lazy affine walk multiply the fourth central moment of
+every function by at most
+
+`2 (1 - 1 / (155648 H ^ 4)) ^ (2 t)`, respectively `2 (1 - 1 / (155648 (J + 1) H ^ 4)) ^ (2 t)`,
+
+uniformly in the primes, the sides, the identifiers and the torus modulus
+(`expect_walk_pow_sliceGraph_affineMove_sub_expect_pow_four_le`,
+`expect_walk_pow_componentMove_sub_expect_pow_four_le`). This combines the fourth-moment decay of
+a walk from its spectral gap (`RotationMap.expect_walk_pow_two_mul_sub_expect_pow_four_le`) with
+the uniform gaps of the affine walks (`spectralExpansion_lazy_ofPerms_affineMove_le`,
+`spectralExpansion_lazy_ofPerms_componentMove_le`).
+
+This is the case `s = 4` of the `L^s` bound `‖K^d − Π‖_{s→s} ≤ C_s 2^{−c_s d}` of Lemma 6.2 of
+the OpenAI preprint on derandomizing logarithmic space [OpenAI2026LogSpace], for centered inputs.
+The preprint interpolates between `L²` and `L^∞` (Riesz–Thorin); the decay here comes from the
+`L²` gap by an elementary argument, with the constant `2` and the rate `λ ^ (2 t)` over `2 t`
+steps.
+
+## Main results
+
+* `Cslib.Probability.expect_walk_pow_sliceGraph_affineMove_sub_expect_pow_four_le`: on one
+  retention slice.
+* `Cslib.Probability.expect_walk_pow_componentMove_sub_expect_pow_four_le`: on a product of
+  retention slices with free bits.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace]
+-/
+
+public section
+
+namespace Cslib.Probability
+
+open Finset RotationMap
+open scoped BigOperators
+
+variable {P H L M J : ℕ}
+
+/-- A fourth-moment bound `2 λ ^ (2 t)` from a spectral-expansion bound `λ ≤ lam`. -/
+private theorem two_mul_pow_le {V D : Type*} [Fintype V] [Fintype D]
+    (G : RotationMap V D) {lam : ℝ} (hG : G.spectralExpansion ≤ lam) (t : ℕ) (X : ℝ)
+    (hX : 0 ≤ X) : 2 * G.spectralExpansion ^ (2 * t) * X ≤ 2 * lam ^ (2 * t) * X := by
+  gcongr
+  exact G.spectralExpansion_nonneg
+
+/-- **Fourth-moment conditional averaging on a retention slice**: on the retention slice of every
+identifier `y`, `2 t` steps of the lazy affine walk multiply the fourth central moment of every
+function by at most `2 (1 - 1 / (155648 H ^ 4)) ^ (2 t)`, for a prime `P`, `H ≥ 3` and
+`1 ≤ L ≤ P`, uniformly in `P`, `L` and `y`. -/
+theorem expect_walk_pow_sliceGraph_affineMove_sub_expect_pow_four_le [Fact P.Prime] [NeZero L]
+    (hH : 3 ≤ H) (hL : L ≤ P) (y : ZMod P) (f : RetentionSlice P H 1 L y → ℝ) (t : ℕ) :
+    𝔼 A, (((sliceGraph L hL y (ofPerms (affineMove P H L 1)).lazy).walk ^ (2 * t)) f A -
+        𝔼 B, f B) ^ 4 ≤
+      2 * (1 - 1 / (155648 * H ^ 4)) ^ (2 * t) * 𝔼 A, (f A - 𝔼 B, f B) ^ 4 := by
+  have : Nonempty ({p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H) := ⟨.inr ⟨0, by omega⟩⟩
+  refine ((sliceGraph L hL y _).expect_walk_pow_two_mul_sub_expect_pow_four_le f t).trans ?_
+  refine two_mul_pow_le _ ?_ t _ (expect_nonneg fun _ _ ↦ by positivity)
+  rw [spectralExpansion_sliceGraph]
+  exact spectralExpansion_lazy_ofPerms_affineMove_le hH
+
+/-- **Fourth-moment conditional averaging over channels and free bits**: on the product of the
+retention slices of identifiers `y j` of `J` channels with free bits in `ZMod M ^ H`, `2 t` steps
+of the lazy product walk multiply the fourth central moment of every function by at most
+`2 (1 - 1 / (155648 (J + 1) H ^ 4)) ^ (2 t)`, for `H ≥ 3`, uniformly in the primes, the sides, the
+identifiers and the torus modulus. -/
+theorem expect_walk_pow_componentMove_sub_expect_pow_four_le {P L : Fin J → ℕ}
+    [∀ j, Fact (P j).Prime] [∀ j, NeZero (L j)] [NeZero M] (hH : 3 ≤ H) (hL : ∀ j, L j ≤ P j)
+    (y : ∀ j, ZMod (P j))
+    (f : (∀ j, RetentionSlice (P j) H 1 (L j) (y j)) × (Fin H → ZMod M) → ℝ) (t : ℕ) :
+    𝔼 A, ((((ofPerms (componentMove H M P L)).lazy.reindex
+        (componentEquiv M hL y).symm).walk ^ (2 * t)) f A - 𝔼 B, f B) ^ 4 ≤
+      2 * (1 - 1 / (155648 * (J + 1) * H ^ 4)) ^ (2 * t) * 𝔼 A, (f A - 𝔼 B, f B) ^ 4 := by
+  have : Nonempty ((Σ _ : Fin J, {p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H) ⊕
+      ({p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H)) := ⟨.inr (.inr ⟨0, by omega⟩)⟩
+  refine (RotationMap.expect_walk_pow_two_mul_sub_expect_pow_four_le _ f t).trans ?_
+  refine two_mul_pow_le _ ?_ t _ (expect_nonneg fun _ _ ↦ by positivity)
+  rw [spectralExpansion_reindex]
+  exact spectralExpansion_lazy_ofPerms_componentMove_le hH
+
+end Cslib.Probability

Complexity/Probability/PairwiseIndependentHash/ValidatedWords.lean

@@ -0,0 +1,171 @@
+/-
+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.Lazy
+public import Complexity.Probability.PairwiseIndependentHash.SliceGap
+
+/-!
+# Validated words of the lazy conditional walk
+
+The conditional walk on a retention slice moves channels by affine moves that refer to the
+identifier `y`. It is implemented by *validated variants* (`variantMove`), permutations of all
+channels that do not refer to `y`, filtered by a wrap test on the value `A.eval y`
+(`IsValidWrap`); for one step, the sum of the variants passing the test is the conditional move
+(`walk_sliceGraph_ofPerms_eq`). This module extends this to words of every length, for the lazy
+walk that the spectral-gap results use.
+
+The **validated step** (`validatedStep`) maps a function `g` of the channel to
+`A ↦ (g A + 𝔼 over generators and directions of ∑ over candidate wraps z of
+[the wrap z passes at A] g (variant_z A)) / 2`. By induction on `t`, `t` steps of the lazy walk on
+the slice, applied to a function of the channel, are the `t`-th iterate of the validated step,
+evaluated at the channel (`walk_pow_sliceGraph_lazy_ofPerms_eq`). Unfolding the iterate, this is
+the average over words of `t` moves (generators with directions, or stays) of the sum over words
+of `t` wraps of `f` at the end of the variant path, counted only when every wrap passes its test:
+exactly one word of wraps survives, and nothing is divided by the number of candidate wraps. For
+the affine generators (`affineGenerator`), every valid wrap lies in the fixed box
+`{-3, …, 3} ^ H`, independently of `P`, `L`, `y` and `t`
+(`walk_pow_sliceGraph_lazy_affineMove_eq`).
+
+This is Lemma 6.3 of the OpenAI preprint on derandomizing logarithmic space [OpenAI2026LogSpace],
+items 1–4, for length-`t` words of the lazy walk on one channel: the variants form a
+bounded-alphabet family described by `O(t)` symbols, independent of the identifiers, and the sum
+of the valid variants is the conditional walk.
+
+## Main definitions
+
+* `Cslib.Probability.validatedStep`: one step of the validated lazy walk on all channels.
+
+## Main results
+
+* `Cslib.Probability.walk_pow_sliceGraph_lazy_ofPerms_eq`: validated words of every length
+  compute the lazy conditional walk.
+* `Cslib.Probability.walk_pow_sliceGraph_lazy_affineMove_eq`: the same for the affine generators,
+  with the candidate wraps `{-3, …, 3} ^ H`.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace]
+-/
+
+public section
+
+namespace Cslib.Probability
+
+open Finset RotationMap
+open scoped BigOperators
+
+variable {P H r L : ℕ} [NeZero P] {K : Type*} [Fintype K]
+
+variable (L) in
+/-- **One step of the validated lazy walk** on all channels: with probability `1 / 2` stay, and
+otherwise pick a generator `σ k` and a direction, and sum the values at the variants whose wrap
+passes the test at the identifier `y`, over the candidate wraps `Z`. It refers to `y` only through
+the wrap test on the value `A.eval y`. -/
+@[expose] noncomputable def validatedStep
+    (σ : K → Matrix.SpecialLinearGroup (Fin H) ℤ × (Fin H → ℤ)) (Z : Finset (Fin H → ℤ))
+    (y : ZMod P) (g : FrameChannel P H r → ℝ) (A : FrameChannel P H r) : ℝ :=
+  (g A + 𝔼 kb : K × Bool, ∑ z ∈ Z,
+    (if IsValidWrap L (signedMove (σ kb.1) kb.2).1 (signedMove (σ kb.1) kb.2).2 z (A.eval y)
+      then g (variantMove L (signedMove (σ kb.1) kb.2).1 (signedMove (σ kb.1) kb.2).2 z A)
+      else 0)) / 2
+
+/-- **Validated words compute the conditional walk** (Lemma 6.3 for words of every length). For a
+family `σ` of affine generators and a candidate set `Z` containing every valid wrap, `t` steps of
+the lazy walk of their moves on the retention slice of `y`, applied to a function `f` of the
+channel, equal `t` iterations of the validated step, evaluated at the channel. Unfolding the
+iterations, this is the average over words of `t` generators and directions (or stays) of the sum,
+over words of wraps, of `f` at the end of the variant path, counted only when every wrap passes
+its test. -/
+theorem walk_pow_sliceGraph_lazy_ofPerms_eq [Nonempty K] [NeZero L] (hL : L ≤ P) {y : ZMod P}
+    (σ : K → Matrix.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 → ℝ) (t : ℕ) (A : RetentionSlice P H r L y) :
+    ((sliceGraph L hL y (ofPerms fun k ↦ coordMove (σ k).1 (σ k).2).lazy).walk ^ t)
+        (fun B ↦ f B.1) A =
+      (validatedStep L σ Z y)^[t] f A.1 := by
+  induction t generalizing A with
+  | zero => rfl
+  | succ t ih =>
+    have hfun : ((sliceGraph L hL y (ofPerms fun k ↦ coordMove (σ k).1 (σ k).2).lazy).walk ^ t)
+        (fun B ↦ f B.1) = fun B ↦ (validatedStep L σ Z y)^[t] f B.1 := funext ih
+    rw [pow_succ', Module.End.mul_apply, hfun, Function.iterate_succ_apply']
+    set h := (validatedStep L σ Z y)^[t] f
+    have hstep := walk_sliceGraph_ofPerms_eq hL σ hZ h A
+    simp only [sliceGraph, walk_reindex] at hstep ⊢
+    rw [walk_lazy_apply, hstep, validatedStep]
+    simp only [Function.comp_apply, Equiv.symm_symm, Equiv.symm_apply_apply]
+
+
+/-- The row sums of absolute values of a transvection `1 + c E_ab` are at most `1 + |c|`. -/
+private theorem sum_abs_transvection_le {a b : Fin H} (h : a ≠ b) (c : ℤ) (i : Fin H) :
+    ∑ j, |(Matrix.SpecialLinearGroup.transvection h c : Matrix (Fin H) (Fin H) ℤ) i j| ≤
+      1 + |c| := by
+  calc _ ≤ ∑ j, ((if i = j then 1 else 0) + (if j = b then |c| else 0)) := by
+        refine sum_le_sum fun j _ ↦ ?_
+        rw [Matrix.SpecialLinearGroup.transvection_coe]
+        simp only [Matrix.add_apply, Matrix.one_apply, Matrix.single_apply]
+        refine (abs_add_le _ _).trans (add_le_add (le_of_eq ?_) ?_)
+        · split_ifs <;> simp
+        · by_cases hij : a = i ∧ b = j
+          · obtain ⟨rfl, rfl⟩ := hij
+            simp
+          · simp only [hij, ite_false, abs_zero]
+            split_ifs <;> simp
+    _ = 1 + |c| := by simp [sum_add_distrib]
+
+/-- Every valid wrap of the affine generators and their inverses lies in `{-3, …, 3} ^ H`. -/
+private theorem wrap_affineGenerator_mem (k : {p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H) (b : Bool)
+    {w : Fin H → ZMod P} (hw : w ∈ retentionBox P H L) [NeZero L] :
+    wrap L (signedMove (affineGenerator H k) b).1 (signedMove (affineGenerator H k) b).2 w ∈
+      Fintype.piFinset fun _ ↦ Icc (-3 : ℤ) 3 := by
+  rw [Fintype.mem_piFinset]
+  intro i
+  rw [mem_Icc, ← abs_le]
+  refine (abs_wrap_le _ _ hw i).trans ?_
+  rcases k with p | j <;> cases b
+  · have := sum_abs_transvection_le p.2 1 i
+    simp only [signedMove, affineGenerator, Sum.elim_inl, Bool.cond_false, Pi.zero_apply, abs_zero,
+      add_zero]
+    norm_num at this
+    linarith
+  · have := sum_abs_transvection_le p.2 (-1) i
+    simp only [signedMove, affineGenerator, Sum.elim_inl, Bool.cond_true,
+      Matrix.SpecialLinearGroup.transvection_inv, Matrix.mulVec_zero, neg_zero, Pi.zero_apply,
+      abs_zero, add_zero]
+    norm_num at this
+    linarith
+  · simp only [signedMove, affineGenerator, Sum.elim_inr, Bool.cond_false,
+      Matrix.SpecialLinearGroup.coe_one, Matrix.one_apply]
+    have : |(Pi.single j 1 : Fin H → ℤ) i| ≤ 1 := by
+      rw [Pi.single_apply]
+      split_ifs <;> simp
+    simp only [apply_ite, abs_one, abs_zero, sum_ite_eq, mem_univ, ite_true]
+    linarith
+  · simp only [signedMove, affineGenerator, Sum.elim_inr, Bool.cond_true, inv_one,
+      Matrix.SpecialLinearGroup.coe_one, Matrix.one_apply, Matrix.one_mulVec, Pi.neg_apply,
+      abs_neg]
+    have : |(Pi.single j 1 : Fin H → ℤ) i| ≤ 1 := by
+      rw [Pi.single_apply]
+      split_ifs <;> simp
+    simp only [apply_ite, abs_one, abs_zero, sum_ite_eq, mem_univ, ite_true]
+    linarith
+
+/-- **Validated words of the affine walk**: `t` steps of the lazy affine walk on the retention slice
+of `y` equal `t` iterations of the validated step of the affine generators, with the candidate
+wraps `{-3, …, 3} ^ H`, a box independent of `P`, `L`, `y` and `t`. -/
+theorem walk_pow_sliceGraph_lazy_affineMove_eq [NeZero H] [NeZero L] (hL : L ≤ P) {y : ZMod P}
+    (f : FrameChannel P H r → ℝ) (t : ℕ) (A : RetentionSlice P H r L y) :
+    ((sliceGraph L hL y (ofPerms (affineMove P H L r)).lazy).walk ^ t) (fun B ↦ f B.1) A =
+      (validatedStep L (affineGenerator H) (Fintype.piFinset fun _ ↦ Icc (-3) 3) y)^[t] f A.1 := by
+  have : Nonempty ({p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H) := ⟨.inr 0⟩
+  exact walk_pow_sliceGraph_lazy_ofPerms_eq hL (affineGenerator H)
+    (fun k b _ hw ↦ wrap_affineGenerator_mem k b hw) f t A
+
+end Cslib.Probability

ComplexityTests/SliceMoments.lean

@@ -0,0 +1,70 @@
+/-
+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.SliceFourthMoment
+import Complexity.Probability.PairwiseIndependentHash.ValidatedWords
+
+/-!
+# Fourth moments and validated words on retention slices
+
+A concrete valid wrap of an inverse generator inside the box `{-3, …, 3} ^ H`, fourth-moment
+conditional averaging over two channels and free bits with every hypothesis discharged, and a
+client combining validated words with the `L²` gap: the validated estimator, computed without
+referring to the identifier except through the wrap tests, concentrates at the conditional mean.
+-/
+
+namespace ComplexityTests.SliceMoments
+
+open Cslib Cslib.Probability Cslib.RotationMap Finset
+open scoped BigOperators
+
+-- The inverse of the translation by `e_0` maps the value `(0, 2)` to `(-1, 2)`; the valid wrap
+-- `1` brings it back to `(2, 2)` in the box `{0, 1, 2} ^ 2`.
+example : wrap 3 (signedMove (affineGenerator 2 (.inr 0)) true).1
+    (signedMove (affineGenerator 2 (.inr 0)) true).2 (![0, 2] : Fin 2 → ZMod 5) = ![1, 0] := by
+  decide
+example : IsValidWrap 3 (signedMove (affineGenerator 2 (.inr 0)) true).1
+    (signedMove (affineGenerator 2 (.inr 0)) true).2 ![1, 0] (![0, 2] : Fin 2 → ZMod 5) := by
+  decide
+
+instance (j : Fin 2) : Fact (![5, 7] j).Prime := by
+  fin_cases j
+  exacts [⟨Nat.prime_five⟩, ⟨by decide⟩]
+
+instance (j : Fin 2) : NeZero (![3, 4] j) := by
+  fin_cases j
+  exacts [⟨by norm_num⟩, ⟨by norm_num⟩]
+
+/-- **Fourth-moment conditional averaging over two channels and free bits, with every hypothesis
+discharged**: channels over `𝔽₅` and `𝔽₇` with sides `3` and `4` and free bits in `(ZMod 8) ^ 3`;
+`2 t` steps multiply the fourth central moment by at most `2 (1 - 1 / 37822464) ^ (2 t)`. -/
+example (y : ∀ j : Fin 2, ZMod (![5, 7] j))
+    (f : (∀ j, RetentionSlice (![5, 7] j) 3 1 (![3, 4] j) (y j)) × (Fin 3 → ZMod 8) → ℝ)
+    (t : ℕ) :
+    𝔼 A, ((((ofPerms (componentMove 3 8 ![5, 7] ![3, 4])).lazy.reindex
+        (componentEquiv 8 (fun j ↦ by fin_cases j <;> decide) y).symm).walk ^ (2 * t)) f A -
+          𝔼 B, f B) ^ 4 ≤ 2 * (1 - 1 / 37822464) ^ (2 * t) * 𝔼 A, (f A - 𝔼 B, f B) ^ 4 := by
+  have h := expect_walk_pow_componentMove_sub_expect_pow_four_le le_rfl
+    (fun j ↦ by fin_cases j <;> decide) y f t
+  norm_num at h ⊢
+  exact h
+
+/-- **The validated estimator concentrates**: for every prime `P`, side `L ≤ P` and identifier `y`,
+and every function `f` of the channel, `t` iterations of the validated step of the affine
+generators, evaluated on the retention slice of `y`, have variance at most
+`(1 - 1 / (155648 H ^ 4)) ^ (2 t)` times the conditional variance of `f`. -/
+example {P L H : ℕ} [Fact P.Prime] [NeZero L] [NeZero H] (hH : 3 ≤ H) (hL : L ≤ P) (y : ZMod P)
+    (f : FrameChannel P H 1 → ℝ) (t : ℕ) :
+    𝔼 A : RetentionSlice P H 1 L y,
+        ((validatedStep L (affineGenerator H) (Fintype.piFinset fun _ ↦ Icc (-3) 3) y)^[t] f A.1 -
+          𝔼 B : RetentionSlice P H 1 L y, f B.1) ^ 2 ≤
+      (1 - 1 / (155648 * H ^ 4)) ^ (2 * t) *
+        𝔼 A : RetentionSlice P H 1 L y, (f A.1 - 𝔼 B : RetentionSlice P H 1 L y, f B.1) ^ 2 := by
+  have h := expect_walk_pow_sliceGraph_affineMove_sub_expect_sq_le hH hL y (fun B ↦ f B.1) t
+  simp only [walk_pow_sliceGraph_lazy_affineMove_eq] at h
+  exact h
+
+end ComplexityTests.SliceMoments