Tabulated rotations of the arbitrary-size arithmetic family

Build the selected tower's complete rotation table, contract through quotient/remainder slots, and add laziness. The total functional program agrees with the existing family on valid vertex names, including its return label. Polynomial machine certificates are supplied separately in Computability/Machines/Turing/MultiTape/Complexity/PolyTime/RotationMap/Family.

Main definitions

• Cslib.RotationMap.TowerTable.contract: contract the rows of a table to size vertices, with self-loops at unoccupied slots.
• Cslib.RotationMap.TowerTable.rotateFamily: the total program on every requested vertex count.
• Cslib.RotationMap.arithmeticExpanderRotate: the concrete arithmetic instance.

Main results

• Cslib.RotationMap.TowerTable.contract_eq: contracted table rotations agree with quotient/remainder contraction of the graph (contractFin).
• Cslib.RotationMap.TowerTable.rotateFamily_eq: exact rotation and return-label agreement.
• Cslib.RotationMap.arithmeticExpanderRotate_eq: the concrete instance realizes the same family.

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.

def Cslib.RotationMap.TowerTable.contract {D : Type} {b : ℕ} (hb : 0 < b) (table : TowerTable D) (size : ℕ) (p : ℕ × Fin b × D × D) : ℕ × Fin b × D × D

Contract occupied rows to slots over size vertices; unoccupied slots are self-loops.

def Cslib.RotationMap.TowerTable.rotateFamily {D : Type} {b : ℕ} (H : RotationMap (Fin b) D) (e : Fin b ≃ (Fin 2 → D × D)) (hb : 0 < b) (p : ℕ × ℕ × (Fin b × D × D ⊕ Fin b × D × D)) : ℕ × (Fin b × D × D ⊕ Fin b × D × D)

Rotate a requested arbitrary-size family member, with the vertex count supplied at runtime.

theorem Cslib.RotationMap.TowerTable.contract_eq {D : Type} {b m n : ℕ} (G : RotationMap (Fin m) (D × D)) (hb : 0 < b) (hcap : m ≤ b * n) (table : TowerTable D) (hlength : List.length table = m) (hlookup : ∀ (vertex : Fin m) (label : D × D), table.lookup (↑vertex) label = (↑(G.rot (vertex, label)).1, (G.rot (vertex, label)).2)) (vertex : Fin n) (label : Fin b × D × D) : contract hb table n (↑vertex, label) = (↑((G.contractFin hcap).rot (vertex, label)).1, ((G.contractFin hcap).rot (vertex, label)).2)

Contracted table rotations agree with quotient/remainder contraction of the graph.

theorem Cslib.RotationMap.TowerTable.rotateFamily_eq {D : Type} {b : ℕ} {B : Type u_1} (H : RotationMap B D) (e : B ≃ (Fin 2 → D × D)) (numbering : B ≃ Fin b) (hb : 1 < b) (size : ℕ) (vertex : Fin size) (label : Fin b × D × D ⊕ Fin b × D × D) : rotateFamily (H.reindex numbering) (numbering.symm.trans e) ⋯ (size, ↑vertex, label) = (↑((H.zigzagTowerFamily e numbering hb size).rot (vertex, label)).1, ((H.zigzagTowerFamily e numbering hb size).rot (vertex, label)).2)

The total rotation program realizes the existing arbitrary-size tower family.

def Cslib.RotationMap.arithmeticExpanderRotate (p : ℕ × ℕ × AffinePlaneFamilyLabel (ZMod 257) 257) : ℕ × AffinePlaneFamilyLabel (ZMod 257) 257

A total executable rotation program for the arithmetic expander family. The first runtime input is the unary vertex count; fixed edge labels retain their full return-port information.

theorem Cslib.RotationMap.arithmeticExpanderRotate_eq (size : ℕ) (vertex : Fin size) (label : AffinePlaneFamilyLabel (ZMod 257) 257) : arithmeticExpanderRotate (size, ↑vertex, label) = (↑((arithmeticExpander size).rot (vertex, label)).1, ((arithmeticExpander size).rot (vertex, label)).2)

The efficient program computes exactly the existing arithmetic expander rotation.