Def_6: Cycle-Sparsified Graph

Statement

Given a graph $G$ and a constant $c$ called the cycle-degree bound, a cycle-sparsification of $G$ is a new graph $\bar{\bar{G}}$ constructed as follows:

Layer structure: Build $R+1$ copies of $G$, labeled as layers $0, 1, 2, \ldots, R$. Layer 0 corresponds to the original graph $G$; layers $1, \ldots, R$ are copies on dummy vertices.

Inter-layer edges: Connect each vertex $v$ in layer $i$ to its copy in layer $i+1$ by an edge, for all $i = 0, \ldots, R-1$.

Cellulation edges: For each cycle in a chosen generating set of cycles for $G$, in exactly one layer, add edges that triangulate (cellulate) the cycle. The triangulation of a cycle $v_1 \to v_2 \to \cdots \to v_N \to v_1$ adds edges: $\{(v_1, v_{N-1}), (v_{N-1}, v_2), (v_2, v_{N-2}), (v_{N-2}, v_3), \ldots\}$ forming a sequence of triangles.

Cycle-degree constraint: The assignment of cycles to layers must ensure that in the resulting graph $\bar{\bar{G}}$, every edge participates in at most $c$ cycles from the chosen generating set.

Let $R_G^c$ denote the minimum number of layers required to achieve cycle-degree at most $c$. The Freedman-Hastings decongestion lemma establishes that $R_G^c = O(\log^2 |V_G|)$ for any constant-degree graph $G$.

Main Definitions

• LayeredVertex : Vertices in the layered graph (layer index × original vertex)
• CycleSparsification : The cycle-sparsified graph structure
• CycleLayerAssignment : Assignment of cycles to layers
• triangulationEdgePairs : The vertex pairs added to triangulate a cycle
• cycleDegree : The number of cycles containing an edge in the generating set

Key Properties

• layer_zero_adj_iff_original : Layer 0 is isomorphic to the original graph
• interLayerEdge_connects_copies : Each vertex connects to its copy in the next layer
• cycleDegConstraint : Every edge has cycle-degree at most c

Layered Vertex Type

structure LayeredVertex (V : Type u_1) (R : ℕ) : Type u_1

A vertex in the layered graph: a pair of (layer index, original vertex). Layer 0 contains the original vertices; layers 1, ..., R contain dummy copies.

• layer : Fin (R + 1)

  The layer index (0, 1, ..., R)

• vertex : V

  The original vertex that this is a copy of

theorem LayeredVertex.ext_iff {V : Type u_1} {R : ℕ} {x y : LayeredVertex V R} : x = y ↔ x.layer = y.layer ∧ x.vertex = y.vertex

theorem LayeredVertex.ext {V : Type u_1} {R : ℕ} {x y : LayeredVertex V R} (layer : x.layer = y.layer) (vertex : x.vertex = y.vertex) : x = y

def LayeredVertex.isOriginal {V : Type u_1} {R : ℕ} (lv : LayeredVertex V R) : Prop

Layer 0 vertices are the "original" vertices

Equations

• lv.isOriginal = (lv.layer = 0)

def LayeredVertex.isDummy {V : Type u_1} {R : ℕ} (lv : LayeredVertex V R) : Prop

Layers 1, ..., R contain "dummy" vertices

Equations

• lv.isDummy = (lv.layer ≠ 0)

instance LayeredVertex.instDecidableEq {V : Type u_1} {R : ℕ} [DecidableEq V] : DecidableEq (LayeredVertex V R)

Equations

• lv1.instDecidableEq lv2 = if h1 : lv1.layer = lv2.layer then if h2 : lv1.vertex = lv2.vertex then isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance LayeredVertex.instFintype {V : Type u_1} {R : ℕ} [Fintype V] : Fintype (LayeredVertex V R)

Equations

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

def LayeredVertex.ofOriginal {V : Type u_1} {R : ℕ} (v : V) : LayeredVertex V R

