The zig-zag tower, numbered

ZigZagTower builds its members out of nested product types and names the base's vertices by an arbitrary bijection. That is enough for the mathematics, but an algorithm has to be handed numbers. This module rebuilds the tower with every vertex and dart numbered, and with each naming chosen explicitly: pairs are packed by finProdFinEquiv, so a level-k vertex is a mixed-radix numeral with k + 1 digits in base deg ^ 4.

The recursion carries its own involutivity proof, which is what lets the next level's types be Fin on the nose rather than up to a transport.

Main definitions

• Complexity.FinBase — a numbered zig-zag base
• Complexity.FinBase.data — the rotation map at each level, with its proof
• Complexity.FinBase.graphAt — the level's graph
• Complexity.FinBase.rotVal — the same rotation map on raw numbers

Main results

• Complexity.FinBase.graphAt_succ — one level is a zig-zag of the previous
• Complexity.FinBase.spectral_graphAt — every level has bound 2 / 5
• Complexity.FinBase.rotVal_eq — the numeric recursion computes it
• Complexity.nonempty_finBase — a numbered base exists

The recursion, in the open

theorem Complexity.RegGraph.rot_power_two (G : RegGraph) (v : G.V) (s : Fin 2 → G.D) : (G.power 2).rot (v, s) = ((G.rot ((G.rot (v, s 0)).1, s 1)).1, ![(G.rot ((G.rot (v, s 0)).1, s 1)).2, (G.rot (v, s 0)).2])

The rotation map of the square: walk two darts, and hand back the two return labels in the opposite order.

structure Complexity.FinBase : Type

A zig-zag base with its vertices and darts numbered: deg ^ 4 vertices, deg darts, and a spectral bound of a fifth.

• deg : ℕ

  The degree.

• deg_pos : 0 < self.deg

  The degree is positive.

• rot : Fin (self.deg ^ 4) × Fin self.deg → Fin (self.deg ^ 4) × Fin self.deg

  The rotation map.

• rot_involutive : Function.Involutive self.rot

  It is an involution.

• lam : ℝ

  The spectral bound.

• lam_nonneg : 0 ≤ self.lam

  It is nonnegative.

• lam_le : self.lam ≤ 1 / 5

  And at most a fifth.

• spectral : (RegGraph.ofRot self.deg ⋯ (self.deg ^ 4) self.rot ⋯).SpectralBound self.lam

  The bound holds.

def Complexity.FinBase.graph (F : FinBase) : RegGraph

The base graph.

Equations

• F.graph = Complexity.RegGraph.ofRot F.deg ⋯ (F.deg ^ 4) F.rot ⋯

@[simp]

theorem Complexity.FinBase.V_graph (F : FinBase) : F.graph.V = Fin (F.deg ^ 4)

@[simp]

theorem Complexity.FinBase.D_graph (F : FinBase) : F.graph.D = Fin F.deg

@[simp]

theorem Complexity.FinBase.deg_graph (F : FinBase) : F.graph.deg = F.deg

theorem Complexity.FinBase.sq_pos (F : FinBase) : 0 < F.deg ^ 2

def Complexity.FinBase.size (F : FinBase) (k : ℕ) : ℕ

The number of vertices at level k.

Equations

• F.size k = (F.deg ^ 4) ^ (k + 1)

theorem Complexity.FinBase.size_succ (F : FinBase) (k : ℕ) : F.size (k + 1) = F.size k * F.deg ^ 4

def Complexity.FinBase.toBase (F : FinBase) : ZigZagBase

The numbered base is a zig-zag base.

Equations

• F.toBase = { base := F.graph, card_eq := ⋯, lam := F.lam, lam_nonneg := ⋯, lam_le := ⋯, spectral := ⋯ }

The chosen namings

def Complexity.FinBase.dartName (F : FinBase) : Fin F.deg × Fin F.deg ≃ Fin (F.deg ^ 2)

Two darts of the base, as one dart of the level.

Equations

• F.dartName = finProdFinEquiv.trans (finCongr ⋯)

def Complexity.FinBase.baseName (F : FinBase) : Fin (F.deg ^ 4) ≃ (Fin 2 → Fin (F.deg ^ 2))

The base's vertices name the pairs of darts of a level.

Equations

• F.baseName = (finCongr ⋯).trans (finProdFinEquiv.symm.trans (finTwoArrowEquiv (Fin (F.deg ^ 2))).symm)

def Complexity.FinBase.vertName (F : FinBase) (k : ℕ) : Fin (F.size k) × (Fin 2 → Fin (F.deg ^ 2)) ≃ Fin (F.size (k + 1))

A level-k vertex together with a base vertex, as a level-(k+1) vertex.

Equations

