Definition 6: Cycle-Sparsified Graph

Statement

The cycle-sparsified graph (decongested graph) G̿ with cycle-degree bound c is constructed from a connected graph G with a chosen generating set of cycles by:

1. Creating R+1 layers (layer 0 = original, layers 1..R = copies of V)
2. Adding inter-layer edges (v^(i), v^(i+1)) for each vertex v and 0 ≤ i < R
3. Adding intra-layer edges from the original graph (replicated in all layers)
4. Adding cellulation (triangulation) edges in layers i > 0 to decompose high-degree cycles into triangles using the zigzag pattern
5. Choosing R large enough so each edge participates in at most c cycles per layer

The key property is that the generating set of cycles consists of:

• Triangles from cellulation (weight 3)
• Squares connecting adjacent layers (weight 4) All generating cycles have weight at most 4.

Main Results

• SparsifiedVertex : vertex type V × Fin (R+1)
• isIntraLayerEdge : same-layer edge from original graph
• isInterLayerEdge : same vertex in consecutive layers
• zigzagDiagonals : cellulation diagonals using zigzag pattern
• isTriangulationEdge : cellulation edge in some layer > 0
• sparsifiedAdj / sparsifiedGraph : the sparsified graph
• edgeCycleDegreeInLayer / LayerCycleDegreeBound : per-layer cycle participation bound
• SparsificationData : complete construction data
• square_is_cycle : squares from adjacent layers form 4-cycles
• zigzagDiagonals_mem : diagonal endpoints come from original cycle
• zigzagDiagonals_length : m-gon produces exactly m-2 diagonals
• cellulation_adj_of_diagonal : diagonals create edges in sparsified graph
• cellulation_triangle_exists : cellulation produces triangles (weight 3)

@[reducible, inline]

abbrev CycleSparsification.SparsifiedVertex (V : Type u_1) (R : ℕ) : Type u_1

The vertex type of the sparsified graph: (v, i) represents vertex v in layer i. Layer 0 is the original.

Equations

• CycleSparsification.SparsifiedVertex V R = (V × Fin (R + 1))

def CycleSparsification.originalLayer {R : ℕ} : Fin (R + 1)

The original layer is layer 0.

Equations

• CycleSparsification.originalLayer = ⟨0, ⋯⟩

Layer Structure

theorem CycleSparsification.card_sparsifiedVertex {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} : Fintype.card (SparsifiedVertex V R) = (R + 1) * Fintype.card V

def CycleSparsification.layerVertices {V : Type u_1} [Fintype V] {R : ℕ} (i : Fin (R + 1)) : Finset (SparsifiedVertex V R)

Equations

• CycleSparsification.layerVertices i = {p : CycleSparsification.SparsifiedVertex V R | p.2 = i}

