Contraction through bounded vertex fibers

Represent the vertices of a graph by occupied slots in W × I, with an executable partial inverse. Contract each fiber to its vertex in W, moving the slot into the edge label. Empty slots carry self-loops. The new degree is |I| times the original degree, and no enumeration or choice is used by the rotation program.

When every fiber is inhabited, the contraction retains edge expansion. Applying the existing lazy Cheeger bound gives a spectral gap depending only on |I| and the original gap. This is the size-adjustment step needed when a constructive expander tower supplies only selected vertex counts. Quotient/remainder indexing also contracts Fin m to Fin n whenever n ≤ m ≤ k*n. Numbering the tower's vertices and certifying uniform efficiency remain separate.

Main definitions

• Cslib.RotationMap.contractDart: move the slot of a represented vertex into its edge label.
• Cslib.RotationMap.contractRot: the functional rotation program.
• Cslib.RotationMap.contract: contraction with self-loops in unoccupied slots.
• Cslib.RotationMap.finSlotEncode, Cslib.RotationMap.finSlotDecode: executable indexing.
• Cslib.RotationMap.contractFin: contraction of an indexed graph using those maps.

Main results

• Cslib.RotationMap.card_interedges_le_contract: original crossing darts survive contraction.
• Cslib.RotationMap.le_card_interedges_compl_contract: inhabited fibers retain edge expansion.
• Cslib.RotationMap.spectralExpansion_contract_lazy_le: laziness gives a spectral gap with loss depending only on the number of slots.
• Cslib.RotationMap.spectralExpansion_contractFin_lazy_le: the indexed specialization.

References

The spectral consequence uses the lazy Cheeger inequality from S. Hoory, N. Linial, A. Wigderson, Expander graphs and their applications.

def Cslib.RotationMap.contractDart {V : Type u_1} {W : Type u_2} {I : Type u_3} {D : Type u_4} (encode : V → W × I) (p : V × D) : W × I × D

Move the slot of a represented vertex into its edge label.

def Cslib.RotationMap.contractRot {V : Type u_1} {W : Type u_2} {I : Type u_3} {D : Type u_4} (encode : V → W × I) (decode : W × I → Option V) (rotate : V × D → V × D) (p : W × I × D) : W × I × D

Decode an occupied slot, rotate there, and encode the result; unused slots are self-loops.

theorem Cslib.RotationMap.contractRot_contractDart {V : Type u_1} {W : Type u_2} {I : Type u_3} {D : Type u_4} (encode : V → W × I) (decode : W × I → Option V) (h : Function.IsPartialInv encode decode) (rotate : V × D → V × D) (p : V × D) : contractRot encode decode rotate (contractDart encode p) = contractDart encode (rotate p)

An occupied dart executes the original rotation and retains both return labels.

def Cslib.RotationMap.contract {V : Type u_1} {W : Type u_2} {I : Type u_3} {D : Type u_4} (encode : V → W × I) (decode : W × I → Option V) (h : Function.IsPartialInv encode decode) (G : RotationMap V D) : RotationMap W (I × D)

Contract the occupied slots over each vertex, completing the degree with self-loops.

theorem Cslib.RotationMap.rot_contract {V : Type u_1} {W : Type u_2} {I : Type u_3} {D : Type u_4} (encode : V → W × I) (decode : W × I → Option V) (h : Function.IsPartialInv encode decode) (G : RotationMap V D) (p : W × I × D) : (contract encode decode h G).rot p = (decode (p.1, p.2.1)).elim p fun (v : V) => contractDart encode (G.rot (v, p.2.2))

The rotation map of contract encode decode h G decodes the slot, rotates in G, and re-encodes the resulting vertex, leaving an unoccupied slot as a self-loop.

@[simp]

theorem Cslib.RotationMap.rot_contract_contractDart {V : Type u_1} {W : Type u_2} {I : Type u_3} {D : Type u_4} (encode : V → W × I) (decode : W × I → Option V) (h : Function.IsPartialInv encode decode) (G : RotationMap V D) (p : V × D) : (contract encode decode h G).rot (contractDart encode p) = contractDart encode (G.rot p)

On an occupied slot contractDart encode p, the rotation map of contract encode decode h G rotates p in G and re-encodes the resulting dart.

