Documentation

Complexitylib.Classes.PCP.Internal.FamilyFin

An expander of every size, numbered #

TowerFin gives an expander at the tower's own sizes; a constraint graph asks for one on exactly its own vertex count, and Dinur's degree reduction asks for one on every vertex degree. This module closes the gap — fold the first large enough member onto n vertices, then pad the degree with self-loops — keeping every naming explicit, so that the rotation map stays a formula in numbers.

Nothing is numbered by an arbitrary bijection: a slot and a dart are packed with finProdFinEquiv, and the padding with finSumFinEquiv. That is what lets famRotVal compute the family's rotation map on raw numerals, which is what an algorithm has to be handed.

Main definitions #

Complexity.FinBase.famGraph — the member on n vertices
Complexity.FinBase.toFamily — the family

Main results #

Complexity.FinBase.spectral_famGraph — its spectral bound, below one

The member folded onto `n` vertices #

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

The tower level used for n vertices: the first one at least twice as big.

Equations

F.fitLevel hd n = F.level hd (2 * n)

Instances For

theorem Complexity.FinBase.fitLevel_le (F : FinBase) (hd : 1 < F.deg) (n : ℕ) :

F.fitLevel hd n ≤ 2 * n

A fit's level is at most twice the size asked for, so the polynomial an algorithm needs to bound the search is linear.

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

Its size.

Equations

F.fitN hd n = F.size (F.fitLevel hd n)

Instances For

def Complexity.FinBase.fitD (F : FinBase) :

The degree of every tower member.

Equations

F.fitD = F.deg ^ 2

Instances For

theorem Complexity.FinBase.fitD_pos (F : FinBase) :

0 < F.fitD

theorem Complexity.FinBase.two_mul_le_fitN (F : FinBase) (hd : 1 < F.deg) (n : ℕ) :

2 * n ≤ F.fitN hd n

def Complexity.FinBase.widthBnd (F : FinBase) :

The width bound: the overshoot of the tower is at most 2 deg ^ 4.

Equations

F.widthBnd = 2 * F.deg ^ 4 + 1

Instances For

def Complexity.FinBase.famDeg (F : FinBase) :

The family's degree.

Equations

F.famDeg = F.widthBnd * F.fitD

Instances For

theorem Complexity.FinBase.famDeg_pos (F : FinBase) :

