Arithmetic expanders on every vertex count

The affine-plane base, recursive tower numbering, and bounded-fiber contraction give a computable rotation on exactly Fin n for every n. An explicit numbering of a field of size q ≥ 256 gives degree 2*q^12 and spectral expansion at most 1 - 9/(400*q^16).

arithmeticExpander instantiates the construction at ZMod 257, using its arithmetic equivalence with Fin 257. It performs no finite graph search or nonconstructive enumeration. The constants are enormous: executing one rotation and enumerating all edges are very different workloads. The uniform polynomial-time realization is certified in Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family; it constructs complete tables in time polynomial in the vertex count, rather than in its bit length.

Main definitions

• Cslib.RotationMap.affinePlaneTowerBaseNumbering: number the eight field coordinates.
• Cslib.RotationMap.AffinePlaneFamilyLabel: the fixed labels of the contracted lazy arithmetic tower.
• Cslib.RotationMap.affinePlaneFamily: contract the arithmetic tower to each requested size.
• Cslib.RotationMap.arithmeticExpander: the concrete family over ZMod 257.
• Cslib.RotationMap.arithmeticExpanderFamily: its interpretation on arbitrary finite types.

Main results

• Cslib.RotationMap.spectralExpansion_affinePlaneFamily_le: a uniform gap for numbered fields.
• Cslib.RotationMap.spectralExpansion_arithmeticExpander_le: the concrete spectral bound.

References

• O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders, Sections 1.2 and 5.1 for the tower and arithmetic base; the arbitrary-size contraction is supplied separately here.

def Cslib.RotationMap.affinePlaneTowerBaseNumbering {K : Type u_1} {q : ℕ} (numbering : K ≃ Fin q) : AffinePlaneTowerBaseVertex K ≃ Fin (q ^ 8)

Number eight field coordinates by pairing their explicit indices, without enumeration.

@[reducible, inline]

abbrev Cslib.RotationMap.AffinePlaneFamilyLabel (K : Type u_2) (q : ℕ) : Type u_2

The fixed label type of the contracted lazy arithmetic tower over a field with q elements.

def Cslib.RotationMap.affinePlaneFamily {K : Type u_1} {q : ℕ} [Field K] (numbering : K ≃ Fin q) (hq : 1 < q) (n : ℕ) : RotationMap (Fin n) (AffinePlaneFamilyLabel K q)

Use a numbered field as an arithmetic base, then contract the tower to the requested size.

theorem Cslib.RotationMap.card_affinePlaneFamilyLabel {K : Type u_1} {q : ℕ} [Fintype K] (numbering : K ≃ Fin q) : Fintype.card (AffinePlaneFamilyLabel K q) = 2 * q ^ 12

The arithmetic family has degree 2*q^12, independently of the requested vertex count.

theorem Cslib.RotationMap.spectralExpansion_affinePlaneFamily_le {K : Type u_1} {q : ℕ} [Field K] [Fintype K] (numbering : K ≃ Fin q) (hq : 256 ≤ q) (n : ℕ) : (affinePlaneFamily numbering ⋯ n).spectralExpansion ≤ 1 - 9 / (400 * ↑q ^ 16)

A numbered field with at least 256 elements yields a positive uniform spectral gap.

def Cslib.RotationMap.arithmeticExpander (n : ℕ) : RotationMap (Fin n) (AffinePlaneFamilyLabel (ZMod 257) 257)

A concrete arithmetic expander on exactly n vertices, with a fixed degree.

theorem Cslib.RotationMap.spectralExpansion_arithmeticExpander_le (n : ℕ) : (arithmeticExpander n).spectralExpansion ≤ 1 - 9 / (400 * 257 ^ 16)

The concrete family has a positive spectral gap independent of n.

theorem Cslib.RotationMap.spectralExpansion_arithmeticExpander_lt_one (n : ℕ) : (arithmeticExpander n).spectralExpansion < 1

Every member of the concrete family has positive spectral gap.

noncomputable def Cslib.RotationMap.arithmeticExpanderFamily : ExpanderFamily (AffinePlaneFamilyLabel (ZMod 257) 257) (1 - 9 / (400 * 257 ^ 16))

The arithmetic construction interpreted as an expander family on arbitrary finite types. The numbering chosen by this wrapper is noncomputable; arithmeticExpander itself is executable on Fin n, and an explicit equivalence allows executable transport to other representations.