Embed a vertex from the original graph into layer 0

Equations

• LayeredVertex.ofOriginal v = { layer := 0, vertex := v }

def LayeredVertex.inLayer {V : Type u_1} {R : ℕ} (i : Fin (R + 1)) (v : V) : LayeredVertex V R

Embed a vertex into a specific layer

Equations

• LayeredVertex.inLayer i v = { layer := i, vertex := v }

@[simp]

theorem LayeredVertex.ofOriginal_layer {V : Type u_1} {R : ℕ} (v : V) : (ofOriginal v).layer = 0

@[simp]

theorem LayeredVertex.ofOriginal_vertex {V : Type u_1} {R : ℕ} (v : V) : (ofOriginal v).vertex = v

@[simp]

theorem LayeredVertex.inLayer_layer {V : Type u_1} {R : ℕ} (i : Fin (R + 1)) (v : V) : (inLayer i v).layer = i

@[simp]

theorem LayeredVertex.inLayer_vertex {V : Type u_1} {R : ℕ} (i : Fin (R + 1)) (v : V) : (inLayer i v).vertex = v

theorem LayeredVertex.original_or_dummy {V : Type u_1} {R : ℕ} (lv : LayeredVertex V R) : lv.isOriginal ∨ lv.isDummy

Every layered vertex is either original or dummy

@[simp]

theorem LayeredVertex.card_layeredVertex {V : Type u_1} {R : ℕ} [Fintype V] : Fintype.card (LayeredVertex V R) = (R + 1) * Fintype.card V

The cardinality of layered vertices: (R+1) * |V|

Triangulation of a Cycle

The triangulation of a cycle [v₁, v₂, ..., vₙ, v₁] adds edges that form triangles using a "zigzag" pattern that alternates between low and high indices: {(v₁, vₙ₋₁), (vₙ₋₁, v₂), (v₂, vₙ₋₂), (vₙ₋₂, v₃), ...}

This creates a sequence of triangles moving inward from both ends of the cycle. We represent cycles as lists of vertices and compute the triangulation edge pairs.

structure ZigzagState : Type

A state for building zigzag triangulation edges. low = current low index, high = current high index (exclusive), fromLow = true means next edge starts from low index

• low : ℕ
• high : ℕ
• fromLow : Bool

def zigzagStep {V : Type u_1} (cycleVerts : List V) (n : ℕ) (hn : n = cycleVerts.length) (s : ZigzagState) (hlow : s.low < n) (hhigh : s.high ≤ n) (hgap : s.low + 2 < s.high) : (V × V) × ZigzagState

One step of zigzag edge generation. Returns the edge and next state. Given list length n and current state, produces edge (src, dst) based on direction.

Equations

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

def triangulationEdgePairs {V : Type u_1} (cycleVerts : List V) : List (V × V)

Compute the zigzag triangulation edge pairs for a cycle. For a cycle [v₀, v₁, v₂, ..., vₙ₋₁] (0-indexed), we compute edges using the zigzag pattern specified in the paper: {(v₀, vₙ₋₂), (vₙ₋₂, v₁), (v₁, vₙ₋₃), (vₙ₋₃, v₂), ...}

This alternates: connect from low to high end, then high to next low, etc. For a cycle of length n ≥ 4, this produces n - 3 triangulation edges.

Equations

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

@[simp]

theorem triangulationEdgePairs_small {V : Type u_1} (cycleVerts : List V) (h : cycleVerts.length < 4) : triangulationEdgePairs cycleVerts = []

For cycles of length < 4, no triangulation edges are needed

Cycle-Layer Assignment

structure CycleLayerAssignment (C : Type u_1) (R : ℕ) : Type u_1

An assignment of cycles to layers. Each cycle is assigned to exactly one layer where its triangulation edges will be added.

• assign : C → Fin (R + 1)

  The layer assigned to each cycle

