The zig-zag tower

One graph of constant size generates an infinite family. Square a member — the degree becomes the fourth power of the base's, exactly the number of the base's vertices — and zig-zag with the base: the vertex count is multiplied by that same number while the degree drops back to the base's squared.

The spectral bookkeeping is what makes the recursion close. If the base has bound lam ≤ 1/5 and a member has bound 2/5, squaring gives 4/25 and the zig-zag estimate λ(G ⓩ H) ≤ λ(G) + λ(H) + λ(H)² gives at most 4/25 + 1/5 + 1/25 = 2/5, the invariant again.

Only the base is non-constructive; the recursion itself is an algorithm, which is why this yields an expander family a machine can build.

Main definitions

• Complexity.ZigZagBase — a constant-size graph to build from
• Complexity.TowerStep — a member of the family, with its invariants
• Complexity.towerSucc — one round of squaring and zig-zagging

Main results

• Complexity.towerSucc carries the invariants forward, by construction
• Complexity.ZigZagBase.order_tower — the sizes are the powers of deg ^ 4

structure Complexity.ZigZagBase : Type 1

The seed of the tower: a graph whose vertices number the fourth power of its degree, with a spectral bound of at most a fifth.

• base : RegGraph

  The graph itself.

• card_eq : Fintype.card self.base.V = self.base.deg ^ 4

  Its vertices number the fourth power of its degree.

• lam : ℝ

  Its spectral bound.

• lam_nonneg : 0 ≤ self.lam

  The bound is nonnegative.

• lam_le : self.lam ≤ 1 / 5

  And at most a fifth, which is what makes the recursion close.

• spectral : self.base.SpectralBound self.lam

  The bound holds.

structure Complexity.ZigZagBase.TowerStep (B : ZigZagBase) : Type 1

A member of the family: its degree is the base's squared, and its spectral bound is two fifths.

• graph : RegGraph

  The graph.

• deg_eq : self.graph.deg = B.base.deg ^ 2

  Its degree is the base's squared.

• spec : self.graph.SpectralBound (2 / 5)

  Its spectral bound.

theorem Complexity.ZigZagBase.card_sq_eq (B : ZigZagBase) (T : B.TowerStep) : Fintype.card B.base.V = Fintype.card (T.graph.power 2).D

Squaring a member makes its degree match the base's vertex count.

noncomputable def Complexity.ZigZagBase.stepEquiv (B : ZigZagBase) (T : B.TowerStep) : B.base.V ≃ (T.graph.power 2).D

So the base's vertices name the squared member's darts.

Equations

• B.stepEquiv T = Fintype.equivOfCardEq ⋯

noncomputable def Complexity.ZigZagBase.towerSuccOf (B : ZigZagBase) (T : B.TowerStep) (e : B.base.V ≃ (T.graph.power 2).D) : B.TowerStep

One round of the tower, against a chosen naming of the base's vertices by the squared member's darts. The tower itself takes the arbitrary naming stepEquiv; an explicitly encoded tower supplies its own.

Equations

• B.towerSuccOf T e = { graph := (T.graph.power 2).zigzag B.base e, deg_eq := ⋯, spec := ⋯ }

noncomputable def Complexity.ZigZagBase.towerSucc (B : ZigZagBase) (T : B.TowerStep) : B.TowerStep

One round of the tower.

Equations

• B.towerSucc T = B.towerSuccOf T (B.stepEquiv T)

@[simp]

theorem Complexity.ZigZagBase.graph_towerSucc (B : ZigZagBase) (T : B.TowerStep) : (B.towerSucc T).graph = (T.graph.power 2).zigzag B.base (B.stepEquiv T)

noncomputable def Complexity.ZigZagBase.towerZero (B : ZigZagBase) : B.TowerStep

The first member: the base, squared.

Equations

• B.towerZero = { graph := B.base.power 2, deg_eq := ⋯, spec := ⋯ }

noncomputable def Complexity.ZigZagBase.tower (B : ZigZagBase) : ℕ → B.TowerStep

The tower.

Equations

• B.tower 0 = B.towerZero
• B.tower k.succ = B.towerSucc (B.tower k)

theorem Complexity.ZigZagBase.deg_tower (B : ZigZagBase) (k : ℕ) : (B.tower k).graph.deg = B.base.deg ^ 2

theorem Complexity.ZigZagBase.spectral_tower (B : ZigZagBase) (k : ℕ) : (B.tower k).graph.SpectralBound (2 / 5)

theorem Complexity.ZigZagBase.order_tower (B : ZigZagBase) (k : ℕ) : (B.tower k).graph.order = (B.base.deg ^ 4) ^ (k + 1)

The sizes of the tower. Each round multiplies the vertex count by the base's vertex count, so the k-th member has (deg ^ 4) ^ (k + 1) vertices.

theorem Complexity.ZigZagBase.exists_order_ge (B : ZigZagBase) (hd : 1 < B.base.deg) (n : ℕ) : ∃ (k : ℕ), n ≤ (B.tower k).graph.order

The sizes grow, so every vertex count is eventually passed.