Cayley graphs of the Boolean cube

The Cayley graph of the cube ι → Bool with generators s₁, …, s_d joins each u to u + sⱼ along its j-th edge (Cslib.RotationMap.cubeCayley). Every bit string is its own negative, so this is an undirected d-regular multigraph and the rotation map is an involution.

Its walk operator multiplies the Fourier coefficient of each function at S by the bias of the generators at S (Cslib.RotationMap.fourierCoeff_walk_cubeCayley). The characters are therefore its eigenvectors, and by Plancherel's identity its spectral expansion is at most the bias of the generators: if the uniform distribution over the generators is ε-biased with ε ≥ 0, then λ(G) ≤ ε (Cslib.RotationMap.spectralExpansion_cubeCayley_le). The expander mixing lemma then counts the edges between two sets (Cslib.RotationMap.card_interedges_cubeCayley_le), again for ε ≥ 0. This is the mixing estimate (6.3) in the proof of [OpenAI2026ETH, Lemma 6.1], whose bipartite double cover has left vertex u joined by its j-th edge to right vertex u + sⱼ.

Main definitions

• Cslib.RotationMap.cubeCayley: the Cayley graph of the cube with given generators.

Main results

• Cslib.RotationMap.fourierCoeff_walk_cubeCayley: the walk is diagonal in the Fourier basis.
• Cslib.RotationMap.spectralExpansion_cubeCayley_le: small-bias generators give small spectral expansion.
• Cslib.RotationMap.card_interedges_cubeCayley_le: the edge count between two sets.

References

• OpenAI, The Exponential Time Hypothesis is False, §6.1
• R. O'Donnell, Analysis of Boolean Functions

def Cslib.RotationMap.cubeCayley {ι : Type u_1} {d : ℕ} (s : Fin d → ι → Bool) : RotationMap (ι → Bool) (Fin d)

The Cayley graph of the cube with generators s j: the j-th edge at u leads to u + s j, where it is also the j-th edge.

@[simp]

theorem Cslib.RotationMap.cubeCayley_neighbor {ι : Type u_1} {d : ℕ} (s : Fin d → ι → Bool) (u : ι → Bool) (j : Fin d) : (cubeCayley s).neighbor u j = u + s j

The j-th neighbor of u is u + s j.

theorem Cslib.RotationMap.fourierCoeff_walk_cubeCayley {ι : Type u_1} {d : ℕ} [Fintype ι] [DecidableEq ι] [NeZero d] (s : Fin d → ι → Bool) (f : (ι → Bool) → ℝ) (S : Finset ι) : BitString.fourierCoeff ((cubeCayley s).walk f) S = BitString.bias (PMF.map s (Probability.PMF.uniformOfFintype (Fin d))) S * BitString.fourierCoeff f S

The walk operator of a Cayley graph of the cube multiplies each Fourier coefficient by the bias of the generators.

theorem Cslib.RotationMap.spectralExpansion_cubeCayley_le {ι : Type u_1} {d : ℕ} [Fintype ι] [DecidableEq ι] [NeZero d] (s : Fin d → ι → Bool) {ε : ℝ} (hε : 0 ≤ ε) (hs : BitString.IsSmallBias ε (PMF.map s (Probability.PMF.uniformOfFintype (Fin d)))) : (cubeCayley s).spectralExpansion ≤ ε

Small-bias generators give small spectral expansion: if the uniform distribution over the generators is ε-biased, with ε ≥ 0, the spectral expansion of the Cayley graph is at most ε.

theorem Cslib.RotationMap.card_interedges_cubeCayley_le {ι : Type u_1} {d : ℕ} [Fintype ι] [DecidableEq ι] [NeZero d] (s : Fin d → ι → Bool) {ε : ℝ} (hε : 0 ≤ ε) (hs : BitString.IsSmallBias ε (PMF.map s (Probability.PMF.uniformOfFintype (Fin d)))) (U V : Finset (ι → Bool)) : ↑((cubeCayley s).interedges U V).card ≤ ↑d * ↑U.card * ↑V.card / 2 ^ Fintype.card ι + ε * ↑d * √(↑U.card * ↑V.card)

Edges between two sets of a small-bias Cayley graph (the mixing estimate (6.3) of [OAI26c]): if the generators are ε-biased, with ε ≥ 0, the number of edges from U to V is at most d |U| |V| / 2^|ι| + ε d √(|U| |V|).