def CycleLayerAssignment.cyclesInLayer {C : Type u_1} {R : ℕ} [DecidableEq C] [Fintype C] (a : CycleLayerAssignment C R) (layer : Fin (R + 1)) : Finset C

The set of cycles assigned to a particular layer

Equations

• a.cyclesInLayer layer = {c : C | a.assign c = layer}

theorem CycleLayerAssignment.each_cycle_in_one_layer {C : Type u_1} {R : ℕ} [DecidableEq C] [Fintype C] (a : CycleLayerAssignment C R) (c : C) : ∃! layer : Fin (R + 1), c ∈ a.cyclesInLayer layer

Every cycle is assigned to exactly one layer

Cycle Degree

def cycleDegree {E : Type u_1} {C : Type u_2} [DecidableEq E] [DecidableEq C] [Fintype C] (cycles : C → Finset E) (e : E) : ℕ

The cycle degree of an edge e in a graph with cycles C is the number of cycles in the generating set that contain edge e.

Equations

• cycleDegree cycles e = {c : C | e ∈ cycles c}.card

def maxCycleDegree {E : Type u_1} {C : Type u_2} [DecidableEq E] [DecidableEq C] [Fintype E] [Fintype C] (cycles : C → Finset E) : ℕ

The maximum cycle degree over all edges

Equations

• maxCycleDegree cycles = Finset.univ.sup fun (e : E) => cycleDegree cycles e

@[simp]

theorem cycleDegree_empty {E : Type u_1} {C : Type u_2} [DecidableEq E] [DecidableEq C] [Fintype C] [IsEmpty C] (cycles : C → Finset E) (e : E) : cycleDegree cycles e = 0

theorem cycleDegree_le_card {E : Type u_1} {C : Type u_2} [DecidableEq E] [DecidableEq C] [Fintype C] (cycles : C → Finset E) (e : E) : cycleDegree cycles e ≤ Fintype.card C

Cycle-Sparsified Graph Structure

structure CycleSparsification (V : Type u_1) (E : Type u_2) (C : Type u_3) [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] : Type (max (max u_1 u_2) u_3)

A cycle-sparsification of a graph G with cycles. This structure captures the layered construction with inter-layer edges and cellulation (triangulation) edges.

The construction requires:

• A base graph G with a chosen generating set of cycles
• R+1 layers (layer 0 is original, layers 1..R are dummy copies)
• A cycle-degree bound c
• An assignment of each cycle to a layer for triangulation
• The constraint that every edge participates in at most c cycles

• baseGraph : GraphWithCycles V E C

  The original graph with its chosen cycles

• numLayers : ℕ

  The number of additional layers (total layers = R + 1)

• cycleDegBound : ℕ

  The cycle-degree bound c

• cycleAssignment : CycleLayerAssignment C self.numLayers

  Assignment of cycles to layers for triangulation

• cycleVertices : C → List V

  For each cycle, a list of vertices representing the cycle in order

• cycleDegConstraint (e : E) : cycleDegree self.baseGraph.cycles e ≤ self.cycleDegBound

  The cycle-degree constraint is satisfied: every edge participates in at most c cycles

@[reducible, inline]

abbrev CycleSparsification.SparsifiedVertex {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) : Type u_1

The vertex type of the sparsified graph

Equations

• S.SparsifiedVertex = LayeredVertex V S.numLayers

@[simp]

theorem CycleSparsification.card_sparsifiedVertex {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) : Fintype.card S.SparsifiedVertex = (S.numLayers + 1) * Fintype.card V

The number of vertices in the sparsified graph: (R+1) * |V|

def CycleSparsification.originalLayer {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) : Finset S.SparsifiedVertex

Layer 0 of the sparsified graph (the original vertices)

Equations

• S.originalLayer = {lv : S.SparsifiedVertex | lv.layer = 0}

