From 14714b9a71fd012a55ca5605a15655c7830736a0 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 23:27:56 +0000 Subject: [PATCH 1/4] feat(Probability): retention by pairwise independent hashing (#1444) A point is retained when its hash lies in a target set B. Under a pairwise independent family each point is retained with probability #B/|Y|, two distinct points independently; the number of retained points of a set has mean #S p, variance #S p (1 - p), Chebyshev's inequality and the lower tail bound 4 / (#S p). Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../PairwiseIndependentHash/Retention.lean | 207 ++++++++++++++++++ ComplexityTests/PairwiseRetention.lean | 54 +++++ references.bib | 10 + 4 files changed, 272 insertions(+) create mode 100644 Complexity/Probability/PairwiseIndependentHash/Retention.lean create mode 100644 ComplexityTests/PairwiseRetention.lean diff --git a/Complexity.lean b/Complexity.lean index f59b96f22..3bd2f256c 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2911,6 +2911,7 @@ public import Complexity.Probability.PMF.Uniform public import Complexity.Probability.PairwiseIndependent public import Complexity.Probability.PairwiseIndependentHash public import Complexity.Probability.PairwiseIndependentHash.Affine +public import Complexity.Probability.PairwiseIndependentHash.Retention public import Complexity.Probability.PairwiseIndependentHash.Shift public import Complexity.Probability.PairwiseIndependentHash.Toeplitz public import Complexity.Probability.PairwiseIndependentHash.Universal diff --git a/Complexity/Probability/PairwiseIndependentHash/Retention.lean b/Complexity/Probability/PairwiseIndependentHash/Retention.lean new file mode 100644 index 000000000..33feb4034 --- /dev/null +++ b/Complexity/Probability/PairwiseIndependentHash/Retention.lean @@ -0,0 +1,207 @@ +/- +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 +import Complexity.Foundations.Data.Finset.Expect +import Mathlib.Algebra.Order.BigOperators.Expect + +/-! +# Retention by pairwise independent hashing + +Fix a target set `B ⊆ Y` and a pairwise independent family `h i : X → Y`. A point `x` is +*retained* by the seed `i` when its hash `h i x` lies in `B`. Each point is then retained with +probability exactly `p = #B / |Y|`, and the retention events of two distinct points are +independent: both are retained with probability exactly `p ^ 2` +(`IsPairwiseIndependentHash.expect_boole_apply_mem_and_apply_mem`). This is sampling at rate `p` +with pairwise independence, the technique of Chor and Goldreich [ChorGoldreich1989] built on the +hash families of Carter and Wegman [CarterWegman1979], [WegmanCarter1981]. For polynomial or affine +hashing over a finite field with a box `B`, the rate `p` ranges over the ratios of box size to +field size. + +The number `N i = #{x ∈ S | h i x ∈ B}` of retained points of a finite set `S` therefore has mean +`#S p`, second factorial moment `#S (#S - 1) p ^ 2` and variance `#S p (1 - p)`, and Chebyshev's +inequality bounds its deviations. In particular fewer than half of the expected number of points +are retained with probability at most `4 / (#S p)`. For a single target, `B = {y}`, these are the +cell-size moments of `Complexity.Probability.PairwiseIndependentHash`. + +## Main results + +* `Cslib.Probability.IsPairwiseIndependentHash.expect_boole_apply_mem`, + `Cslib.Probability.IsPairwiseIndependentHash.dens_filter_apply_mem`: a point is retained with + probability `#B / |Y|`. +* `Cslib.Probability.IsPairwiseIndependentHash.expect_boole_apply_mem_and_apply_mem`, + `Cslib.Probability.IsPairwiseIndependentHash.dens_filter_apply_mem_and_apply_mem`: two distinct + points are retained independently. +* `Cslib.Probability.IsPairwiseIndependentHash.expect_card_filter_apply_mem`, + `Cslib.Probability.IsPairwiseIndependentHash.expect_card_filter_apply_mem_mul_sub_one`, + `Cslib.Probability.IsPairwiseIndependentHash.expect_card_filter_apply_mem_sub_sq`: the mean, + second factorial moment and variance of the number of retained points. +* `Cslib.Probability.IsPairwiseIndependentHash.dens_le_abs_card_filter_apply_mem_sub_le`: + Chebyshev's inequality for it. +* `Cslib.Probability.IsPairwiseIndependentHash.dens_two_mul_card_filter_apply_mem_lt_le`: fewer + than half of the expected number of points are retained with probability at most `4 / (#S p)`. + +## References + +* [B. Chor, O. Goldreich, *On the power of two-point based sampling*][ChorGoldreich1989] +* [J. L. Carter, M. N. Wegman, *Universal classes of hash functions*][CarterWegman1979] +* [M. N. Wegman, J. L. Carter, *New hash functions and their use in authentication and set + equality*][WegmanCarter1981] +-/ + +public section + +namespace Cslib.Probability.IsPairwiseIndependentHash + +open Finset +open scoped BigOperators + +variable {ι X Y 𝕜 : Type*} [Fintype ι] [Fintype Y] [DecidableEq Y] {h : ι → X → Y} + +/-- **Retention probability**: a point is retained, its hash lying in `B`, with probability +`#B / |Y|`. -/ +theorem expect_boole_apply_mem [Semifield 𝕜] [CharZero 𝕜] (hh : IsPairwiseIndependentHash h) + (x : X) (B : Finset Y) : + 𝔼 i, (if h i x ∈ B then 1 else 0 : 𝕜) = #B / Fintype.card Y := by + have hpt (i : ι) : (if h i x ∈ B then 1 else 0 : 𝕜) = ∑ y ∈ B, if h i x = y then 1 else 0 := + (sum_ite_eq B (h i x) fun _ ↦ (1 : 𝕜)).symm + simp only [hpt] + rw [expect_sum_comm] + simp only [Fintype.expect_boole, hh.dens_filter_apply_eq, NNRat.cast_inv, NNRat.cast_natCast, + sum_const, nsmul_eq_mul, div_eq_mul_inv] + +/-- **Retention probability**: a point is retained, its hash lying in `B`, with probability +`#B / |Y|`. -/ +theorem dens_filter_apply_mem (hh : IsPairwiseIndependentHash h) (x : X) (B : Finset Y) : + dens {i | h i x ∈ B} = #B / Fintype.card Y := by + have := hh.expect_boole_apply_mem (𝕜 := ℚ≥0) x B + rwa [Fintype.expect_boole, NNRat.cast_id] at this + +/-- **Pairwise independent retention**: two distinct points are retained by `B₁` and `B₂` with +probability `#B₁ / |Y| * (#B₂ / |Y|)`. -/ +theorem expect_boole_apply_mem_and_apply_mem [Semifield 𝕜] [CharZero 𝕜] + (hh : IsPairwiseIndependentHash h) {x₁ x₂ : X} (hx : x₁ ≠ x₂) (B₁ B₂ : Finset Y) : + 𝔼 i, (if h i x₁ ∈ B₁ ∧ h i x₂ ∈ B₂ then 1 else 0 : 𝕜) = + #B₁ / Fintype.card Y * (#B₂ / Fintype.card Y) := by + have hpt (i : ι) : (if h i x₁ ∈ B₁ ∧ h i x₂ ∈ B₂ then 1 else 0 : 𝕜) = + ∑ y₁ ∈ B₁, ∑ y₂ ∈ B₂, if h i x₁ = y₁ ∧ h i x₂ = y₂ then 1 else 0 := by + have e₂ : (if h i x₂ ∈ B₂ then 1 else 0 : 𝕜) = + ∑ y₂ ∈ B₂, if h i x₂ = y₂ then 1 else 0 := + (sum_ite_eq B₂ (h i x₂) fun _ ↦ (1 : 𝕜)).symm + rw [ite_and, ← sum_ite_eq B₁ (h i x₁) fun _ ↦ (if h i x₂ ∈ B₂ then 1 else 0 : 𝕜)] + refine sum_congr rfl fun y₁ _ ↦ ?_ + by_cases hy : h i x₁ = y₁ + · simp only [hy, true_and, ite_true] + exact e₂ + · simp [hy] + simp only [hpt] + rw [expect_sum_comm] + simp only [expect_sum_comm, Fintype.expect_boole, hh.dens_filter_apply_eq_and_apply_eq hx, + NNRat.cast_inv, NNRat.cast_pow, NNRat.cast_natCast, sum_const, nsmul_eq_mul] + ring + +/-- **Pairwise independent retention**: two distinct points are retained by `B₁` and `B₂` with +probability `#B₁ / |Y| * (#B₂ / |Y|)`. -/ +theorem dens_filter_apply_mem_and_apply_mem (hh : IsPairwiseIndependentHash h) {x₁ x₂ : X} + (hx : x₁ ≠ x₂) (B₁ B₂ : Finset Y) : + dens {i | h i x₁ ∈ B₁ ∧ h i x₂ ∈ B₂} = #B₁ / Fintype.card Y * (#B₂ / Fintype.card Y) := by + have := hh.expect_boole_apply_mem_and_apply_mem (𝕜 := ℚ≥0) hx B₁ B₂ + rwa [Fintype.expect_boole, NNRat.cast_id] at this + +/-- **The mean number of retained points** of `S` is `#S * (#B / |Y|)`. -/ +theorem expect_card_filter_apply_mem [Semifield 𝕜] [CharZero 𝕜] + (hh : IsPairwiseIndependentHash h) (S : Finset X) (B : Finset Y) : + 𝔼 i, (#{x ∈ S | h i x ∈ B} : 𝕜) = #S * (#B / Fintype.card Y) := by + simp only [card_filter, Nat.cast_sum, Nat.cast_ite, Nat.cast_one, Nat.cast_zero] + rw [expect_sum_comm] + simp only [hh.expect_boole_apply_mem, sum_const, nsmul_eq_mul] + +/-- **The second factorial moment of the number of retained points**: the number of ordered +pairs of distinct retained points of `S` has expectation `#S (#S - 1) (#B / |Y|) ^ 2`. -/ +theorem expect_card_filter_apply_mem_mul_sub_one [Field 𝕜] [CharZero 𝕜] + (hh : IsPairwiseIndependentHash h) (S : Finset X) (B : Finset Y) : + 𝔼 i, (#{x ∈ S | h i x ∈ B} : 𝕜) * (#{x ∈ S | h i x ∈ B} - 1) = + #S * (#S - 1) * (#B / Fintype.card Y) ^ 2 := by + classical + have hcount (i : ι) : (#{x ∈ S | h i x ∈ B} : 𝕜) * (#{x ∈ S | h i x ∈ B} - 1) = + ∑ q ∈ S.offDiag, if h i q.1 ∈ B ∧ h i q.2 ∈ B then 1 else 0 := by + have hoff : {x ∈ S | h i x ∈ B}.offDiag = {q ∈ S.offDiag | h i q.1 ∈ B ∧ h i q.2 ∈ B} := by + ext q + simp only [mem_offDiag, mem_filter] + tauto + rw [sum_boole, ← hoff, offDiag_card, Nat.cast_sub (Nat.le_mul_self _), Nat.cast_mul] + ring + have hpair (q : X × X) (hq : q ∈ S.offDiag) : + 𝔼 i, (if h i q.1 ∈ B ∧ h i q.2 ∈ B then 1 else 0 : 𝕜) = (#B / Fintype.card Y) ^ 2 := by + rw [hh.expect_boole_apply_mem_and_apply_mem (mem_offDiag.1 hq).2.2, sq] + simp only [hcount] + rw [expect_sum_comm, sum_congr rfl hpair, sum_const, nsmul_eq_mul, offDiag_card, + Nat.cast_sub (Nat.le_mul_self _), Nat.cast_mul] + ring + +/-- **The variance of the number of retained points** is `#S p (1 - p)` with `p = #B / |Y|`. -/ +theorem expect_card_filter_apply_mem_sub_sq [Field 𝕜] [CharZero 𝕜] + (hh : IsPairwiseIndependentHash h) (S : Finset X) (B : Finset Y) : + 𝔼 i, ((#{x ∈ S | h i x ∈ B} : 𝕜) - #S * (#B / Fintype.card Y)) ^ 2 = + #S * (#B / Fintype.card Y) * (1 - #B / Fintype.card Y) := by + have hsq (i : ι) : ((#{x ∈ S | h i x ∈ B} : 𝕜) - #S * (#B / Fintype.card Y)) ^ 2 = + (#{x ∈ S | h i x ∈ B} : 𝕜) * (#{x ∈ S | h i x ∈ B} - 1) + + (1 - 2 * (#S * (#B / Fintype.card Y))) * #{x ∈ S | h i x ∈ B} + + (#S * (#B / Fintype.card Y)) ^ 2 := by + ring + rcases isEmpty_or_nonempty ι with hι | hι + · rcases S.eq_empty_or_nonempty with rfl | ⟨x, -⟩ + · simp + rcases B.eq_empty_or_nonempty with rfl | ⟨y, -⟩ + · simp + exact absurd (hh.nonempty x y) (not_nonempty_iff.2 hι) + simp only [hsq, expect_add_distrib, ← mul_expect, hh.expect_card_filter_apply_mem_mul_sub_one, + hh.expect_card_filter_apply_mem, Fintype.expect_const] + ring + +/-- **Chebyshev's inequality for the number of retained points**: it is at distance at least +`ε > 0` from its mean `#S p`, with `p = #B / |Y|`, with probability at most `#S p / ε²`. -/ +theorem dens_le_abs_card_filter_apply_mem_sub_le [Field 𝕜] [LinearOrder 𝕜] + [IsStrictOrderedRing 𝕜] (hh : IsPairwiseIndependentHash h) (S : Finset X) (B : Finset Y) + {ε : 𝕜} (hε : 0 < ε) : + (dens {i | ε ≤ |(#{x ∈ S | h i x ∈ B} : 𝕜) - #S * (#B / Fintype.card Y)|} : 𝕜) ≤ + #S * (#B / Fintype.card Y) / ε ^ 2 := by + have hmarkov := Fintype.mul_dens_filter_le_expect + (f := fun i ↦ ((#{x ∈ S | h i x ∈ B} : 𝕜) - #S * (#B / Fintype.card Y)) ^ 2) + (fun _ ↦ sq_nonneg _) (ε ^ 2) + simp only [sq_le_sq, abs_of_pos hε] at hmarkov + rw [le_div_iff₀ (by positivity), mul_comm] + refine hmarkov.trans ?_ + rw [hh.expect_card_filter_apply_mem_sub_sq] + have hp : (#B : 𝕜) / Fintype.card Y ≥ 0 := by positivity + exact mul_le_of_le_one_right (by positivity) (sub_le_self _ hp) + +/-- **Lower tail of the number of retained points**: fewer than half of the expected number +`#S p`, with `p = #B / |Y|`, are retained with probability at most `4 / (#S p)`. -/ +theorem dens_two_mul_card_filter_apply_mem_lt_le [Field 𝕜] [LinearOrder 𝕜] + [IsStrictOrderedRing 𝕜] (hh : IsPairwiseIndependentHash h) (S : Finset X) (B : Finset Y) + (hpos : 0 < (#S : 𝕜) * (#B / Fintype.card Y)) : + (dens {i | 2 * (#{x ∈ S | h i x ∈ B} : 𝕜) < #S * (#B / Fintype.card Y)} : 𝕜) ≤ + 4 / (#S * (#B / Fintype.card Y)) := by + set μ : 𝕜 := #S * (#B / Fintype.card Y) + have hsub : ({i | 2 * (#{x ∈ S | h i x ∈ B} : 𝕜) < μ} : Finset ι) ⊆ + ({i | μ / 2 ≤ |(#{x ∈ S | h i x ∈ B} : 𝕜) - μ|} : Finset ι) := by + intro i hi + simp only [mem_filter, mem_univ, true_and] at hi ⊢ + rw [abs_sub_comm, abs_of_pos (by linarith)] + linarith + calc (dens {i | 2 * (#{x ∈ S | h i x ∈ B} : 𝕜) < μ} : 𝕜) + ≤ (dens {i | μ / 2 ≤ |(#{x ∈ S | h i x ∈ B} : 𝕜) - μ|} : 𝕜) := by + exact_mod_cast dens_le_dens hsub + _ ≤ μ / (μ / 2) ^ 2 := hh.dens_le_abs_card_filter_apply_mem_sub_le S B (by positivity) + _ = 4 / μ := by + field_simp + ring + +end Cslib.Probability.IsPairwiseIndependentHash diff --git a/ComplexityTests/PairwiseRetention.lean b/ComplexityTests/PairwiseRetention.lean new file mode 100644 index 000000000..bb4a35fe5 --- /dev/null +++ b/ComplexityTests/PairwiseRetention.lean @@ -0,0 +1,54 @@ +/- +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.KWiseIndependent.Polynomial +import Complexity.Probability.PairwiseIndependentHash.Retention +import Mathlib.Algebra.Field.ZMod + +/-! +# Retention by polynomial hashing + +Polynomial hashing `x ↦ c₀ + c₁ x` over `𝔽₅`, retaining a point when its hash lies in the box +`{0, 1}`: a point is retained at rate `2 / 5`, as a direct count over the `25` seeds confirms; +two distinct points are retained jointly at rate `4 / 25`; and all five points have `2` retained +on average. +-/ + +namespace ComplexityTests.PairwiseRetention + +open Cslib Cslib.Probability Finset +open scoped BigOperators + +private instance : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩ + +private theorem hp : + IsPairwiseIndependentHash (polynomialHash : (Fin 2 → ZMod 5) → ZMod 5 → ZMod 5) := + (isKWiseIndependentHash_polynomialHash 2).isPairwiseIndependentHash le_rfl + +-- Each point is retained at rate `2 / 5`. +example (x : ZMod 5) : dens {c : Fin 2 → ZMod 5 | polynomialHash c x ∈ ({0, 1} : Finset _)} = + 2 / 5 := by + rw [hp.dens_filter_apply_mem, show #({0, 1} : Finset (ZMod 5)) = 2 by decide] + norm_num [ZMod.card] + +-- The same rate, counted directly: `10` of the `25` seeds retain the point `3`. +example : #{c : Fin 2 → ZMod 5 | polynomialHash c 3 ∈ ({0, 1} : Finset _)} = 10 := by decide + +-- Two distinct points are both retained at rate `4 / 25`. +example : dens {c : Fin 2 → ZMod 5 | + polynomialHash c 0 ∈ ({0, 1} : Finset _) ∧ polynomialHash c 1 ∈ ({0, 1} : Finset _)} = + 4 / 25 := by + rw [hp.dens_filter_apply_mem_and_apply_mem (by decide), + show #({0, 1} : Finset (ZMod 5)) = 2 by decide] + norm_num [ZMod.card] + +-- Of all five points, `2` are retained on average. +example : 𝔼 c : Fin 2 → ZMod 5, + (#{x ∈ (univ : Finset (ZMod 5)) | polynomialHash c x ∈ ({0, 1} : Finset _)} : ℚ) = 2 := by + rw [hp.expect_card_filter_apply_mem, show #({0, 1} : Finset (ZMod 5)) = 2 by decide] + norm_num [ZMod.card] + +end ComplexityTests.PairwiseRetention diff --git a/references.bib b/references.bib index ffd09ecfe..ec215b3f7 100644 --- a/references.bib +++ b/references.bib @@ -1050,6 +1050,16 @@ @article{ChorGoldreich1988 doi = {10.1137/0217015} } +@article{ChorGoldreich1989, + author = {Chor, Benny and Goldreich, Oded}, + title = {On the Power of Two-Point Based Sampling}, + journal = {Journal of Complexity}, + volume = {5}, + number = {1}, + pages = {96--106}, + year = {1989} +} + @article{ChungGrahamFranklShearer1986, author = {Chung, Fan R. K. and Graham, Ronald L. and Frankl, Peter and Shearer, James B.}, title = {Some Intersection Theorems for Ordered Sets and Graphs}, From 4943d9b0e91fa86788863e3fa7a211187d386748 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 23:57:30 +0000 Subject: [PATCH 2/4] feat(Probability): affine retention channels over a prime field (#1682) Identifiers y : ZMod P are retained when A y + b lies in the box {v | all coordinates < L} of ZMod P ^ H. Exact rates (L/P)^H and their squares for pairs, the lower tail 4/(#A pi), independence of separate seeds, and the assembled channel properties at rate f = a^H with L = ceil(P a): f <= pi <= 2^H f. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../RetentionChannel.lean | 212 ++++++++++++++++++ ComplexityTests/RetentionChannel.lean | 56 +++++ 3 files changed, 269 insertions(+) create mode 100644 Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean create mode 100644 ComplexityTests/RetentionChannel.lean diff --git a/Complexity.lean b/Complexity.lean index 3bd2f256c..957459612 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2912,6 +2912,7 @@ public import Complexity.Probability.PairwiseIndependent public import Complexity.Probability.PairwiseIndependentHash public import Complexity.Probability.PairwiseIndependentHash.Affine public import Complexity.Probability.PairwiseIndependentHash.Retention +public import Complexity.Probability.PairwiseIndependentHash.RetentionChannel public import Complexity.Probability.PairwiseIndependentHash.Shift public import Complexity.Probability.PairwiseIndependentHash.Toeplitz public import Complexity.Probability.PairwiseIndependentHash.Universal diff --git a/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean b/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean new file mode 100644 index 000000000..b890a5bad --- /dev/null +++ b/Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean @@ -0,0 +1,212 @@ +/- +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.Affine +public import Complexity.Probability.PairwiseIndependentHash.Retention +public import Mathlib.Algebra.Field.ZMod +public import Mathlib.Algebra.Order.Archimedean.Real.Basic +import Mathlib.Data.Fintype.BigOperators + +/-! +# Retention channels over a prime field + +A *retention channel* selects a random set of identifiers at a prescribed rate, with pairwise +independence. Its seed is an affine map `y ↦ A y + b` from `𝔽_P` to `𝔽_P ^ H`, with a uniformly +random matrix `A` and vector `b`. The identifier `y : ZMod P` is *retained* +(`affineRetains P H L s y`) when every coordinate of `A y + b`, read as a number in +`{0, …, P - 1}`, is less than `L`. The target is then the box `retentionBox P H L` with `L ^ H` +points (`card_retentionBox`). By the pairwise independence of affine hashing +(`isPairwiseIndependentHash_affineHash`) and the general retention bounds of +`Complexity.Probability.PairwiseIndependentHash.Retention`, every identifier is retained with +probability exactly `π = (L / P) ^ H`, and two distinct identifiers both with probability `π ^ 2`. +This is sampling by pairwise independent hashing [ChorGoldreich1989] with the hash families of +Carter and Wegman [CarterWegman1979]. + +For a target rate `f = a ^ H` with `1 ≤ P a` and `a ≤ 1`, the side `L = ⌈P a⌉` gives +`f ≤ π ≤ 2 ^ H f` (`affineRetains_rates`). Then the conditional probability that `w` is +retained, given that `y ≠ w` is retained, is at most `2 ^ H f`. A deterministic nonempty set `A` +retains fewer than `#A π / 2` of its identifiers with probability at most `4 / (#A π)`. Two +channels with independent seeds, on the product seed space, give independent events +(`dens_filter_fst_and_snd`). + +These are the channel properties used in Section 4 of the OpenAI preprint *Exact +Derandomization of Logarithmic Space* (2026, unrefereed): there, `c_π f ≤ π_f ≤ C_π f`, +`Pr[Y(w) | Y(y)] ≤ C_pair f`, the lower tail `Pr[∑_{x ∈ A} X(x) < |A| π / 2] ≤ C_var / (|A| π)`, +and the independence of the channels `X` and `Y`. Here the constants are `c_π = 1`, +`C_π = C_pair = 2 ^ H` and `C_var = 4`. The preprint conditions its channels on linearly +independent frames, which changes these constants only by a bounded factor. The frames matter +only for the later averaging walks, so they are not needed here. + +## Main definitions + +* `Cslib.Probability.retentionBox`: the box `{v | ∀ j, (v j).val < L}` in `ZMod P ^ H`. +* `Cslib.Probability.affineRetains`: the identifier `y` is retained by the affine seed `s`. + +## Main results + +* `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.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. +* `Cslib.Probability.affineRetains_rates`: the four channel properties at rate `f = a ^ H`. + +## References + +* [B. Chor, O. Goldreich, *On the power of two-point based sampling*][ChorGoldreich1989] +* [J. L. Carter, M. N. Wegman, *Universal classes of hash functions*][CarterWegman1979] +-/ + +public section + +namespace Cslib.Probability + +open Finset +open scoped BigOperators + +/-- **Independence of separate seeds**: on the product of two seed spaces, an event about the +first seed and an event about the second have probability equal to the product of their +probabilities. -/ +theorem dens_filter_fst_and_snd {ι κ : Type*} [Fintype ι] [Fintype κ] (p : ι → Prop) + (q : κ → Prop) [DecidablePred p] [DecidablePred q] : + dens {z : ι × κ | p z.1 ∧ q z.2} = dens {i | p i} * dens {j | q j} := by + rw [dens_eq_card_div_card, dens_eq_card_div_card, dens_eq_card_div_card, + ← univ_product_univ, filter_product, card_product, Fintype.card_prod] + push_cast + rw [mul_div_mul_comm] + +variable (P H L : ℕ) [NeZero P] + +/-- The **retention box** `{v | ∀ j, (v j).val < L}` in `ZMod P ^ H`: every coordinate, read as +a number in `{0, …, P - 1}`, is less than `L`. -/ +def retentionBox : Finset (Fin H → ZMod P) := + Fintype.piFinset fun _ ↦ {a : ZMod P | a.val < L} + +variable {P H L} + +/-- `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 + ext k + simp only [mem_image, mem_filter, mem_univ, true_and, mem_range] + refine ⟨fun ⟨a, ha, hak⟩ ↦ hak ▸ ha, fun hk ↦ ⟨k, ?_, ?_⟩⟩ <;> + rw [ZMod.val_cast_of_lt (by omega)] + exact hk + calc #({a : ZMod P | a.val < L} : Finset (ZMod P)) + = #(({a : ZMod P | a.val < L} : Finset (ZMod P)).image ZMod.val) := + (card_image_of_injective _ (ZMod.val_injective P)).symm + _ = L := by rw [himage, card_range] + +/-- The retention box has `L ^ H` points when `L ≤ P`. -/ +theorem card_retentionBox (hL : L ≤ P) : #(retentionBox P H L) = L ^ H := by + rw [retentionBox, Fintype.card_piFinset, prod_const, card_univ, Fintype.card_fin, + card_filter_val_lt hL] + +variable (P H L) + +/-- The identifier `y` is **retained** by the affine seed `s = (A, b)` when `A y + b` lies in the +retention box. -/ +abbrev affineRetains (s : Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P)) (y : ZMod P) : + Prop := + affineHash s (fun _ ↦ y) ∈ retentionBox P H L + +variable {P H L} [Fact P.Prime] + +/-- The affine hash of identifiers is pairwise independent. -/ +private theorem isPairwiseIndependentHash_affineIdentifier : + IsPairwiseIndependentHash fun (s : Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P)) + (y : ZMod P) ↦ affineHash s (fun _ ↦ y) := + isPairwiseIndependentHash_affineHash.comp (e := fun y _ ↦ y) fun _ _ h ↦ congrFun h 0 + +/-- **Retention probability**: every identifier is retained with probability `(L / P) ^ H`. -/ +theorem dens_affineRetains (hL : L ≤ P) (y : ZMod P) : + dens {s | affineRetains P H L s y} = ((L : ℚ≥0) / P) ^ H := by + have h := isPairwiseIndependentHash_affineIdentifier.dens_filter_apply_mem y + (retentionBox P H L) + rw [card_retentionBox hL, Fintype.card_fun, Fintype.card_fin, ZMod.card] at h + unfold affineRetains + rw [h, div_pow] + push_cast + rfl + +/-- **Pairwise independent retention**: two distinct identifiers are both retained with +probability `((L / P) ^ H) ^ 2`. -/ +theorem dens_affineRetains_and (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, Fintype.card_fun, Fintype.card_fin, ZMod.card] at h + unfold affineRetains + rw [h, 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)) + (hpos : 0 < (#A : ℝ) * ((L : ℝ) / P) ^ H) : + (dens {s | 2 * (#{y ∈ A | affineRetains P H L s y} : ℝ) < #A * ((L : ℝ) / P) ^ H} : ℝ) ≤ + 4 / (#A * ((L : ℝ) / P) ^ H) := by + have hrate : ((#(retentionBox P H L) : ℝ) / Fintype.card (Fin H → ZMod P)) = + ((L : ℝ) / P) ^ H := by + rw [card_retentionBox hL, Fintype.card_fun, Fintype.card_fin, ZMod.card, div_pow] + push_cast + rfl + have h := isPairwiseIndependentHash_affineIdentifier.dens_two_mul_card_filter_apply_mem_lt_le + (𝕜 := ℝ) A (retentionBox P H L) (by rwa [hrate]) + rw [hrate] at h + exact h + +/-- **The four channel properties at rate `f = a ^ H`.** Let `1 ≤ P a`, `a ≤ 1` and +`L = ⌈P a⌉`, and write `π = (L / P) ^ H` for the retention probability. Then `L ≤ P`, +`f ≤ π ≤ 2 ^ H f`, two distinct identifiers are both retained with probability at most +`2 ^ H f` times the probability that one of them is, and a nonempty set `A` retains fewer than +`#A π / 2` of its identifiers with probability at most `4 / (#A π)`. Independence of two channels +is `dens_filter_fst_and_snd`. -/ +theorem affineRetains_rates {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) : + let L := ⌈P * a⌉₊ + L ≤ P ∧ a ^ H ≤ ((L : ℝ) / P) ^ H ∧ ((L : ℝ) / P) ^ H ≤ 2 ^ H * a ^ H ∧ + (∀ w y : ZMod P, w ≠ y → + (dens {s | affineRetains P H L s w ∧ affineRetains P H L s y} : ℝ) ≤ + 2 ^ H * a ^ H * dens {s | affineRetains P H L s y}) ∧ + ∀ A : Finset (ZMod P), A.Nonempty → + (dens {s | 2 * (#{y ∈ A | affineRetains P H L s y} : ℝ) < #A * ((L : ℝ) / P) ^ H} : + ℝ) ≤ 4 / (#A * ((L : ℝ) / P) ^ H) := by + intro L + have hP : (0 : ℝ) < P := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne P) + have ha0 : 0 < a := by + by_contra h + have := mul_nonpos_of_nonneg_of_nonpos hP.le (not_lt.1 h) + linarith + have hLlo : (P : ℝ) * a ≤ L := Nat.le_ceil _ + have hLhi : (L : ℝ) ≤ 2 * (P * a) := by + have := Nat.ceil_lt_add_one (by positivity : (0 : ℝ) ≤ P * a) + linarith + have hLP : L ≤ P := Nat.ceil_le.2 (by nlinarith) + have hlo : a ≤ (L : ℝ) / P := by + rw [le_div_iff₀ hP] + linarith + have hhi : (L : ℝ) / P ≤ 2 * a := by + rw [div_le_iff₀ hP] + linarith + have hrate_hi : ((L : ℝ) / P) ^ H ≤ 2 ^ H * a ^ H := by + rw [← mul_pow] + exact pow_le_pow_left₀ (by positivity) hhi H + refine ⟨hLP, pow_le_pow_left₀ ha0.le hlo H, hrate_hi, fun w y hwy ↦ ?_, fun A hA ↦ ?_⟩ + · rw [dens_affineRetains_and hLP hwy, dens_affineRetains hLP] + push_cast + exact mul_le_mul_of_nonneg_right hrate_hi (by positivity) + · refine dens_two_mul_card_filter_affineRetains_lt_le hLP A ?_ + have : (0 : ℝ) < #A := by exact_mod_cast hA.card_pos + have : 0 < (L : ℝ) / P := ha0.trans_le hlo + positivity + +end Cslib.Probability diff --git a/ComplexityTests/RetentionChannel.lean b/ComplexityTests/RetentionChannel.lean new file mode 100644 index 000000000..9f278970a --- /dev/null +++ b/ComplexityTests/RetentionChannel.lean @@ -0,0 +1,56 @@ +/- +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.RetentionChannel + +/-! +# Retention channels over a prime field + +A retention channel over `𝔽₅` with one coordinate and side `2` retains each identifier at rate +`2 / 5`. A direct count over its `25` seeds confirms the rate. Two independent channels retain two +given identifiers jointly at rate `(2 / 5) ^ 2`. Over `𝔽₇` in two coordinates, at target rate +`f = (1 / 2) ^ 2`, the channel properties hold with side `L = ⌈7 / 2⌉ = 4`. +-/ + +namespace ComplexityTests.RetentionChannel + +open Cslib Cslib.Probability Finset + +private instance : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩ +private instance : Fact (Nat.Prime 7) := ⟨by decide⟩ + +-- The box `{0, 1}` in `𝔽₅`, and the exact retention rate `2 / 5`. +example : #(retentionBox 5 1 2) = 2 := card_retentionBox (by norm_num) + +example (y : ZMod 5) : dens {s | affineRetains 5 1 2 s y} = 2 / 5 := by + rw [dens_affineRetains (by norm_num)] + norm_num + +-- A direct count: `10` of the `25` seeds `(A, b)` retain the identifier `3`. +example : #{s | affineRetains 5 1 2 s 3} = 10 := by decide + +-- Two independent channels, on the product seed space, retain `3` in the first and `4` in the +-- second with probability `(2 / 5) * (2 / 5)`. +example : dens {z : (Matrix (Fin 1) (Fin 1) (ZMod 5) × (Fin 1 → ZMod 5)) × + (Matrix (Fin 1) (Fin 1) (ZMod 5) × (Fin 1 → ZMod 5)) | + affineRetains 5 1 2 z.1 3 ∧ affineRetains 5 1 2 z.2 4} = 4 / 25 := by + have h := dens_filter_fst_and_snd (fun s ↦ affineRetains 5 1 2 s 3) + (fun s ↦ affineRetains 5 1 2 s 4) + rw [dens_affineRetains (by norm_num), dens_affineRetains (by norm_num)] at h + convert h using 1 + norm_num + +-- At rate `f = (1 / 2) ^ 2` over `𝔽₇`, the side is `L = ⌈7 / 2⌉ = 4`, and the retention rate +-- `(4 / 7) ^ 2` lies within `[f, 4 f]`. +example : (1 / 2 : ℝ) ^ 2 ≤ ((4 : ℝ) / 7) ^ 2 ∧ ((4 : ℝ) / 7) ^ 2 ≤ 2 ^ 2 * (1 / 2 : ℝ) ^ 2 := by + obtain ⟨-, hlo, hhi, -, -⟩ := + affineRetains_rates (P := 7) (H := 2) (a := 1 / 2) (by norm_num) (by norm_num) + have hceil : ⌈((7 : ℕ) : ℝ) * (1 / 2)⌉₊ = 4 := by norm_num [Nat.ceil_eq_iff] + rw [hceil] at hlo hhi + push_cast at hlo hhi + exact ⟨hlo, hhi⟩ + +end ComplexityTests.RetentionChannel From 53de6a3f649ab48909a0733d9b7699608cffad88 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 00:33:24 +0000 Subject: [PATCH 3/4] feat(Probability): frame-conditioned channels, validated variants and conditional averaging (#1682) Frame-conditioned retention channels over ZMod P with their exact marginal rate, coordinates (F, w) on retention slices, the affine move (F, w) -> (gF, gw + c), validated walk variants with their unique wrap, and conditional variance decay on every slice from a spectral-gap hypothesis on the coordinates. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 2 + .../Combinatorics/Expander/Mixing.lean | 14 + .../ConditionalAveraging.lean | 336 ++++++++++++++++++ .../PairwiseIndependentHash/FrameChannel.lean | 231 ++++++++++++ .../RetentionChannel.lean | 6 + ComplexityTests/ConditionalAveraging.lean | 91 +++++ references.bib | 9 + 7 files changed, 689 insertions(+) create mode 100644 Complexity/Probability/PairwiseIndependentHash/ConditionalAveraging.lean create mode 100644 Complexity/Probability/PairwiseIndependentHash/FrameChannel.lean create mode 100644 ComplexityTests/ConditionalAveraging.lean diff --git a/Complexity.lean b/Complexity.lean index 957459612..a8eeb519d 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2911,6 +2911,8 @@ public import Complexity.Probability.PMF.Uniform public import Complexity.Probability.PairwiseIndependent public import Complexity.Probability.PairwiseIndependentHash public import Complexity.Probability.PairwiseIndependentHash.Affine +public import Complexity.Probability.PairwiseIndependentHash.ConditionalAveraging +public import Complexity.Probability.PairwiseIndependentHash.FrameChannel public import Complexity.Probability.PairwiseIndependentHash.Retention public import Complexity.Probability.PairwiseIndependentHash.RetentionChannel public import Complexity.Probability.PairwiseIndependentHash.Shift diff --git a/Complexity/Foundations/Combinatorics/Expander/Mixing.lean b/Complexity/Foundations/Combinatorics/Expander/Mixing.lean index f68a740af..dea30246e 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 000000000..04001ee81 --- /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 000000000..c42f9dad8 --- /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 b890a5bad..99d023615 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. @@ -91,6 +92,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 000000000..72e7b8b5c --- /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 diff --git a/references.bib b/references.bib index ec215b3f7..652d3cc22 100644 --- a/references.bib +++ b/references.bib @@ -3461,6 +3461,15 @@ @misc{OpenAI2026ETH url = {https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf} } +@misc{OpenAI2026LogSpace, + author = {{OpenAI}}, + title = {Exact Derandomization of Logarithmic Space: {L} = {RL} = {BPL}}, + year = {2026}, + howpublished = {Preprint}, + note = {Dated 23 September 2026, not peer reviewed; source revision 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a}, + url = {https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/preprints/Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026/paper.pdf} +} + @misc{OpenAI2026RationalHitting, author = {{OpenAI}}, title = {{Rational} matrix hitting lists for noncommutative rational formulas}, From b70b78ed7d8920d38318c0e4ffc04c4afc13c3df Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 02:35:25 +0000 Subject: [PATCH 4/4] feat(Probability): affine substitution invariance of frame-conditioned channels Lemma 3.1, item 4, of the OpenAI preprint: substituting alpha*y + beta (alpha != 0) into a frame-conditioned channel multiplies its coefficient columns by an invertible upper-triangular binomial matrix, so it permutes the frame-conditioned channels (FrameChannel.affineSubst, affineSubstEquiv), and the joint law of all evaluations of one or several independent channels is unchanged (dens_eval_comp_affine, dens_pi_eval_comp_affine). Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../FrameSubstitution.lean | 215 ++++++++++++++++++ ComplexityTests/FrameSubstitution.lean | 63 +++++ 3 files changed, 279 insertions(+) create mode 100644 Complexity/Probability/PairwiseIndependentHash/FrameSubstitution.lean create mode 100644 ComplexityTests/FrameSubstitution.lean diff --git a/Complexity.lean b/Complexity.lean index a8eeb519d..1c0c033b6 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2913,6 +2913,7 @@ public import Complexity.Probability.PairwiseIndependentHash public import Complexity.Probability.PairwiseIndependentHash.Affine public import Complexity.Probability.PairwiseIndependentHash.ConditionalAveraging public import Complexity.Probability.PairwiseIndependentHash.FrameChannel +public import Complexity.Probability.PairwiseIndependentHash.FrameSubstitution public import Complexity.Probability.PairwiseIndependentHash.Retention public import Complexity.Probability.PairwiseIndependentHash.RetentionChannel public import Complexity.Probability.PairwiseIndependentHash.Shift diff --git a/Complexity/Probability/PairwiseIndependentHash/FrameSubstitution.lean b/Complexity/Probability/PairwiseIndependentHash/FrameSubstitution.lean new file mode 100644 index 000000000..30f94d172 --- /dev/null +++ b/Complexity/Probability/PairwiseIndependentHash/FrameSubstitution.lean @@ -0,0 +1,215 @@ +/- +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.FrameChannel +import Mathlib.Data.Nat.Choose.Sum +import Mathlib.LinearAlgebra.Matrix.Block +import Mathlib.LinearAlgebra.Matrix.NonsingularInverse + +/-! +# Affine substitution invariance of frame-conditioned channels + +A frame-conditioned channel `A = (a₀, F)` (`Cslib.Probability.FrameChannel`) evaluates an +identifier `y` as the polynomial `a₀ + ∑ j, y ^ (j + 1) • F j`. Substituting `α y + β` for `y`, with +`α ≠ 0`, gives another polynomial of the same degree. Its constant column is +`a₀ + ∑ j, β ^ (j + 1) • F j`, and its coefficient columns are `B F`, where `B` is the +upper-triangular matrix of binomial coefficients with diagonal `α, α ^ 2, …, α ^ r`. Since `B` is +invertible, `B F` is again a frame, so the substitution is a map of frame-conditioned channels +(`FrameChannel.affineSubst`) with `(A.affineSubst β hα).eval y = A.eval (α * y + β)` +(`FrameChannel.eval_affineSubst`). The map is injective, hence a permutation of the finite +channel space (`FrameChannel.affineSubstEquiv`). So it preserves the uniform law. + +Consequently, replacing every identifier `y` by `α y + β` leaves the joint law of all evaluations +unchanged, for one channel (`dens_eval_comp_affine`) and for any finite family of independent +channels (`dens_pi_eval_comp_affine`). This is item 4 of Lemma 3.1 of the OpenAI preprint +[OpenAI2026LogSpace, Lemma 3.1 and its proof, pp. 9–10]. There it covers, in particular, a common +fixed padding suffix appended to all identifiers. + +## Main definitions + +* `Cslib.Probability.FrameChannel.affineSubst`: the channel obtained by substituting `α y + β`. +* `Cslib.Probability.FrameChannel.affineSubstEquiv`: the same map, as a permutation. + +## Main results + +* `Cslib.Probability.FrameChannel.eval_affineSubst`: its value at `y` is the value at `α y + β`. +* `Cslib.Probability.FrameChannel.affineSubst_injective`: substitution is injective. +* `Cslib.Probability.dens_eval_comp_affine`, `Cslib.Probability.dens_pi_eval_comp_affine`: the + substitution leaves the law of all evaluations unchanged. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Lemma 3.1 (preprint, not peer reviewed) +-/ + +public section + +namespace Cslib.Probability + +open Finset Matrix + +variable {P H r : ℕ} [Fact P.Prime] + +section SubstMatrix + +variable (α β : ZMod P) + +/-- The **substitution matrix** of `y ↦ α y + β`: its entry `(k, j)` is the coefficient of +`y ^ (k + 1)` in `(α y + β) ^ (j + 1)`, namely `C(j + 1, k + 1) α ^ (k + 1) β ^ (j - k)`. -/ +private def substMatrix : Matrix (Fin r) (Fin r) (ZMod P) := + Matrix.of fun k j ↦ ((j.val + 1).choose (k.val + 1) : ZMod P) * α ^ (k.val + 1) * + β ^ (j.val - k.val) + +private theorem substMatrix_apply (k j : Fin r) : + substMatrix α β k j = + ((j.val + 1).choose (k.val + 1) : ZMod P) * α ^ (k.val + 1) * β ^ (j.val - k.val) := + rfl + +private theorem substMatrix_isUpperTriangular : (substMatrix (r := r) α β).IsUpperTriangular := by + intro k j hjk + rw [substMatrix_apply, Nat.choose_eq_zero_of_lt (by simp only [id] at hjk; omega), + Nat.cast_zero, zero_mul, zero_mul] + +variable {α} in +/-- The substitution matrix is invertible: it is upper triangular with diagonal `α ^ (k + 1)`. -/ +private theorem isUnit_substMatrix (hα : α ≠ 0) : IsUnit (substMatrix (r := r) α β) := by + rw [isUnit_iff_isUnit_det, isUnit_iff_ne_zero, + (substMatrix_isUpperTriangular α β).det_ne_zero_iff] + intro k + simp [substMatrix_apply, hα] + +/-- The binomial expansion of `(α y + β) ^ (j + 1)` through the substitution matrix. -/ +private theorem pow_add_sum_substMatrix (j : Fin r) (y : ZMod P) : + β ^ (j.val + 1) + ∑ k : Fin r, y ^ (k.val + 1) * substMatrix α β k j = + (α * y + β) ^ (j.val + 1) := by + rw [add_pow, sum_range_succ', pow_zero, one_mul, Nat.sub_zero, Nat.choose_zero_right, + Nat.cast_one, mul_one, add_comm (β ^ (j.val + 1))] + congr 1 + simp only [substMatrix_apply] + rw [Fin.sum_univ_eq_sum_range (fun k ↦ y ^ (k + 1) * (((j.val + 1).choose (k + 1) : ZMod P) * + α ^ (k + 1) * β ^ (j.val - k)))] + refine (sum_subset (range_subset_range.2 (by omega : j.val + 1 ≤ r)) fun k _ hk ↦ ?_).symm.trans + (sum_congr rfl fun k _ ↦ ?_) + · rw [Nat.choose_eq_zero_of_lt (by simp only [mem_range] at hk; omega), Nat.cast_zero, + zero_mul, zero_mul, mul_zero] + · rw [Nat.add_sub_add_right, mul_pow] + ring + +/-- The coefficient columns after substituting `α y + β`: `F' k = ∑ j, B k j • F j`. -/ +private def substColumns (F : Fin r → Fin H → ZMod P) : Fin r → Fin H → ZMod P := + fun k ↦ ∑ j, substMatrix α β k j • F j + +/-- Substitution maps frames to frames, since the substitution matrix is invertible. -/ +private theorem linearIndependent_substColumns {α : ZMod P} (hα : α ≠ 0) + {F : Fin r → Fin H → ZMod P} (hF : LinearIndependent (ZMod P) F) : + LinearIndependent (ZMod P) (substColumns α β F) := by + rw [Fintype.linearIndependent_iff] at hF ⊢ + intro g hg + have hsum : ∑ j, (g ᵥ* substMatrix α β) j • F j = 0 := by + rw [← hg] + simp only [substColumns, smul_sum, smul_smul, vecMul, dotProduct, sum_smul] + exact sum_comm + have h0 : g ᵥ* substMatrix α β = 0 ᵥ* substMatrix α β := by + rw [zero_vecMul] + exact funext (hF _ hsum) + intro k + rw [vecMul_injective_iff_isUnit.2 (isUnit_substMatrix β hα) h0] + rfl + +end SubstMatrix + +namespace FrameChannel + +variable {α : ZMod P} (β : ZMod P) (hα : α ≠ 0) + +/-- The channel obtained by **substituting `α y + β`** into `A`, for `α ≠ 0`: its value at `y` is +the value of `A` at `α y + β` (`eval_affineSubst`). -/ +def affineSubst (A : FrameChannel P H r) : FrameChannel P H r := + (A.1 + ∑ j, β ^ (j.val + 1) • A.2.1 j, + ⟨substColumns α β A.2.1, linearIndependent_substColumns β hα A.2.2⟩) + +/-- **Substitution**: the substituted channel evaluates `y` as the original channel evaluates +`α y + β`. -/ +theorem eval_affineSubst (A : FrameChannel P H r) (y : ZMod P) : + (A.affineSubst β hα).eval y = A.eval (α * y + β) := by + simp only [FrameChannel.eval, affineSubst, substColumns] + simp_rw [← pow_add_sum_substMatrix α β, add_smul, sum_add_distrib, sum_smul, smul_sum, + smul_smul] + rw [sum_comm (s := univ) (t := univ) + (f := fun j k ↦ (y ^ (k.val + 1) * substMatrix α β k j) • A.2.1 j)] + abel + +/-- The substituted channel, as a function of the identifier. -/ +theorem eval_comp_affineSubst (A : FrameChannel P H r) : + (A.affineSubst β hα).eval = fun y ↦ A.eval (α * y + β) := + funext (eval_affineSubst β hα A) + +/-- Substitution is injective: the substitution matrix is invertible, so it recovers the frame, +and then the constant column. -/ +theorem affineSubst_injective : + Function.Injective (affineSubst (P := P) (H := H) (r := r) β hα) := by + intro A A' h + have hF : A.2.1 = A'.2.1 := by + have h2 := congrArg (fun A ↦ A.2.1) h + funext j i + have hi : substMatrix α β *ᵥ (fun j ↦ A.2.1 j i) = substMatrix α β *ᵥ (fun j ↦ A'.2.1 j i) := by + funext k + have := congrFun (congrFun h2 k) i + simpa [affineSubst, substColumns, mulVec, dotProduct, Finset.sum_apply] using this + exact congrFun (mulVec_injective_iff_isUnit.2 (isUnit_substMatrix β hα) hi) j + have h1 := congrArg Prod.fst h + simp only [affineSubst, hF] at h1 + exact Prod.ext (add_right_cancel h1) (Subtype.ext hF) + +/-- Substituting `α y + β`, for `α ≠ 0`, permutes the frame-conditioned channels. -/ +noncomputable def affineSubstEquiv : FrameChannel P H r ≃ FrameChannel P H r := + Equiv.ofBijective _ (Finite.injective_iff_bijective.1 (affineSubst_injective β hα)) + +theorem affineSubstEquiv_apply (A : FrameChannel P H r) : + affineSubstEquiv β hα A = A.affineSubst β hα := by + rw [affineSubstEquiv, Equiv.ofBijective_apply] + +end FrameChannel + +/-- Precomposing an event with a permutation of a finite uniform space keeps its probability. -/ +private theorem dens_filter_comp_equiv {ι : Type*} [Fintype ι] (e : ι ≃ ι) (p : ι → Prop) + [DecidablePred p] : dens {i | p (e i)} = dens {i | p i} := by + rw [dens_eq_card_div_card, dens_eq_card_div_card] + congr 2 + exact card_nbij' e e.symm (fun i hi ↦ by simpa using hi) (fun i hi ↦ by simpa using hi) + (fun i _ ↦ e.symm_apply_apply i) fun i _ ↦ e.apply_symm_apply i + +variable {α : ZMod P} (hα : α ≠ 0) (β : ZMod P) + +include hα in +/-- **Affine substitution invariance**: for `α ≠ 0`, the evaluations `y ↦ A.eval (α y + β)` of a +uniformly random frame-conditioned channel have the same law as the evaluations `y ↦ A.eval y` +[OpenAI2026LogSpace, Lemma 3.1, item 4]. -/ +theorem dens_eval_comp_affine (E : (ZMod P → Fin H → ZMod P) → Prop) [DecidablePred E] : + dens {A : FrameChannel P H r | E fun y ↦ A.eval (α * y + β)} = + dens {A : FrameChannel P H r | E A.eval} := by + rw [← dens_filter_comp_equiv (FrameChannel.affineSubstEquiv β hα) fun A ↦ E A.eval] + simp only [FrameChannel.affineSubstEquiv_apply, FrameChannel.eval_comp_affineSubst] + +include hα in +/-- **Affine substitution invariance for independent channels**: for `α ≠ 0`, replacing every +identifier `y` by `α y + β` in a finite family of independent uniformly random frame-conditioned +channels leaves the joint law of all their evaluations unchanged +[OpenAI2026LogSpace, Lemma 3.1, item 4]. -/ +theorem dens_pi_eval_comp_affine {ι : Type*} [Fintype ι] [DecidableEq ι] + (E : (ι → ZMod P → Fin H → ZMod P) → Prop) [DecidablePred E] : + dens {As : ι → FrameChannel P H r | E fun c y ↦ (As c).eval (α * y + β)} = + dens {As : ι → FrameChannel P H r | E fun c ↦ (As c).eval} := by + rw [← dens_filter_comp_equiv (Equiv.piCongrRight fun _ ↦ FrameChannel.affineSubstEquiv β hα) + fun As : ι → FrameChannel P H r ↦ E fun c ↦ (As c).eval] + simp only [Equiv.piCongrRight_apply, Pi.map_apply, FrameChannel.affineSubstEquiv_apply, + FrameChannel.eval_comp_affineSubst] + +end Cslib.Probability diff --git a/ComplexityTests/FrameSubstitution.lean b/ComplexityTests/FrameSubstitution.lean new file mode 100644 index 000000000..2a4d7bdf8 --- /dev/null +++ b/ComplexityTests/FrameSubstitution.lean @@ -0,0 +1,63 @@ +/- +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.FrameSubstitution +import Mathlib.Tactic.NormNum.Prime + +/-! +# Tests for affine substitution invariance of frame-conditioned channels + +Substituting `2 y + 1` over `𝔽₃` swaps the identifiers `0` and `1` and leaves the joint retention +law unchanged. The constant substitution `α = 0` changes that law, so `α ≠ 0` is needed. +-/ + +namespace ComplexityTests.FrameSubstitution + +open Finset Cslib.Probability + +private instance : Fact (Nat.Prime 3) := ⟨by norm_num⟩ +private instance : Fact (Nat.Prime 5) := ⟨by norm_num⟩ + +/-- The channel `y ↦ (1 + y, 2 + y ^ 2)` over `𝔽₅`, with the standard frame of length two. -/ +private def chan : FrameChannel 5 2 2 := + (![1, 2], ⟨![![1, 0], ![0, 1]], by + rw [Fintype.linearIndependent_iff] + intro g hg i + have h0 := congrFun hg 0 + have h1 := congrFun hg 1 + simp [Fin.sum_univ_two] at h0 h1 + fin_cases i <;> simpa⟩) + +-- The substituted channel evaluates `3` as `chan` evaluates `2 · 3 + 1 = 2`, namely `(3, 1)`. +example : (chan.affineSubst 1 (α := 2) (by decide)).eval 3 = ![3, 1] := by + rw [FrameChannel.eval_affineSubst] + decide + +/-- The event that both `0` and `1` lie in the retention box of side `2`. -/ +private abbrev Both (e : ZMod 3 → Fin 1 → ZMod 3) : Prop := + e 0 ∈ retentionBox 3 1 2 ∧ e 1 ∈ retentionBox 3 1 2 + +-- Substituting `2 y + 1` exchanges `0` and `1`; the law is unchanged, for frames of length two in +-- `𝔽₃ ^ 2` as for any other. +example (E : (ZMod 3 → Fin 2 → ZMod 3) → Prop) [DecidablePred E] : + dens {A : FrameChannel 3 2 2 | E fun y ↦ A.eval (2 * y + 1)} = + dens {A : FrameChannel 3 2 2 | E A.eval} := + dens_eval_comp_affine (by decide) 1 E + +-- The joint law of two independent channels is invariant too. +example (E : (Fin 2 → ZMod 3 → Fin 1 → ZMod 3) → Prop) [DecidablePred E] : + dens {As : Fin 2 → FrameChannel 3 1 1 | E fun c y ↦ (As c).eval (2 * y + 1)} = + dens {As : Fin 2 → FrameChannel 3 1 1 | E fun c ↦ (As c).eval} := + dens_pi_eval_comp_affine (by decide) 1 E + +-- Two of the six channels over `𝔽₃` retain both `0` and `1`, before and after substitution. +example : #{A : FrameChannel 3 1 1 | Both A.eval} = 2 := by decide +example : #{A : FrameChannel 3 1 1 | Both fun y ↦ A.eval (2 * y + 1)} = 2 := by decide + +-- With `α = 0` both identifiers become `1`, which four of the six channels retain: the +-- substitution `y ↦ 1` changes the law. +example : #{A : FrameChannel 3 1 1 | Both fun y ↦ A.eval (0 * y + 1)} = 4 := by decide + +end ComplexityTests.FrameSubstitution