theorem Cslib.RotationMap.neighbor_contract {V : Type u_1} {W : Type u_2} {I : Type u_3} {D : Type u_4} (encode : V → W × I) (decode : W × I → Option V) (h : Function.IsPartialInv encode decode) (G : RotationMap V D) (v : V) (d : D) : (contract encode decode h G).neighbor (encode v).1 ((encode v).2, d) = (encode (G.neighbor v d)).1

The neighbor of an occupied slot is the image of its original neighbor.

theorem Cslib.RotationMap.card_interedges_le_contract {V : Type u_1} {W : Type u_2} {I : Type u_3} {D : Type u_4} (encode : V → W × I) (decode : W × I → Option V) (h : Function.IsPartialInv encode decode) (G : RotationMap V D) [Fintype V] [Fintype I] [Fintype D] [DecidableEq V] [DecidableEq W] (S T : Finset W) : (G.interedges {v : V | (encode v).1 ∈ S} {v : V | (encode v).1 ∈ T}).card ≤ ((contract encode decode h G).interedges S T).card

Every original edge crossing between lifted sets gives a distinct edge of the contraction. The inequality also permits loops arising from unused slots when the two sets overlap.

theorem Cslib.RotationMap.le_card_interedges_compl_contract {V : Type u_1} {W : Type u_2} {I : Type u_3} {D : Type u_4} (encode : V → W × I) (decode : W × I → Option V) (h : Function.IsPartialInv encode decode) (G : RotationMap V D) [Fintype V] [Fintype I] [Fintype D] [DecidableEq W] [Fintype W] (hcover : Function.Surjective fun (v : V) => (encode v).1) {S : Finset W} (hS : 2 * S.card ≤ Fintype.card W) : (1 - G.spectralExpansion) * ↑(Fintype.card D) * ↑S.card / 2 ≤ ↑((contract encode decode h G).interedges S Sᶜ).card

If each new vertex has an original representative, contraction retains the original unnormalized edge-expansion lower bound.

theorem Cslib.RotationMap.spectralExpansion_contract_lazy_le {V : Type u_1} {W : Type u_2} {I : Type u_3} {D : Type u_4} (encode : V → W × I) (decode : W × I → Option V) (h : Function.IsPartialInv encode decode) (G : RotationMap V D) [Fintype V] [Fintype I] [Fintype D] [Fintype W] [Nontrivial W] [Nonempty I] [Nonempty D] (hcover : Function.Surjective fun (v : V) => (encode v).1) : (contract encode decode h G).lazy.spectralExpansion ≤ 1 - (1 - G.spectralExpansion) ^ 2 / (16 * ↑(Fintype.card I) ^ 2)

Contracting inhabited fibers with at most |I| slots and then making the walk lazy gives spectral expansion at most 1 - (1 - λ(G))² / (16 |I|²).

def Cslib.RotationMap.finSlotEncode {m n k : ℕ} (hcap : m ≤ k * n) (v : Fin m) : Fin n × Fin k

Place consecutive indices in columns of height n, using at most k slots per vertex.

def Cslib.RotationMap.finSlotDecode {m n k : ℕ} (p : Fin n × Fin k) : Option (Fin m)

Decode a column and slot, rejecting unused slots beyond the original vertex count.

theorem Cslib.RotationMap.isPartialInv_finSlots {m n k : ℕ} (hcap : m ≤ k * n) : Function.IsPartialInv (finSlotEncode hcap) finSlotDecode

Quotient/remainder indexing and a checked multiply/add are partial inverses.

def Cslib.RotationMap.contractFin {D : Type u_4} {m n k : ℕ} (G : RotationMap (Fin m) D) (hcap : m ≤ k * n) : RotationMap (Fin n) (Fin k × D)

Contract an indexed graph from m vertices to n vertices, using k slots per vertex.

theorem Cslib.RotationMap.spectralExpansion_contractFin_lazy_le {D : Type u_4} [Fintype D] {m n k : ℕ} [Nonempty D] (G : RotationMap (Fin m) D) (hcap : m ≤ k * n) (hsize : n ≤ m) (hn : 2 ≤ n) : (G.contractFin hcap).lazy.spectralExpansion ≤ 1 - (1 - G.spectralExpansion) ^ 2 / (16 * ↑k ^ 2)

An indexed graph with n ≤ m ≤ k*n contracts to n ≥ 2 vertices. After adding laziness, the gap bound depends on k, not on m or n, and is positive when the original gap is.