theorem Complexity.FinBase.fitN_le (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

F.fitN hd n ≤ 2 * F.deg ^ 4 * n

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

The width of the fold.

Equations

F.wid hd n = Complexity.RegGraph.mergeWidth (F.fitN hd n) n

Instances For

theorem Complexity.FinBase.three_le_wid (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

3 ≤ F.wid hd n

theorem Complexity.FinBase.wid_pos (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

0 < F.wid hd n

theorem Complexity.FinBase.wid_le (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

F.wid hd n ≤ F.widthBnd

theorem Complexity.FinBase.fitN_le_wid_mul (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

F.fitN hd n ≤ F.wid hd n * n

theorem Complexity.FinBase.wid_sub_one_mul_le (F : FinBase) (hd : 1 < F.deg) (n : ℕ) :

(F.wid hd n - 1) * n ≤ F.fitN hd n

theorem Complexity.FinBase.wid_mul_fitD_le (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

F.wid hd n * F.fitD ≤ F.famDeg

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

The tower member used for n, on its own numbers.

Equations

F.fitGraph hd n = F.graphAt (F.fitLevel hd n)

Instances For

@[simp]

theorem Complexity.FinBase.order_fitGraph (F : FinBase) (hd : 1 < F.deg) (n : ℕ) :

(F.fitGraph hd n).order = F.fitN hd n

@[simp]

theorem Complexity.FinBase.deg_fitGraph (F : FinBase) (hd : 1 < F.deg) (n : ℕ) :

(F.fitGraph hd n).deg = F.fitD

theorem Complexity.FinBase.spectral_fitGraph (F : FinBase) (hd : 1 < F.deg) (n : ℕ) :

(F.fitGraph hd n).SpectralBound (2 / 5)

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

Fin (F.fitN hd n) × Fin F.fitD → Fin (F.fitN hd n) × Fin F.fitD

Its rotation map, at the numeric type it lives on.

Equations

F.fitRot hd n = ↑(F.data (F.fitLevel hd n))

Instances For

theorem Complexity.FinBase.fitRot_involutive (F : FinBase) (hd : 1 < F.deg) (n : ℕ) :

Function.Involutive (F.fitRot hd n)

theorem Complexity.FinBase.base_fitRot (F : FinBase) (hd : 1 < F.deg) (n : ℕ) :

RegGraph.base ⋯ (F.fitRot hd n) ⋯ = F.fitGraph hd n

The fold, and the padding #

noncomputable def Complexity.FinBase.mergedG (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

The tower member folded onto exactly n vertices.

Equations

F.mergedG hd hn = Complexity.RegGraph.mergedN hn ⋯ ⋯ ⋯ (F.fitRot hd n) ⋯

Instances For

@[simp]

theorem Complexity.FinBase.order_mergedG (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

(F.mergedG hd hn).order = n

@[simp]

theorem Complexity.FinBase.deg_mergedG (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

(F.mergedG hd hn).deg = F.wid hd n * F.fitD

theorem Complexity.FinBase.spectral_mergedG (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

(F.mergedG hd hn).SpectralBound (4 / 5)

noncomputable def Complexity.FinBase.paddedG (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

The fold padded up to the family's uniform degree.

Equations

F.paddedG hd hn = (F.mergedG hd hn).padLoops (F.famDeg - F.wid hd n * F.fitD)

Instances For

@[simp]

theorem Complexity.FinBase.order_paddedG (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

(F.paddedG hd hn).order = n

@[simp]

theorem Complexity.FinBase.deg_paddedG (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

(F.paddedG hd hn).deg = F.famDeg

noncomputable def Complexity.FinBase.famLam (F : FinBase) :

The uniform contraction factor of the family.

Equations

F.famLam = √(1 - 27 / (25 * ↑F.widthBnd))

Instances For

theorem Complexity.FinBase.three_le_widthBnd (F : FinBase) :

3 ≤ F.widthBnd

theorem Complexity.FinBase.famLam_nonneg (F : FinBase) :

theorem Complexity.FinBase.famLam_lt_one (F : FinBase) :

theorem Complexity.FinBase.spectral_paddedG (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

(F.paddedG hd hn).SpectralBound F.famLam

Numbering the darts #

theorem Complexity.FinBase.wid_mul_fitD_add (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

F.wid hd n * F.fitD + (F.famDeg - F.wid hd n * F.fitD) = F.famDeg

noncomputable def Complexity.FinBase.famDartName (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

(F.paddedG hd hn).D ≃ Fin F.famDeg

The darts of the padded fold, numbered: a slot and a dart of the member are packed together, and the padding loops follow them.

Equations

F.famDartName hd hn = (finProdFinEquiv.sumCongr (Equiv.refl (Fin (F.famDeg - F.wid hd n * F.fitD)))).trans (finSumFinEquiv.trans (finCongr ⋯))

Instances For

noncomputable def Complexity.FinBase.famGraph (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

The member of the family on n vertices, for n positive.

Equations

F.famGraph hd hn = (F.paddedG hd hn).relabel (F.famDartName hd hn)

Instances For

theorem Complexity.FinBase.famGraph_V (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

(F.famGraph hd hn).V = Fin n

theorem Complexity.FinBase.famGraph_D (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

(F.famGraph hd hn).D = Fin F.famDeg

theorem Complexity.FinBase.spectral_famGraph (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

(F.famGraph hd hn).SpectralBound F.famLam

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

Fin n × Fin F.famDeg → Fin n × Fin F.famDeg

The family's rotation map.

Equations

F.famRot hd n = if hn : 0 < n then (F.famGraph hd hn).rot else id

Instances For

theorem Complexity.FinBase.famRot_involutive (F : FinBase) (hd : 1 < F.deg) (n : ℕ) :

Function.Involutive (F.famRot hd n)

theorem Complexity.FinBase.famRot_eq (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) :

F.famRot hd n = (F.famGraph hd hn).rot

theorem Complexity.FinBase.spectral_famRot (F : FinBase) (hd : 1 < F.deg) (n : ℕ) :

(RegGraph.ofRot F.famDeg ⋯ n (F.famRot hd n) ⋯).SpectralBound F.famLam

The rotation map, in numbers #

theorem Complexity.FinBase.val_famDartName_inl (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) (s : Fin (F.wid hd n)) (c : Fin F.fitD) :

↑((F.famDartName hd hn) (Sum.inl (s, c))) = ↑c + F.fitD * ↑s

theorem Complexity.FinBase.val_famDartName_inr (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) (j : Fin (F.famDeg - F.wid hd n * F.fitD)) :

↑((F.famDartName hd hn) (Sum.inr j)) = F.wid hd n * F.fitD + ↑j

theorem Complexity.FinBase.famDartName_symm_of_lt (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) (i : Fin F.famDeg) (h : ↑i < F.wid hd n * F.fitD) :

(F.famDartName hd hn).symm i = Sum.inl (⟨↑i / F.fitD, ⋯⟩, ⟨↑i % F.fitD, ⋯⟩)

theorem Complexity.FinBase.famDartName_symm_of_ge (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) (i : Fin F.famDeg) (h : F.wid hd n * F.fitD ≤ ↑i) :

(F.famDartName hd hn).symm i = Sum.inr ⟨↑i - F.wid hd n * F.fitD, ⋯⟩

noncomputable def Complexity.FinBase.famRotVal (F : FinBase) (hd : 1 < F.deg) (n : ℕ) (p : ℕ × ℕ) :

The family's rotation map, on raw numbers. A dart below wid * fitD splits into a slot and a dart of the tower member; the vertex it lifts to is v + slot * n, and the vertex it lands on is read modulo n, with the slot it landed in becoming part of the new dart. Every other dart is a self-loop.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Complexity.FinBase.famRotVal_eq (F : FinBase) (hd : 1 < F.deg) {n : ℕ} (hn : 0 < n) (v : Fin n) (i : Fin F.famDeg) :

F.famRotVal hd n (↑v, ↑i) = (↑(F.famRot hd n (v, i)).1, ↑(F.famRot hd n (v, i)).2)

The numbers compute the family's rotation map.

noncomputable def Complexity.FinBase.toFamily (F : FinBase) (hd : 1 < F.deg) :

The expander family the numbered tower generates: one member at every size, of a constant degree, all contracting by the same factor, and with every naming explicit.

Equations

F.toFamily hd = { degree := F.famDeg, degree_pos := ⋯, rot := F.famRot hd, rot_involutive := ⋯, lam := F.famLam, lam_nonneg := ⋯, lam_lt_one := ⋯, spectral := ⋯ }

Instances For

The family the algorithm uses #

noncomputable def Complexity.algBase :

A numbered base of degree above one, chosen once.

Equations

Complexity.algBase = Classical.choose Complexity.exists_finBase

Instances For

theorem Complexity.one_lt_algBase_deg :

1 < algBase.deg

noncomputable def Complexity.algFamily :

The explicit expander family: the tower over that base. Unlike randExpander it comes with rotation tables an algorithm can read.

Equations

Complexity.algFamily = Complexity.algBase.toFamily Complexity.one_lt_algBase_deg

Instances For