• F.vertName k = ((Equiv.refl (Fin (F.size k))).prodCongr F.baseName.symm).trans (finProdFinEquiv.trans (finCongr ⋯))

def Complexity.FinBase.zeroDartName (F : FinBase) : (Fin 2 → Fin F.deg) ≃ Fin (F.deg ^ 2)

The two darts of the squared base, as one.

Equations

• F.zeroDartName = (finTwoArrowEquiv (Fin F.deg)).trans F.dartName

def Complexity.FinBase.zeroVertName (F : FinBase) : Fin (F.deg ^ 4) ≃ Fin (F.size 0)

The squared base's vertices, numbered as level zero's.

Equations

• F.zeroVertName = finCongr ⋯

The namings, in numbers

@[simp]

theorem Complexity.FinBase.val_dartName (F : FinBase) (a b : Fin F.deg) : ↑(F.dartName (a, b)) = ↑b + F.deg * ↑a

@[simp]

theorem Complexity.FinBase.val_dartName_symm_fst (F : FinBase) (i : Fin (F.deg ^ 2)) : ↑(F.dartName.symm i).1 = ↑i / F.deg

@[simp]

theorem Complexity.FinBase.val_dartName_symm_snd (F : FinBase) (i : Fin (F.deg ^ 2)) : ↑(F.dartName.symm i).2 = ↑i % F.deg

@[simp]

theorem Complexity.FinBase.val_baseName_zero (F : FinBase) (x : Fin (F.deg ^ 4)) : ↑(F.baseName x 0) = ↑x / F.deg ^ 2

@[simp]

theorem Complexity.FinBase.val_baseName_one (F : FinBase) (x : Fin (F.deg ^ 4)) : ↑(F.baseName x 1) = ↑x % F.deg ^ 2

@[simp]

theorem Complexity.FinBase.val_baseName_symm (F : FinBase) (s : Fin 2 → Fin (F.deg ^ 2)) : ↑(F.baseName.symm s) = ↑(s 1) + F.deg ^ 2 * ↑(s 0)

@[simp]

theorem Complexity.FinBase.val_vertName (F : FinBase) (k : ℕ) (u : Fin (F.size k)) (s : Fin 2 → Fin (F.deg ^ 2)) : ↑((F.vertName k) (u, s)) = ↑(F.baseName.symm s) + F.deg ^ 4 * ↑u

@[simp]

theorem Complexity.FinBase.val_vertName_symm_fst (F : FinBase) (k : ℕ) (v : Fin (F.size (k + 1))) : ↑((F.vertName k).symm v).1 = ↑v / F.deg ^ 4

@[simp]

theorem Complexity.FinBase.val_vertName_symm_snd_zero (F : FinBase) (k : ℕ) (v : Fin (F.size (k + 1))) : ↑(((F.vertName k).symm v).2 0) = ↑v % F.deg ^ 4 / F.deg ^ 2

@[simp]

theorem Complexity.FinBase.val_vertName_symm_snd_one (F : FinBase) (k : ℕ) (v : Fin (F.size (k + 1))) : ↑(((F.vertName k).symm v).2 1) = ↑v % F.deg ^ 4 % F.deg ^ 2

theorem Complexity.FinBase.val_baseName_symm_vertName_symm (F : FinBase) (k : ℕ) (v : Fin (F.size (k + 1))) : ↑(F.baseName.symm ((F.vertName k).symm v).2) = ↑v % F.deg ^ 4

@[simp]

theorem Complexity.FinBase.val_zeroVertName (F : FinBase) (x : Fin (F.deg ^ 4)) : ↑(F.zeroVertName x) = ↑x

@[simp]

theorem Complexity.FinBase.val_zeroVertName_symm (F : FinBase) (v : Fin (F.size 0)) : ↑(F.zeroVertName.symm v) = ↑v

@[simp]

theorem Complexity.FinBase.val_zeroDartName (F : FinBase) (s : Fin 2 → Fin F.deg) : ↑(F.zeroDartName s) = ↑(s 1) + F.deg * ↑(s 0)

@[simp]

theorem Complexity.FinBase.val_zeroDartName_symm_zero (F : FinBase) (i : Fin (F.deg ^ 2)) : ↑(F.zeroDartName.symm i 0) = ↑i / F.deg

@[simp]

theorem Complexity.FinBase.val_zeroDartName_symm_one (F : FinBase) (i : Fin (F.deg ^ 2)) : ↑(F.zeroDartName.symm i 1) = ↑i % F.deg

The tower

