Zig-zag expanders on every vertex count

An explicitly numbered base gives explicit numberings of every level of the zig-zag tower. For a requested size n ≥ 2, choose the first tower with at least n vertices. Its size is at most b*n, where b is the base size. Bounded-fiber contraction and laziness then give a graph on exactly Fin n, with degree and spectral gap independent of n. Sizes zero and one use loops.

The rotation is executable given the base and numbering. A uniform machine-time realization using complete rotation tables is certified in Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family. Its input vertex count is unary. The contraction increases the already large degree, so asymptotic constructibility, practical enumeration and time polynomial in the bit length of a vertex name are separate targets.

Main definitions

• Cslib.RotationMap.ZigzagTowerVertex.equivFin: recursive numbering from a numbered base.
• Cslib.RotationMap.zigzagTowerFamily: the contracted lazy tower on every Fin n.

Main results

• Cslib.RotationMap.zigzagTower_size_bounds: the selected tower has size between n and b*n.
• Cslib.RotationMap.spectralExpansion_zigzagTowerFamily_le: the uniform spectral bound.

References

The underlying tower is the construction of O. Reingold, S. Vadhan, A. Wigderson, Entropy waves, the zig-zag graph product, and new constant-degree expanders, Section 1.2. The size adjustment uses bounded-fiber contraction.

def Cslib.RotationMap.ZigzagTowerVertex.equivFin {B : Type u_1} {b : ℕ} (numbering : B ≃ Fin b) (n : ℕ) : ZigzagTowerVertex B n ≃ Fin (b ^ (n + 1))

Number a tower vertex by recursively pairing the explicit base indices.

theorem Cslib.RotationMap.zigzagTower_size_bounds {b : ℕ} (hb : 1 < b) {n : ℕ} (hn : 2 ≤ n) : n ≤ b ^ (Nat.clog b n - 1 + 1) ∧ b ^ (Nat.clog b n - 1 + 1) ≤ b * n

The first tower size at least n is bounded by b*n, independently of its depth.

def Cslib.RotationMap.zigzagTowerFamily {B : Type u_1} {D : Type u_2} {b : ℕ} (H : RotationMap B D) (e : B ≃ (Fin 2 → D × D)) (numbering : B ≃ Fin b) (hb : 1 < b) (n : ℕ) : RotationMap (Fin n) (Fin b × D × D ⊕ Fin b × D × D)

A constant-degree graph on every vertex count, from a numbered zig-zag base.

theorem Cslib.RotationMap.spectralExpansion_zigzagTowerFamily_le {B : Type u_1} {D : Type u_2} {b : ℕ} [Fintype B] [Fintype D] [Nonempty D] (H : RotationMap B D) (e : B ≃ (Fin 2 → D × D)) (numbering : B ≃ Fin b) (hb : 1 < b) {c : ℝ} (hc : c ^ 2 + H.spectralExpansion + H.spectralExpansion ^ 2 ≤ c) (hc1 : c ≤ 1) (n : ℕ) : (H.zigzagTowerFamily e numbering hb n).spectralExpansion ≤ 1 - (1 - c) ^ 2 / (16 * ↑b ^ 2)

A tower with expansion at most c ≤ 1 gives expansion at most 1 - (1-c)²/(16*b²) on every vertex count after contraction and laziness.