def CycleSparsification.dummyLayers {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) : Finset S.SparsifiedVertex

Dummy layers 1, ..., R of the sparsified graph

Equations

• S.dummyLayers = {lv : S.SparsifiedVertex | lv.layer ≠ 0}

theorem CycleSparsification.vertex_partition {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) : S.originalLayer ∪ S.dummyLayers = Finset.univ

Partition: every vertex is in either the original layer or a dummy layer

theorem CycleSparsification.vertex_partition_disjoint {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) : Disjoint S.originalLayer S.dummyLayers

The partition is disjoint

Edge Types in the Sparsified Graph

def CycleSparsification.isIntraLayerEdge {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv₁ lv₂ : S.SparsifiedVertex) : Prop

Edge type 1: Intra-layer edges from the original graph G, copied to each layer. An edge (v, v') in layer i is a copy of edge (v, v') from the original graph.

Equations

• S.isIntraLayerEdge lv₁ lv₂ = (lv₁.layer = lv₂.layer ∧ S.baseGraph.graph.Adj lv₁.vertex lv₂.vertex)

def CycleSparsification.isInterLayerEdge {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv₁ lv₂ : S.SparsifiedVertex) : Prop

Edge type 2: Inter-layer edges connecting a vertex to its copy in the next layer. These form "vertical" connections between layers.

Equations

• S.isInterLayerEdge lv₁ lv₂ = (lv₁.vertex = lv₂.vertex ∧ (↑lv₁.layer + 1 = ↑lv₂.layer ∨ ↑lv₂.layer + 1 = ↑lv₁.layer))