theorem CycleSparsification.card_layerVertices {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (i : Fin (R + 1)) : (layerVertices i).card = Fintype.card V

def CycleSparsification.embedOriginal {V : Type u_1} {R : ℕ} (v : V) : SparsifiedVertex V R

Equations

• CycleSparsification.embedOriginal v = (v, CycleSparsification.originalLayer)

theorem CycleSparsification.embedOriginal_injective {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} : Function.Injective embedOriginal

theorem CycleSparsification.vertex_partition {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (p : SparsifiedVertex V R) : ∃! i : Fin (R + 1), p ∈ layerVertices i

theorem CycleSparsification.vertex_partition_disjoint {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (i j : Fin (R + 1)) (hij : i ≠ j) : Disjoint (layerVertices i) (layerVertices j)

Three Types of Edges

def CycleSparsification.isIntraLayerEdge {V : Type u_1} {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] (p q : SparsifiedVertex V R) : Prop

An intra-layer edge: two vertices in the same layer where the original graph has an edge. The original graph edges are replicated in every layer, enabling square cycles between any two consecutive layers.

Equations

• CycleSparsification.isIntraLayerEdge G p q = (p.2 = q.2 ∧ G.Adj p.1 q.1)

def CycleSparsification.isInterLayerEdge {V : Type u_1} {R : ℕ} (p q : SparsifiedVertex V R) : Prop

An inter-layer edge: copies of the same vertex in consecutive layers.

Equations

• CycleSparsification.isInterLayerEdge p q = (p.1 = q.1 ∧ (↑p.2 + 1 = ↑q.2 ∨ ↑q.2 + 1 = ↑p.2))

Zigzag Triangulation (Cellulation)

For a cycle visiting vertices v₁, v₂, ..., vₘ in order, cellulation adds diagonal edges following the zigzag pattern: (v₁, v_{m-1}), (v_{m-1}, v₂), (v₂, v_{m-2}), (v_{m-2}, v₃), ... This decomposes the m-gon into m-2 triangles.

def CycleSparsification.zigzagGo {V : Type u_1} {n : ℕ} (vs : Fin n → V) (left right : ℕ) (hleft : left < n) (hright : right < n) (fromLeft : Bool) (fuel : ℕ) : List (V × V)

Auxiliary recursive function for zigzag diagonals. Given a vector vs of length n, left/right indices, and alternation flag, produces the zigzag diagonal pairs. Requires left < n and right < n.

Equations

• One or more equations did not get rendered due to their size.
• CycleSparsification.zigzagGo vs left right hleft hright fromLeft 0 = []

def CycleSparsification.zigzagDiagonals {V : Type u_1} (vs : List V) : List (V × V)

Zigzag diagonal pairs from a list of cycle vertices. Given [v₁, v₂, ..., vₘ], produces the zigzag cellulation diagonals: (v₁, v_{m-1}), (v_{m-1}, v₂), (v₂, v_{m-2}), (v_{m-2}, v₃), ... The zigzag alternates between connecting from the "left" end and the "right" end of the remaining polygon, working inward.

For m ≤ 3, no diagonals are needed (triangle or simpler). For m = 4 (square), one diagonal (v₁, v₃). For m = 5 (pentagon), two diagonals: (v₁, v₄), (v₄, v₂).

Equations

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

def CycleSparsification.isTriangulationEdge {V : Type u_1} {R : ℕ} {C : Type u_2} (cycleAssignment : C → Fin (R + 1)) (cycleVerts : C → List V) (p q : SparsifiedVertex V R) : Prop

A triangulation edge: a cellulation diagonal in some layer i > 0. The zigzag diagonals of a cycle assigned to layer i create new edges in that layer, decomposing the cycle into triangles.

Equations

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

Symmetry and Irreflexivity

theorem CycleSparsification.isIntraLayerEdge_symm {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {p q : SparsifiedVertex V R} (h : isIntraLayerEdge G p q) : isIntraLayerEdge G q p

theorem CycleSparsification.isInterLayerEdge_symm {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} {p q : SparsifiedVertex V R} (h : isInterLayerEdge p q) : isInterLayerEdge q p

theorem CycleSparsification.isTriangulationEdge_symm {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} {C : Type u_2} {cycleAssignment : C → Fin (R + 1)} {cycleVerts : C → List V} {p q : SparsifiedVertex V R} (h : isTriangulationEdge cycleAssignment cycleVerts p q) : isTriangulationEdge cycleAssignment cycleVerts q p

theorem CycleSparsification.isIntraLayerEdge_irrefl {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] (p : SparsifiedVertex V R) : ¬isIntraLayerEdge G p p

theorem CycleSparsification.isInterLayerEdge_irrefl {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (p : SparsifiedVertex V R) : ¬isInterLayerEdge p p

The Sparsified Adjacency Relation

def CycleSparsification.sparsifiedAdj {V : Type u_1} {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} (cycleAssignment : C → Fin (R + 1)) (cycleVerts : C → List V) (p q : SparsifiedVertex V R) : Prop

The adjacency relation combining all three edge types.

Equations

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

theorem CycleSparsification.sparsifiedAdj_symm {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} {cycleAssignment : C → Fin (R + 1)} {cycleVerts : C → List V} {p q : SparsifiedVertex V R} (h : sparsifiedAdj G cycleAssignment cycleVerts p q) : sparsifiedAdj G cycleAssignment cycleVerts q p

theorem CycleSparsification.sparsifiedAdj_irrefl {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} (cycleAssignment : C → Fin (R + 1)) (cycleVerts : C → List V) (p : SparsifiedVertex V R) : ¬sparsifiedAdj G cycleAssignment cycleVerts p p

The Cycle-Sparsified Simple Graph

def CycleSparsification.sparsifiedGraph {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} (cycleAssignment : C → Fin (R + 1)) (cycleVerts : C → List V) : SimpleGraph (SparsifiedVertex V R)

The cycle-sparsified graph G̿ as a SimpleGraph on V × Fin (R+1).

Equations

• CycleSparsification.sparsifiedGraph G cycleAssignment cycleVerts = { Adj := CycleSparsification.sparsifiedAdj G cycleAssignment cycleVerts, symm := ⋯, loopless := ⋯ }

Layer-0 Preserves Original Graph

theorem CycleSparsification.layer_zero_adj_of_original {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} (cycleAssignment : C → Fin (R + 1)) (cycleVerts : C → List V) {v w : V} (hadj : G.Adj v w) : (sparsifiedGraph G cycleAssignment cycleVerts).Adj (v, originalLayer) (w, originalLayer)

Inter-Layer Edge Properties

theorem CycleSparsification.interLayerEdge_exists {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} (cycleAssignment : C → Fin (R + 1)) (cycleVerts : C → List V) (v : V) (i : Fin R) : have i₀ := ⟨↑i, ⋯⟩; have i₁ := ⟨↑i + 1, ⋯⟩; (sparsifiedGraph G cycleAssignment cycleVerts).Adj (v, i₀) (v, i₁)

Triangulation Edge Properties

theorem CycleSparsification.triangulationEdge_same_layer {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} {C : Type u_2} {cycleAssignment : C → Fin (R + 1)} {cycleVerts : C → List V} {p q : SparsifiedVertex V R} (h : isTriangulationEdge cycleAssignment cycleVerts p q) : p.2 = q.2

theorem CycleSparsification.triangulationEdge_not_layer_zero {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} {C : Type u_2} {cycleAssignment : C → Fin (R + 1)} {cycleVerts : C → List V} {p q : SparsifiedVertex V R} (h : isTriangulationEdge cycleAssignment cycleVerts p q) : p.2 ≠ originalLayer

Simp lemmas

@[simp]

theorem CycleSparsification.intraLayer_iff {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] (v w : V) (i : Fin (R + 1)) : isIntraLayerEdge G (v, i) (w, i) ↔ G.Adj v w

@[simp]

theorem CycleSparsification.interLayer_same_vertex_iff {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (v : V) (i j : Fin (R + 1)) : isInterLayerEdge (v, i) (v, j) ↔ ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i

Edge Classification

theorem CycleSparsification.edge_trichotomy {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} {cycleAssignment : C → Fin (R + 1)} {cycleVerts : C → List V} {p q : SparsifiedVertex V R} (hadj : (sparsifiedGraph G cycleAssignment cycleVerts).Adj p q) : isIntraLayerEdge G p q ∨ isInterLayerEdge p q ∨ isTriangulationEdge cycleAssignment cycleVerts p q

theorem CycleSparsification.diff_layer_not_intra {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {p q : SparsifiedVertex V R} (h : p.2 ≠ q.2) : ¬isIntraLayerEdge G p q

theorem CycleSparsification.diff_vertex_not_inter {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} {p q : SparsifiedVertex V R} (h : p.1 ≠ q.1) : ¬isInterLayerEdge p q

Squares: Explicit 4-Cycles

theorem CycleSparsification.square_is_cycle {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} (cycleAssignment : C → Fin (R + 1)) (cycleVerts : C → List V) (v u : V) (hadj : G.Adj v u) (i : Fin R) : have G' := sparsifiedGraph G cycleAssignment cycleVerts; have i₀ := ⟨↑i, ⋯⟩; have i₁ := ⟨↑i + 1, ⋯⟩; G'.Adj (v, i₀) (v, i₁) ∧ G'.Adj (v, i₁) (u, i₁) ∧ G'.Adj (u, i₁) (u, i₀) ∧ G'.Adj (u, i₀) (v, i₀)

A square in the sparsified graph: given (v,u) ∈ E(G) and layer i < R, (v^i, v^{i+1}, u^{i+1}, u^i) form a 4-cycle.

Zigzag Cellulation: Vertex Membership and Triangle Decomposition

The zigzag cellulation decomposes an m-gon (m ≥ 4) into m-2 triangles by adding diagonal edges. We prove:

1. All diagonal endpoints come from the original cycle vertices
2. The diagonals produce exactly m-2 pairs
3. Each diagonal, together with consecutive cycle edges (intra-layer), forms a triangle in the sparsified graph — establishing the paper's key claim that the generating set consists of triangles (weight 3) and squares (weight 4).

theorem CycleSparsification.zigzagGo_mem_range {V : Type u_1} [Fintype V] [DecidableEq V] {n : ℕ} (vs : Fin n → V) (left right : ℕ) (hl : left < n) (hr : right < n) (b : Bool) (fuel : ℕ) {p : V × V} (hp : p ∈ zigzagGo vs left right hl hr b fuel) : (∃ (i : Fin n), vs i = p.1) ∧ ∃ (j : Fin n), vs j = p.2

Every vertex appearing in a zigzagGo output is a value of vs at some index in the range [left, right].

theorem CycleSparsification.zigzagDiagonals_mem {V : Type u_1} [Fintype V] [DecidableEq V] (vs : List V) {p : V × V} (hp : p ∈ zigzagDiagonals vs) : p.1 ∈ vs ∧ p.2 ∈ vs

Every vertex in a zigzag diagonal pair is a member of the original cycle list.

theorem CycleSparsification.zigzagGo_nil {V : Type u_1} [Fintype V] [DecidableEq V] {n : ℕ} (vs : Fin n → V) (left right : ℕ) (hl : left < n) (hr : right < n) (b : Bool) (fuel : ℕ) (hle : right ≤ left + 1) : zigzagGo vs left right hl hr b fuel = []

When the gap is closed (right ≤ left + 1), zigzagGo returns the empty list.

theorem CycleSparsification.zigzagGo_exact_length {V : Type u_1} [Fintype V] [DecidableEq V] {n : ℕ} (vs : Fin n → V) (left right : ℕ) (hl : left < n) (hr : right < n) (b : Bool) (fuel : ℕ) (hfuel : right - left - 1 ≤ fuel) (hgt : left + 1 < right) : (zigzagGo vs left right hl hr b fuel).length = right - left - 1

The exact number of diagonals from zigzagGo: when right > left + 1 and fuel ≥ right - left - 1, zigzagGo produces exactly right - left - 1 pairs.

theorem CycleSparsification.zigzagDiagonals_length {V : Type u_1} [Fintype V] [DecidableEq V] (vs : List V) (hlen : 4 ≤ vs.length) : (zigzagDiagonals vs).length = vs.length - 2

For a cycle of length m ≥ 4, zigzag cellulation produces exactly m-2 diagonals. This corresponds to decomposing an m-gon into m-2 triangles.

Cellulation Produces Triangles in the Sparsified Graph

The key property from the paper: for each cycle assigned to a layer i > 0, the zigzag cellulation diagonals together with the intra-layer cycle edges form triangles in the sparsified graph.

A cellulation triangle consists of three vertices a, b, c in the same layer i, where two pairs are connected by intra-layer edges (from the original cycle) and one pair by a triangulation diagonal. Since all three edge types (intra-layer, triangulation) are part of sparsifiedAdj, these triangles are 3-cycles in the sparsified graph.

theorem CycleSparsification.cellulation_adj_of_diagonal {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} (cycleAssignment : C → Fin (R + 1)) (cycleVerts : C → List V) (c : C) (a b : V) (hab_ne : a ≠ b) (hne : cycleAssignment c ≠ originalLayer) (hdiag : (a, b) ∈ zigzagDiagonals (cycleVerts c)) : have i := cycleAssignment c; (sparsifiedGraph G cycleAssignment cycleVerts).Adj (a, i) (b, i)

For a cycle c assigned to layer i > 0, if (a, b) is a zigzag diagonal of c, then (a, i) and (b, i) are adjacent in the sparsified graph via a triangulation edge.

theorem CycleSparsification.cellulation_adj_of_cycle_edge {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} (cycleAssignment : C → Fin (R + 1)) (cycleVerts : C → List V) (u v : V) (huv_ne : u ≠ v) (hadj : G.Adj u v) (i : Fin (R + 1)) : (sparsifiedGraph G cycleAssignment cycleVerts).Adj (u, i) (v, i)

For a cycle c assigned to layer i > 0, if consecutive vertices u, v of the cycle are adjacent in G, then (u, i) and (v, i) are adjacent in the sparsified graph via an intra-layer edge.

theorem CycleSparsification.cellulation_triangle_exists {V : Type u_1} [Fintype V] [DecidableEq V] {R : ℕ} (G : SimpleGraph V) [DecidableRel G.Adj] {C : Type u_2} (cycleAssignment : C → Fin (R + 1)) (cycleVerts : C → List V) (c : C) (a b x : V) (hab_ne : a ≠ b) (hax_ne : a ≠ x) (hbx_ne : b ≠ x) (hne : cycleAssignment c ≠ originalLayer) (hdiag : (a, b) ∈ zigzagDiagonals (cycleVerts c)) (hadj_ax : G.Adj a x) (hadj_bx : G.Adj b x) : have i := cycleAssignment c; have G' := sparsifiedGraph G cycleAssignment cycleVerts; G'.Adj (a, i) (b, i) ∧ G'.Adj (a, i) (x, i) ∧ G'.Adj (b, i) (x, i)

Key property (Cellulation Triangle Existence): For a cycle c visiting vertices v₁, ..., vₘ assigned to layer i > 0, each zigzag diagonal (a, b) together with two intra-layer edges from G forms a triangle in the sparsified graph.

Specifically: if (a, b) is a diagonal and both a-x and b-x are edges in G for some common neighbor x on the cycle, then (a,i)-(b,i)-(x,i) is a triangle. This is the content of the paper's claim that cellulation decomposes cycles into triangles, all of weight 3 in the generating set.

Cycle Degree in the Sparsified Graph

The cycle-degree bound is the key property of the sparsification construction. Given a cycle assignment C → Fin (R+1) that distributes cycles across layers, the sparsified graph has a new generating set consisting of:

• Triangles from cellulation (each original cycle assigned to layer i produces triangles in that layer)
• Squares connecting adjacent layers

The cycle degree of an edge in the sparsified graph is the number of cycles from this new generating set that contain it. The parameter c bounds this.

def CycleSparsification.edgeCycleDegreeInLayer {α : Type u_2} {R' : ℕ} {C : Type u_3} [Fintype C] (cycles : C → Set α) [(c : C) → DecidablePred fun (x : α) => x ∈ cycles c] (cycleAssignment : C → Fin (R' + 1)) (e : α) (i : Fin (R' + 1)) : ℕ

The number of original cycles assigned to a given layer that contain a given edge. This counts how many cellulated cycles in layer i use edge e (as an intra-layer copy). This is the per-layer edge participation count: the whole point of distributing cycles across layers is to make this small.

Equations

• CycleSparsification.edgeCycleDegreeInLayer cycles cycleAssignment e i = {c : C | cycleAssignment c = i ∧ e ∈ cycles c}.card

def CycleSparsification.LayerCycleDegreeBound {α : Type u_2} {R' : ℕ} {C : Type u_3} [Fintype C] (cycles : C → Set α) [(c : C) → DecidablePred fun (x : α) => x ∈ cycles c] (cycleAssignment : C → Fin (R' + 1)) (bound : ℕ) : Prop

The per-layer cycle-degree bound: for every edge and every layer, the number of cycles assigned to that layer containing that edge is at most bound. This is the correct formalization of the paper's cycle-degree bound c: distributing cycles across R layers so that each edge participates in at most c cycles within any single layer.

Equations

• CycleSparsification.LayerCycleDegreeBound cycles cycleAssignment bound = ∀ (e : α) (i : Fin (R' + 1)), CycleSparsification.edgeCycleDegreeInLayer cycles cycleAssignment e i ≤ bound

def CycleSparsification.edgeCycleDegree {α : Type u_2} {C : Type u_3} [Fintype C] (cycles : C → Set α) [(c : C) → DecidablePred fun (x : α) => x ∈ cycles c] (e : α) : ℕ

The global edge-cycle degree: total number of generating cycles containing edge e (across all layers).

Equations

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

theorem CycleSparsification.edgeCycleDegree_le_card {α : Type u_2} {C : Type u_3} [Fintype C] (cycles : C → Set α) [(c : C) → DecidablePred fun (x : α) => x ∈ cycles c] (e : α) : edgeCycleDegree cycles e ≤ Fintype.card C

theorem CycleSparsification.layerBound_implies_global_bound {α : Type u_2} {R' : ℕ} {C : Type u_3} [Fintype C] [DecidableEq C] (cycles : C → Set α) [(c : C) → DecidablePred fun (x : α) => x ∈ cycles c] (cycleAssignment : C → Fin (R' + 1)) (bound : ℕ) (hbound : LayerCycleDegreeBound cycles cycleAssignment bound) (e : α) : edgeCycleDegree cycles e ≤ (R' + 1) * bound

Per-layer bound implies global bound scaled by number of layers.

Complete Sparsification Data

structure CycleSparsification.SparsificationData {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] : Type (max u_1 u_2)

The complete data for a cycle-sparsified graph construction. The cycle assignment distributes cycles across layers, and the per-layer cycle-degree bound ensures each edge participates in at most cycleBound cycles within any single layer.

• numLayers : ℕ
• cycleAssignment : C → Fin (self.numLayers + 1)
• cycleVerts : C → List V
• cycleBound : ℕ
• bound_holds : LayerCycleDegreeBound cycles self.cycleAssignment self.cycleBound

  The cycle assignment achieves the per-layer bound: each edge participates in at most cycleBound cycles within any single layer.

noncomputable def CycleSparsification.SparsificationData.graph {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] {cycles : C → Set ↑G.edgeSet} [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (data : SparsificationData G cycles) : SimpleGraph (SparsifiedVertex V data.numLayers)

Extract the sparsified graph from sparsification data.

Equations

• data.graph = CycleSparsification.sparsifiedGraph G data.cycleAssignment data.cycleVerts

Minimum Number of Layers R_G^c

The minimum number of layers R_G^c is the smallest R such that there exists a cycle assignment C → Fin (R+1) achieving per-layer cycle-degree ≤ c. This is nontrivial: distributing cycles across more layers allows reducing the per-layer participation, and the Freedman-Hastings decongestion lemma gives R_G^c = O(log² W) for constant-degree graphs.

noncomputable def CycleSparsification.minLayers {α : Type u_2} {C : Type u_3} [Fintype C] (cycles : C → Set α) [(c : C) → DecidablePred fun (x : α) => x ∈ cycles c] (bound : ℕ) (hexists : ∃ (R : ℕ) (f : C → Fin (R + 1)), LayerCycleDegreeBound cycles f bound) : ℕ

The minimum number of layers R_G^c for cycle-sparsification with per-layer cycle-degree bound c. This is the smallest R such that cycles can be distributed across R+1 layers with each edge participating in at most c cycles per layer.

Equations

• CycleSparsification.minLayers cycles bound hexists = Nat.find hexists

theorem CycleSparsification.minLayers_spec {α : Type u_2} {C : Type u_3} [Fintype C] (cycles : C → Set α) [(c : C) → DecidablePred fun (x : α) => x ∈ cycles c] (bound : ℕ) (hexists : ∃ (R : ℕ) (f : C → Fin (R + 1)), LayerCycleDegreeBound cycles f bound) : ∃ (f : C → Fin (minLayers cycles bound hexists + 1)), LayerCycleDegreeBound cycles f bound

The minimum layers value achieves the bound.

theorem CycleSparsification.minLayers_minimal {α : Type u_2} {C : Type u_3} [Fintype C] (cycles : C → Set α) [(c : C) → DecidablePred fun (x : α) => x ∈ cycles c] (bound : ℕ) (hexists : ∃ (R : ℕ) (f : C → Fin (R + 1)), LayerCycleDegreeBound cycles f bound) (R' : ℕ) (hR' : R' < minLayers cycles bound hexists) : ¬∃ (f : C → Fin (R' + 1)), LayerCycleDegreeBound cycles f bound

No smaller number of layers suffices.

Zigzag Triangulation Properties

theorem CycleSparsification.zigzagDiagonals_short {V : Type u_1} [Fintype V] [DecidableEq V] (vs : List V) (h : vs.length < 4) : zigzagDiagonals vs = []

For short lists (length < 4), no diagonals are produced.

theorem CycleSparsification.zigzagGo_length_le {V : Type u_1} [Fintype V] [DecidableEq V] {n : ℕ} (vs : Fin n → V) (left right : ℕ) (hl : left < n) (hr : right < n) (b : Bool) (fuel : ℕ) : (zigzagGo vs left right hl hr b fuel).length ≤ fuel

The zigzag go function produces at most fuel diagonal pairs.