16 Def 6: Cycle-Sparsified Graph
This chapter formalizes the cycle-sparsification construction for a graph \(G\) with a chosen generating set of cycles. The construction builds \(R+1\) copies (layers) of \(G\), connects them by inter-layer edges, and adds triangulation edges to cellulate cycles within designated layers. The key constraint is that every edge participates in at most \(c\) cycles from the generating set.
A layered vertex in a graph with \(R+1\) layers is a pair \((i, v)\) where \(i \in \{ 0, 1, \ldots , R\} \) is the layer index and \(v \in V\) is the original vertex. Layer \(0\) contains the original vertices; layers \(1, \ldots , R\) contain dummy copies.
Formally, given a type \(V\) and a natural number \(R\), a layered vertex is a structure consisting of:
a layer index \(\mathrm{layer} \in \mathrm{Fin}(R+1)\),
an original vertex \(\mathrm{vertex} \in V\).
A layered vertex \(\ell v\) is original if its layer index equals \(0\), i.e., \(\ell v.\mathrm{layer} = 0\).
A layered vertex \(\ell v\) is dummy if its layer index is nonzero, i.e., \(\ell v.\mathrm{layer} \neq 0\).
The embedding of an original vertex \(v \in V\) into layer \(0\) of the layered graph is defined by \(\mathrm{ofOriginal}(v) = (0, v)\).
The embedding of a vertex \(v \in V\) into layer \(i\) is defined by \(\mathrm{inLayer}(i, v) = (i, v)\).
Every layered vertex is either original or dummy. That is, for any layered vertex \(\ell v\), either \(\ell v.\mathrm{layer} = 0\) or \(\ell v.\mathrm{layer} \neq 0\).
We consider whether \(\ell v.\mathrm{layer} = 0\). If so, \(\ell v\) is original (left case). If not, \(\ell v\) is dummy (right case). This is an instance of the law of excluded middle applied to the proposition \(\ell v.\mathrm{layer} = 0\).
A zigzag state tracks the progress of building triangulation edges for a cycle. It consists of:
\(\mathrm{low} : \mathbb {N}\), the current low index,
\(\mathrm{high} : \mathbb {N}\), the current high index (exclusive),
\(\mathrm{fromLow} : \mathrm{Bool}\), indicating whether the next edge starts from the low index.
One step of the zigzag edge generation. Given a list of cycle vertices of length \(n\), and a zigzag state \(s\) with \(s.\mathrm{low} {\lt} n\), \(s.\mathrm{high} \leq n\), and \(s.\mathrm{low} + 2 {\lt} s.\mathrm{high}\), the step produces an edge pair \((v_1, v_2)\) and a new zigzag state:
If \(\mathrm{fromLow}\) is true: the edge connects \(v_{\mathrm{low}}\) to \(v_{\mathrm{high}-1}\), and the next state has \(\mathrm{high}' = \mathrm{high} - 1\) and \(\mathrm{fromLow}' = \mathrm{false}\).
If \(\mathrm{fromLow}\) is false: the edge connects \(v_{\mathrm{high}-1}\) to \(v_{\mathrm{low}+1}\), and the next state has \(\mathrm{low}' = \mathrm{low} + 1\) and \(\mathrm{fromLow}' = \mathrm{true}\).
Given a list of cycle vertices \([v_0, v_1, \ldots , v_{n-1}]\), the triangulation edge pairs are the diagonal edges that triangulate the cycle using a zigzag pattern. For a cycle of length \(n \geq 4\), this produces \(n - 3\) triangulation edges following the pattern:
Even-indexed steps connect from the low index to the high end, and odd-indexed steps connect from the high end to the next low index. For cycles of length \({\lt} 4\), the result is the empty list.
For cycles of length less than \(4\), no triangulation edges are needed:
By simplification using the definition of \(\mathrm{triangulationEdgePairs}\): when the length is less than \(4\), the guard condition \(n {\lt} 4\) is satisfied and the function returns the empty list.
A cycle-layer assignment for a set of cycles \(C\) and \(R+1\) layers assigns each cycle to exactly one layer. Formally, it is a function \(\mathrm{assign} : C \to \mathrm{Fin}(R+1)\).
The set of cycles assigned to a particular layer \(\ell \) is:
For any cycle-layer assignment \(a\) and any cycle \(c\), there exists a unique layer \(\ell \) such that \(c \in \mathrm{cyclesInLayer}(a, \ell )\).
We take \(\ell = a.\mathrm{assign}(c)\). First, by the definition of \(\mathrm{cyclesInLayer}\), we have \(c \in \mathrm{cyclesInLayer}(a, a.\mathrm{assign}(c))\) since the filter condition \(a.\mathrm{assign}(c) = a.\mathrm{assign}(c)\) holds trivially. For uniqueness, suppose \(c \in \mathrm{cyclesInLayer}(a, \ell ')\). Then by the filter condition, \(a.\mathrm{assign}(c) = \ell '\), so \(\ell ' = a.\mathrm{assign}(c)\) by symmetry.
The cycle degree of an edge \(e\) with respect to a set of cycles \(C\) (each given as a finset of edges) is the number of cycles in the generating set that contain \(e\):
The maximum cycle degree over all edges is:
For any edge \(e\), the cycle degree is at most the total number of cycles:
By the definition of cycle degree, it equals the cardinality of a filter of the universal finset. The cardinality of a filtered finset is at most the cardinality of the original finset, which equals \(|C|\).
A cycle-sparsification of a graph \(G\) with cycles \(C\) is a structure consisting of:
a base graph \(G\) with its chosen generating set of cycles (of type \(\mathrm{GraphWithCycles}\; V\; E\; C\)),
a number of additional layers \(R\) (total layers \(= R + 1\)),
a cycle-degree bound \(c \in \mathbb {N}\),
a cycle-layer assignment \(\mathrm{cycleAssignment} : C \to \mathrm{Fin}(R+1)\),
for each cycle, a list of vertices representing the cycle in order,
the cycle-degree constraint: for every edge \(e \in E\), \(\mathrm{cycleDegree}(\mathrm{cycles}, e) \leq c\).
The vertex type of the sparsified graph is \(\mathrm{LayeredVertex}\; V\; S.\mathrm{numLayers}\), i.e., pairs of (layer index, original vertex).
The number of vertices in the sparsified graph is \((R+1) \cdot |V|\):
This follows directly from the cardinality of layered vertices, which equals the product of the number of layers and the number of original vertices.
The original layer (layer \(0\)) of the sparsified graph is the set of all layered vertices with layer index \(0\):
The dummy layers of the sparsified graph consist of all layered vertices with nonzero layer index:
Every vertex of the sparsified graph is either in the original layer or in a dummy layer:
By extensionality, it suffices to show that for an arbitrary vertex \(v\), membership in the union is equivalent to membership in the universal set. Expanding the definitions of \(\mathrm{originalLayer}\) and \(\mathrm{dummyLayers}\) as filters, the condition becomes \(v.\mathrm{layer} = 0 \lor v.\mathrm{layer} \neq 0\), which is a tautology.
The original layer and dummy layers are disjoint:
Using the characterization of disjointness via no equal elements, suppose \(a \in \mathrm{originalLayer}(S)\) and \(b \in \mathrm{dummyLayers}(S)\) with \(a = b\). Then \(a.\mathrm{layer} = 0\) (from being in the original layer), and rewriting with \(a = b\), we get \(b.\mathrm{layer} = 0\). But \(b \in \mathrm{dummyLayers}\) requires \(b.\mathrm{layer} \neq 0\), giving a contradiction.
An intra-layer edge in the sparsified graph connects two vertices in the same layer that are adjacent in the original graph. Formally, \((\ell v_1, \ell v_2)\) is an intra-layer edge if:
An inter-layer edge connects a vertex to its copy in an adjacent layer. Formally, \((\ell v_1, \ell v_2)\) is an inter-layer edge if:
The set of triangulation edge pairs for a cycle \(c\) in layer \(\ell \) is:
If the cycle \(c\) is assigned to layer \(\ell \): the image of \(\mathrm{triangulationEdgePairs}(\mathrm{cycleVertices}(c))\) under the embedding into layer \(\ell \).
Otherwise: the empty list.
A triangulation edge \((\ell v_1, \ell v_2)\) is an edge added to cellulate a cycle. Formally:
The adjacency relation in the sparsified graph is defined as: two layered vertices \(\ell v_1, \ell v_2\) are adjacent if \(\ell v_1 \neq \ell v_2\) and at least one of the following holds:
\((\ell v_1, \ell v_2)\) is an intra-layer edge,
\((\ell v_1, \ell v_2)\) is an inter-layer edge,
\((\ell v_1, \ell v_2)\) is a triangulation edge.
Intra-layer adjacency is symmetric:
For both directions, given \(\ell v_1.\mathrm{layer} = \ell v_2.\mathrm{layer}\) and adjacency of the underlying vertices, we use symmetry of the layer equality and the commutativity of adjacency in the base graph (\(G.\mathrm{adj\_ comm}\)).
Inter-layer adjacency is symmetric:
For both directions, we use symmetry of the vertex equality and swap the disjunction on layer indices.
Triangulation adjacency is symmetric:
For both directions, given \(\ell v_1.\mathrm{layer} = \ell v_2.\mathrm{layer}\), a cycle \(c\) assigned to that layer, and the membership condition on triangulation edge pairs, we use symmetry of the layer equality and swap the disjunction on the pair orientations. The cycle assignment condition is transported using the layer equality.
Sparsified adjacency is symmetric:
By simplification using the symmetry of \(\neq \), and the symmetry of each of the three edge types established above.
Sparsified adjacency is irreflexive: \(\neg \, \mathrm{sparsifiedAdj}(S, \ell v, \ell v)\) for all \(\ell v\).
By simplification: the first conjunct of sparsified adjacency requires \(\ell v \neq \ell v\), which is false.
The cycle-sparsified graph as a \(\mathrm{SimpleGraph}\) on the sparsified vertex type, with adjacency given by \(\mathrm{sparsifiedAdj}\), symmetry from the symmetry theorem, and irreflexivity from the irreflexivity theorem.
Layer \(0\) is isomorphic to the original graph for intra-layer edges: for any vertices \(v, w \in V\),
By simplification: both embedded vertices have layer \(0\), so the layer equality holds trivially, and the adjacency condition reduces to adjacency in the base graph.
Each vertex \(v\) in layer \(i\) is connected to its copy in layer \(i+1\): for any \(i\) with \(i + 1 {\lt} R + 1\),
By simplification of the definitions: the vertex components are equal, and the layer index of the first vertex plus one equals the layer index of the second vertex. We choose the left disjunct and verify trivially.
Inter-layer edges only connect consecutive layers: if \((\ell v_1, \ell v_2)\) is an inter-layer edge, then
This follows directly from the second component of the inter-layer edge definition.
Inter-layer edges connect the same underlying vertex: if \((\ell v_1, \ell v_2)\) is an inter-layer edge, then \(\ell v_1.\mathrm{vertex} = \ell v_2.\mathrm{vertex}\).
This follows directly from the first component of the inter-layer edge definition.
Triangulation edges are within the same layer: if \((\ell v_1, \ell v_2)\) is a triangulation edge, then \(\ell v_1.\mathrm{layer} = \ell v_2.\mathrm{layer}\).
This follows directly from the first component of the triangulation edge definition.
Every triangulation edge comes from some cycle assigned to the relevant layer: if \((\ell v_1, \ell v_2)\) is a triangulation edge, then there exists \(c \in C\) with \(\mathrm{assign}(c) = \ell v_1.\mathrm{layer}\).
From the triangulation edge hypothesis, we obtain the layer equality, a cycle \(c\), and the assignment condition. We return \(c\) and its assignment.
The set of vertices in layer \(i\) of the sparsified graph:
Each layer has exactly \(|V|\) vertices:
We define the injection \(f : V \to \mathrm{SparsifiedVertex}(S)\) by \(f(v) = (i, v)\). This is injective because if \(f(v) = f(w)\) then the vertex components must be equal, so \(v = w\). We then show that \(\mathrm{layerVertices}(S, i)\) equals \(\mathrm{univ}.image(f)\): a layered vertex \(\ell v\) has layer \(i\) if and only if it is in the image of \(f\) (by decomposing \(\ell v\) and using the layer equality). The result follows from \(|\mathrm{univ}.image(f)| = |\mathrm{univ}|\) by injectivity of \(f\).
The embedding \(V \hookrightarrow \mathrm{SparsifiedVertex}(S)\) that sends each vertex \(v\) to its layer-\(0\) copy \(\mathrm{ofOriginal}(v)\). This is injective: if \(\mathrm{ofOriginal}(v) = \mathrm{ofOriginal}(w)\), then \(v = w\) by the second component of the equality.
The embedding of the original graph into layer \(0\) preserves adjacency: if \(G.\mathrm{Adj}(v, w)\), then \(\mathrm{isIntraLayerEdge}(S, \mathrm{embedOriginal}(v), \mathrm{embedOriginal}(w))\).
By simplification: both embedded vertices have layer \(0\) (so the layer equality holds), and the vertex components are the original vertices \(v\) and \(w\), which are adjacent by hypothesis.
A graph \(G\) with cycles has a valid assignment with cycle-degree bound \(c\) and \(R\) layers if there exists a cycle-layer assignment such that for every edge \(e\), \(\mathrm{cycleDegree}(G.\mathrm{cycles}, e) \leq c\).
If the cycle-degree bound \(c\) is already satisfied for all edges (i.e., \(\forall e,\; \mathrm{cycleDegree}(G.\mathrm{cycles}, e) \leq c\)), then a valid assignment exists with \(R = 0\) layers.
We take \(R = 0\) and the trivial assignment sending every cycle to layer \(0\) (the unique element of \(\mathrm{Fin}(1)\)). The cycle-degree constraint is satisfied by hypothesis.
A layer bound for a graph \(G\) with cycle-degree bound \(c\) consists of:
a number of layers \(R \in \mathbb {N}\),
a proof that a valid cycle-layer assignment exists with \(R\) layers and cycle-degree bound \(c\).
This represents the value \(R_G^c\) from the paper.
A class asserting that a graph \(G\) satisfies the Freedman–Hastings decongestion bound. This states:
There exists a layer bound \(\mathrm{lb}\) with \(\mathrm{lb}.\mathrm{numLayers} \leq (\log _2 |V| + 1)^2 \cdot (\mathrm{maxDegree} + 1)\).
The cycle-degree bound \(c {\gt} 0\).
The graph has bounded degree: for all \(v \in V\), \(|G.\mathrm{incidentEdges}(v)| \leq \mathrm{maxDegree}\).
For graphs satisfying the Freedman–Hastings bound, there exists a valid layer assignment with \(R = O(\log ^2 n)\) where \(n = |V|\). Specifically, there exists \(R \in \mathbb {N}\) such that:
From the \(\mathrm{HasDecongestionBound}\) instance, we obtain a layer bound \(\mathrm{lb}\) and its bound \(\mathrm{lb}.\mathrm{numLayers} \leq (\log _2 |V| + 1)^2 \cdot (\mathrm{maxDegree} + 1)\). We take \(R = \mathrm{lb}.\mathrm{numLayers}\). The valid assignment comes from \(\mathrm{lb}.\mathrm{valid}\). The inequality follows by commutativity of multiplication: \((\log _2 |V| + 1)^2 \cdot (\mathrm{maxDegree} + 1) = (\mathrm{maxDegree} + 1) \cdot (\log _2 |V| + 1)^2\).