A zig-zag tower with an arithmetic base

Tensor two affine-plane graphs, then zig-zag twice with the same affine-plane graph. This gives a graph on |K|⁸ vertices of degree |K|², with spectral expansion at most 3r + 2r², where r = sqrt (1 / |K|). For |K| ≥ 256 the bound is at most 1 / 5, as the existing zig-zag tower requires. All rotations are computed by field arithmetic and graph combinators, without search or a nonconstructive choice of a base graph. A concrete field is ZMod 257.

This is the affine-plane base construction of Reingold, Vadhan and Wigderson, Section 5.1, adapted to the simpler tower of their Section 1.2. It supplies particular vertex counts; AffineFamily contracts this tower to arbitrary sizes. Complete rotation tables have uniform polynomial-time certificates in Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Tower. Practically small degree and time polynomial in the bit length of a vertex name remain separate targets.

Main definitions

• Cslib.RotationMap.AffinePlaneTowerBaseVertex: the eight field coordinates of a vertex of the arithmetic base.
• Cslib.RotationMap.affinePlaneTowerBase: the arithmetic base on eight field coordinates.
• Cslib.RotationMap.affinePlaneTowerBaseEquiv: the regrouping of the base's coordinates into pairs of pairs of its edge labels.
• Cslib.RotationMap.affinePlaneTower: the tower built from it.

Main results

• Cslib.RotationMap.spectralExpansion_affinePlaneTowerBase_le_one_div_five: the base meets the tower's spectral hypothesis whenever |K| ≥ 256.
• Cslib.RotationMap.spectralExpansion_affinePlaneTower_le: every tower graph has expansion at most 2 / 5 under that same condition.

References

• O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders

@[reducible, inline]

abbrev Cslib.RotationMap.AffinePlaneTowerBaseVertex (K : Type u_1) : Type u_1

The eight coordinates of the arithmetic base, grouped as the graph products produce them.

def Cslib.RotationMap.affinePlaneTowerBase (K : Type u_1) [Field K] : RotationMap (AffinePlaneTowerBaseVertex K) (K × K)

Tensor two affine planes and zig-zag twice, giving degree |K|² on |K|⁸ vertices.

def Cslib.RotationMap.affinePlaneTowerBaseEquiv (K : Type u_1) : AffinePlaneTowerBaseVertex K ≃ (Fin 2 → (K × K) × K × K)

Regroup the base's coordinates into pairs of pairs of its edge labels.

def Cslib.RotationMap.affinePlaneTower (K : Type u_1) [Field K] (n : ℕ) : RotationMap (ZigzagTowerVertex (AffinePlaneTowerBaseVertex K) n) ((K × K) × K × K)

The ordinary zig-zag tower with an arithmetic base instead of a chosen expander.

theorem Cslib.RotationMap.spectralExpansion_affinePlaneTowerBase_le (K : Type u_1) [Field K] [Fintype K] : (affinePlaneTowerBase K).spectralExpansion ≤ 3 * √(1 / ↑(Fintype.card K)) + 2 * √(1 / ↑(Fintype.card K)) ^ 2

The base's expansion is at most 3r + 2r², where r = sqrt (1 / |K|).

theorem Cslib.RotationMap.spectralExpansion_affinePlaneTowerBase_le_one_div_five (K : Type u_1) [Field K] [Fintype K] (hK : 256 ≤ Fintype.card K) : (affinePlaneTowerBase K).spectralExpansion ≤ 1 / 5

A field with at least 256 elements gives a valid base for the existing zig-zag tower.

theorem Cslib.RotationMap.card_affinePlaneTowerVertex (K : Type u_1) [Fintype K] (n : ℕ) : Fintype.card (ZigzagTowerVertex (AffinePlaneTowerBaseVertex K) n) = Fintype.card K ^ (8 * (n + 1))

The (n + 1)-st arithmetic tower graph has |K|^(8(n + 1)) vertices.

theorem Cslib.RotationMap.spectralExpansion_affinePlaneTower_le (K : Type u_1) [Field K] [Fintype K] (hK : 256 ≤ Fintype.card K) (n : ℕ) : (affinePlaneTower K n).spectralExpansion ≤ 2 / 5

Every graph of the arithmetic tower has spectral expansion at most 2 / 5.