noncomputable def Complexity.FinBase.data (F : FinBase) (k : ℕ) : { f : Fin (F.size k) × Fin (F.deg ^ 2) → Fin (F.size k) × Fin (F.deg ^ 2) // Function.Involutive f }

The rotation map at each level, carrying its involutivity so that the next level's types are numbered on the nose.

Equations

• One or more equations did not get rendered due to their size.
• F.data 0 = ⟨(((F.graph.power 2).relabelV F.zeroVertName).relabel F.zeroDartName).rot, ⋯⟩

noncomputable def Complexity.FinBase.graphAt (F : FinBase) (k : ℕ) : RegGraph

The level-k graph.

Equations

• F.graphAt k = Complexity.RegGraph.ofRot (F.deg ^ 2) ⋯ (F.size k) ↑(F.data k) ⋯

@[simp]

theorem Complexity.FinBase.order_graphAt (F : FinBase) (k : ℕ) : (F.graphAt k).order = F.size k

@[simp]

theorem Complexity.FinBase.deg_graphAt (F : FinBase) (k : ℕ) : (F.graphAt k).deg = F.deg ^ 2

theorem Complexity.FinBase.graphAt_zero (F : FinBase) : F.graphAt 0 = ((F.graph.power 2).relabelV F.zeroVertName).relabel F.zeroDartName

theorem Complexity.FinBase.graphAt_succ (F : FinBase) (k : ℕ) : F.graphAt (k + 1) = ((((F.graphAt k).power 2).zigzag F.graph F.baseName).relabelV (F.vertName k)).relabel F.dartName

One level is the zig-zag of the previous with the base, renumbered.

theorem Complexity.FinBase.spectral_graphAt (F : FinBase) (k : ℕ) : (F.graphAt k).SpectralBound (2 / 5)

Every level has spectral bound 2 / 5.

theorem Complexity.FinBase.data_succ_apply (F : FinBase) (k : ℕ) (v : Fin (F.size (k + 1))) (i : Fin (F.deg ^ 2)) {us : Fin (F.size k) × (Fin 2 → Fin (F.deg ^ 2))} (hus : us = (F.vertName k).symm v) {ab : Fin F.deg × Fin F.deg} (hab : ab = F.dartName.symm i) {p : Fin (F.deg ^ 4) × Fin F.deg} (hp : p = F.rot (F.baseName.symm us.2, ab.1)) {q : Fin (F.size k) × (Fin 2 → Fin (F.deg ^ 2))} (hq : q = ((F.graphAt k).power 2).rot (us.1, F.baseName p.1)) {r : Fin (F.deg ^ 4) × Fin F.deg} (hr : r = F.rot (F.baseName.symm q.2, ab.2)) : ↑(F.data (k + 1)) (v, i) = ((F.vertName k) (q.1, F.baseName r.1), F.dartName (r.2, p.2))

One level of the recursion, in coordinates. A level-(k+1) vertex is a level-k vertex together with a base vertex, and a level-(k+1) dart is a pair of base darts; in those coordinates a step is: turn in the base, walk two darts of the level below, turn in the base again.

@[simp]

theorem Complexity.FinBase.rot_graphAt (F : FinBase) (k : ℕ) : (F.graphAt k).rot = ↑(F.data k)

theorem Complexity.FinBase.data_zero_apply (F : FinBase) (v : Fin (F.size 0)) (i : Fin (F.deg ^ 2)) {s : Fin 2 → Fin F.deg} (hs : s = F.zeroDartName.symm i) {p₀ : Fin (F.deg ^ 4) × Fin F.deg} (h0 : p₀ = F.rot (F.zeroVertName.symm v, s 0)) {p₁ : Fin (F.deg ^ 4) × Fin F.deg} (h1 : p₁ = F.rot (p₀.1, s 1)) : ↑(F.data 0) (v, i) = (F.zeroVertName p₁.1, F.zeroDartName ![p₁.2, p₀.2])

The bottom of the recursion, in coordinates. Level zero is the base squared: walk two base darts, and return the labels in the opposite order.

theorem Complexity.FinBase.data_succ_apply' (F : FinBase) (k : ℕ) (v : Fin (F.size (k + 1))) (i : Fin (F.deg ^ 2)) {us : Fin (F.size k) × (Fin 2 → Fin (F.deg ^ 2))} (hus : us = (F.vertName k).symm v) {ab : Fin F.deg × Fin F.deg} (hab : ab = F.dartName.symm i) {p : Fin (F.deg ^ 4) × Fin F.deg} (hp : p = F.rot (F.baseName.symm us.2, ab.1)) {q₀ : Fin (F.size k) × Fin (F.deg ^ 2)} (hq₀ : q₀ = ↑(F.data k) (us.1, F.baseName p.1 0)) {q₁ : Fin (F.size k) × Fin (F.deg ^ 2)} (hq₁ : q₁ = ↑(F.data k) (q₀.1, F.baseName p.1 1)) {r : Fin (F.deg ^ 4) × Fin F.deg} (hr : r = F.rot (F.baseName.symm ![q₁.2, q₀.2], ab.2)) : ↑(F.data (k + 1)) (v, i) = ((F.vertName k) (q₁.1, F.baseName r.1), F.dartName (r.2, p.2))

The step in full, with the two walks of the level below spelled out.

The recursion, in numbers

noncomputable def Complexity.FinBase.baseVal (F : FinBase) (x a : ℕ) : ℕ × ℕ

The base's rotation map, on raw numbers.

Equations

• F.baseVal x a = if h : x < F.deg ^ 4 ∧ a < F.deg then (↑(F.rot (⟨x, ⋯⟩, ⟨a, ⋯⟩)).1, ↑(F.rot (⟨x, ⋯⟩, ⟨a, ⋯⟩)).2) else (0, 0)

@[simp]

theorem Complexity.FinBase.baseVal_apply (F : FinBase) (x : Fin (F.deg ^ 4)) (a : Fin F.deg) : F.baseVal ↑x ↑a = (↑(F.rot (x, a)).1, ↑(F.rot (x, a)).2)

noncomputable def Complexity.FinBase.rotVal (F : FinBase) : ℕ → ℕ × ℕ → ℕ × ℕ

The tower's rotation map, on raw numbers. A level-(k+1) vertex v splits as v / deg^4 (the level below) and v % deg^4 (the base); a dart i splits as i / deg and i % deg. The step turns in the base, walks two darts of the level below, and turns in the base again.

Equations

• One or more equations did not get rendered due to their size.
• F.rotVal 0 (v, i) = ((F.baseVal (F.baseVal v (i / F.deg)).1 (i % F.deg)).1, (F.baseVal v (i / F.deg)).2 + F.deg * (F.baseVal (F.baseVal v (i / F.deg)).1 (i % F.deg)).2)

theorem Complexity.FinBase.rotVal_eq (F : FinBase) (k : ℕ) (v : Fin (F.size k)) (i : Fin (F.deg ^ 2)) : F.rotVal k (↑v, ↑i) = (↑(↑(F.data k) (v, i)).1, ↑(↑(F.data k) (v, i)).2)

The numbers compute the tower.

theorem Complexity.FinBase.baseVal_lt (F : FinBase) {x a : ℕ} (hx : x < F.deg ^ 4) (ha : a < F.deg) : (F.baseVal x a).1 < F.deg ^ 4 ∧ (F.baseVal x a).2 < F.deg

theorem Complexity.FinBase.rotVal_lt (F : FinBase) (k : ℕ) {v i : ℕ} (hv : v < F.size k) (hi : i < F.deg ^ 2) : (F.rotVal k (v, i)).1 < F.size k ∧ (F.rotVal k (v, i)).2 < F.deg ^ 2

Choosing a level

theorem Complexity.FinBase.one_lt_pow_four (F : FinBase) (hd : 1 < F.deg) : 1 < F.deg ^ 4

theorem Complexity.FinBase.exists_size_ge (F : FinBase) (hd : 1 < F.deg) (n : ℕ) : ∃ (k : ℕ), n ≤ F.size k

theorem Complexity.FinBase.le_size_self (F : FinBase) (hd : 1 < F.deg) (n : ℕ) : n ≤ F.size n

noncomputable def Complexity.FinBase.level (F : FinBase) (hd : 1 < F.deg) (n : ℕ) : ℕ

The first level large enough for a requested size.

Equations

• F.level hd n = Nat.find ⋯

theorem Complexity.FinBase.le_size_level (F : FinBase) (hd : 1 < F.deg) (n : ℕ) : n ≤ F.size (F.level hd n)

theorem Complexity.FinBase.level_le (F : FinBase) (hd : 1 < F.deg) (n : ℕ) : F.level hd n ≤ n

The level a size needs is at most that size.

theorem Complexity.FinBase.size_level_le (F : FinBase) (hd : 1 < F.deg) (n : ℕ) (hn : 1 ≤ n) : F.size (F.level hd n) ≤ F.deg ^ 4 * n

Numbering a base

theorem Complexity.ZigZagBase.card_base_darts (B : ZigZagBase) : Fintype.card B.base.D = B.base.deg

noncomputable def Complexity.ZigZagBase.toFin (B : ZigZagBase) : FinBase

A zig-zag base, numbered.

Equations

• B.toFin = { deg := B.base.deg, deg_pos := ⋯, rot := (B.base.toFinFormOf (B.base.deg ^ 4) B.base.deg ⋯ ⋯).rot, rot_involutive := ⋯, lam := B.lam, lam_nonneg := ⋯, lam_le := ⋯, spectral := ⋯ }

theorem Complexity.nonempty_finBase : Nonempty FinBase

A numbered base exists.

theorem Complexity.exists_finBase : ∃ (F : FinBase), 1 < F.deg

And one whose degree is above one, which is what folding a tower onto a requested size needs.