def CycleSparsification.triangulationPairsForCycle {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (c : C) (layer : Fin (S.numLayers + 1)) : List (S.SparsifiedVertex × S.SparsifiedVertex)

The set of triangulation edge pairs for a cycle in a given layer

Equations

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

def CycleSparsification.isTriangulationEdge {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv₁ lv₂ : S.SparsifiedVertex) : Prop

Edge type 3: Triangulation (cellulation) edges added to triangulate cycles. A pair (lv₁, lv₂) is a triangulation edge if:

• They are in the same layer
• There exists a cycle c assigned to that layer
• (lv₁.vertex, lv₂.vertex) is in the triangulation of c

Equations

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

def CycleSparsification.sparsifiedAdj {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv₁ lv₂ : S.SparsifiedVertex) : Prop

Adjacency in the sparsified graph: union of all three edge types

Equations

• S.sparsifiedAdj lv₁ lv₂ = (lv₁ ≠ lv₂ ∧ (S.isIntraLayerEdge lv₁ lv₂ ∨ S.isInterLayerEdge lv₁ lv₂ ∨ S.isTriangulationEdge lv₁ lv₂))

theorem CycleSparsification.isIntraLayerEdge_symm {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv₁ lv₂ : S.SparsifiedVertex) : S.isIntraLayerEdge lv₁ lv₂ ↔ S.isIntraLayerEdge lv₂ lv₁

Intra-layer edges are symmetric

theorem CycleSparsification.isInterLayerEdge_symm {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv₁ lv₂ : S.SparsifiedVertex) : S.isInterLayerEdge lv₁ lv₂ ↔ S.isInterLayerEdge lv₂ lv₁

Inter-layer edges are symmetric

theorem CycleSparsification.isTriangulationEdge_symm {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv₁ lv₂ : S.SparsifiedVertex) : S.isTriangulationEdge lv₁ lv₂ ↔ S.isTriangulationEdge lv₂ lv₁

Triangulation edges are symmetric

theorem CycleSparsification.sparsifiedAdj_symm {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv₁ lv₂ : S.SparsifiedVertex) : S.sparsifiedAdj lv₁ lv₂ ↔ S.sparsifiedAdj lv₂ lv₁

Sparsified adjacency is symmetric

theorem CycleSparsification.sparsifiedAdj_irrefl {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv : S.SparsifiedVertex) : ¬S.sparsifiedAdj lv lv

Sparsified adjacency is irreflexive

The Sparsified Graph as a SimpleGraph

def CycleSparsification.toSimpleGraph {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) : SimpleGraph S.SparsifiedVertex

The cycle-sparsified graph as a SimpleGraph

Equations

• S.toSimpleGraph = { Adj := S.sparsifiedAdj, symm := ⋯, loopless := ⋯ }

theorem CycleSparsification.layer_zero_adj_iff_original {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (v w : V) : S.isIntraLayerEdge (LayeredVertex.ofOriginal v) (LayeredVertex.ofOriginal w) ↔ S.baseGraph.graph.Adj v w

Layer 0 is isomorphic to the original graph G (for intra-layer edges)

Inter-layer Edge Properties

theorem CycleSparsification.interLayerEdge_connects_copies {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (i : Fin (S.numLayers + 1)) (v : V) (h_succ : ↑i + 1 < S.numLayers + 1) : S.isInterLayerEdge (LayeredVertex.inLayer i v) (LayeredVertex.inLayer ⟨↑i + 1, h_succ⟩ v)

Each vertex in layer i is connected to its copy in layer i+1

theorem CycleSparsification.interLayerEdge_consecutive {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv₁ lv₂ : S.SparsifiedVertex) (h : S.isInterLayerEdge lv₁ lv₂) : ↑lv₁.layer + 1 = ↑lv₂.layer ∨ ↑lv₂.layer + 1 = ↑lv₁.layer

Inter-layer edges only connect consecutive layers

theorem CycleSparsification.interLayerEdge_same_vertex {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv₁ lv₂ : S.SparsifiedVertex) (h : S.isInterLayerEdge lv₁ lv₂) : lv₁.vertex = lv₂.vertex

Inter-layer edges connect the same underlying vertex

Triangulation Edge Properties

theorem CycleSparsification.triangulationEdge_same_layer {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv₁ lv₂ : S.SparsifiedVertex) (h : S.isTriangulationEdge lv₁ lv₂) : lv₁.layer = lv₂.layer

Triangulation edges are within the same layer

theorem CycleSparsification.triangulationEdge_from_cycle {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (lv₁ lv₂ : S.SparsifiedVertex) (h : S.isTriangulationEdge lv₁ lv₂) : ∃ (c : C), S.cycleAssignment.assign c = lv₁.layer

Triangulation edges come from some cycle assigned to that layer

def CycleSparsification.layerVertices {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (i : Fin (S.numLayers + 1)) : Finset S.SparsifiedVertex

Layer i vertices form a copy of V

Equations

• S.layerVertices i = {lv : S.SparsifiedVertex | lv.layer = i}

@[simp]

theorem CycleSparsification.card_layerVertices {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (i : Fin (S.numLayers + 1)) : (S.layerVertices i).card = Fintype.card V

Each layer has exactly |V| vertices

def CycleSparsification.embedOriginal {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) : V ↪ S.SparsifiedVertex

The embedding of the original graph into layer 0

Equations

• S.embedOriginal = { toFun := LayeredVertex.ofOriginal, inj' := ⋯ }

theorem CycleSparsification.embedOriginal_preserves_adj {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (S : CycleSparsification V E C) (v w : V) (h : S.baseGraph.graph.Adj v w) : S.isIntraLayerEdge (S.embedOriginal v) (S.embedOriginal w)

The embedding preserves adjacency from the original graph

Minimum Number of Layers

The minimum number of layers R_G^c is the smallest R such that there exists a valid cycle-layer assignment achieving cycle-degree at most c.

def hasValidAssignment {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (c R : ℕ) : Prop

Predicate: there exists a valid cycle-layer assignment with R layers such that every edge has cycle-degree at most c.

Equations

• hasValidAssignment G c R = ∃ (_assignment : CycleLayerAssignment C R), ∀ (e : E), cycleDegree G.cycles e ≤ c

theorem hasValidAssignment_exists {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (c : ℕ) (hc : ∀ (e : E), cycleDegree G.cycles e ≤ c) : ∃ (R : ℕ), hasValidAssignment G c R

A valid assignment always exists with R = 0 layers when cycle-degree ≤ c for all edges.

structure LayerBound {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (c : ℕ) : Type

The number of layers needed to achieve cycle-degree at most c. This is the R in R_G^c from the paper.

The value depends on the specific graph and cycle assignment strategy. The Freedman-Hastings decongestion lemma establishes that for constant-degree graphs, R_G^c = O(log² |V|).

• numLayers : ℕ

  The number of layers (R) in the construction

• valid : hasValidAssignment G c self.numLayers

  A valid cycle-layer assignment exists with this many layers

Freedman-Hastings Decongestion Lemma

The Freedman-Hastings decongestion lemma establishes that for any constant-degree graph G, the minimum number of layers R_G^c = O(log² |V_G|).

This is a deep result requiring probabilistic methods and expander theory. We state it as a class assumption that can be satisfied by specific graphs, rather than proving it here. The proof is beyond the scope of basic type theory and would require significant additional machinery.

class HasDecongestionBound {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (c maxDegree : ℕ) : Prop

Class asserting that a graph satisfies the Freedman-Hastings decongestion bound. This states that there exists a layer bound R satisfying R = O(log² |V|) for the given cycle-degree bound and maximum vertex degree.

This is a hypothesis that must be verified for specific graphs using the Freedman-Hastings decongestion lemma from the literature.

• bound_exists : ∃ (lb : LayerBound G c), lb.numLayers ≤ (Nat.log 2 (Fintype.card V) + 1) ^ 2 * (maxDegree + 1)

  A layer bound exists with polylogarithmic number of layers

• c_pos : c > 0

  The cycle-degree bound is positive

• degree_bounded (v : V) : (G.incidentEdges v).card ≤ maxDegree

  The graph has bounded degree

theorem minLayers_polylog_bound {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (c maxDegree : ℕ) [hbound : HasDecongestionBound G c maxDegree] : ∃ (R : ℕ), hasValidAssignment G c R ∧ R ≤ (maxDegree + 1) * (Nat.log 2 (Fintype.card V) + 1) ^ 2

For graphs satisfying the Freedman-Hastings bound, there exists a valid layer assignment with R_G^c = O(log² n) where n = |V|

Summary

This formalization captures the cycle-sparsification construction:

1. Layered Structure: The sparsified graph has R+1 layers:

   • Layer 0: The original graph vertices
   • Layers 1, ..., R: Dummy vertex copies

2. Vertex Type: LayeredVertex V R represents vertices as (layer, original_vertex) pairs. Total vertices: (R+1) · |V_G|

3. Edge Types:

   • Intra-layer: Copies of original graph edges within each layer
   • Inter-layer: Connect each vertex to its copy in adjacent layers
   • Triangulation: Added to cellulate cycles assigned to each layer

4. Triangulation: For each cycle assigned to a layer, add diagonal edges forming triangles. The triangulationEdgePairs function computes these edges.

5. Cycle-Layer Assignment: Each cycle is assigned to exactly one layer where its triangulation edges are added.

6. Cycle-Degree Bound: The constraint that every edge participates in at most c cycles from the generating set.

7. Freedman-Hastings Bound: Stated as a class HasDecongestionBound asserting R_G^c = O(log² |V_G|) for constant-degree graphs. This is a hypothesis from the literature that must be verified for specific graphs.

Key properties proven:

• Layer 0 is isomorphic to the original graph (for intra-layer edges)
• Inter-layer edges connect consecutive layers
• Triangulation edges are symmetric and within the same layer
• The vertex partition into original and dummy layers
• Cardinality formulas for vertices in each layer