19 Def 6: Cycle-Sparsified Graph
The cycle-sparsified graph (decongested graph) \(\overline{\overline{G}}\) with cycle-degree bound \(c\) is constructed from a connected graph \(G\) with a chosen generating set of cycles by creating multiple layers and distributing cycles across them, then adding cellulation (triangulation) edges via a zigzag pattern to decompose high-degree cycles into triangles.
The vertex type of the sparsified graph is \(V \times \operatorname {Fin}(R+1)\), where a pair \((v, i)\) represents vertex \(v\) in layer \(i\). Layer \(0\) is the original graph layer.
The original layer is layer \(0\), i.e., \(\operatorname {originalLayer} = \langle 0, \ldots \rangle : \operatorname {Fin}(R+1)\).
The number of vertices in the sparsified graph satisfies
By simplification using the cardinality of the product type \(V \times \operatorname {Fin}(R+1)\), we have \(|V \times \operatorname {Fin}(R+1)| = |\operatorname {Fin}(R+1)| \cdot |V|\), and \(|\operatorname {Fin}(R+1)| = R+1\). The result then follows by commutativity of multiplication.
The set of vertices in layer \(i\) is defined as
For each layer \(i \in \operatorname {Fin}(R+1)\), the number of vertices in that layer equals the number of original vertices:
We rewrite the filter \(\{ p \in V \times \operatorname {Fin}(R+1) \mid p_2 = i\} \) as the product \(V \times \{ i\} \), using extensionality and simplification. The cardinality of this product is \(|V| \cdot |\{ i\} | = |V| \cdot 1 = |V|\).
The embedding of an original vertex \(v \in V\) into the sparsified vertex type is
The function \(\operatorname {embedOriginal} : V \to \operatorname {SparsifiedVertex}(V, R)\) is injective.
Let \(v, w \in V\) and suppose \(\operatorname {embedOriginal}(v) = \operatorname {embedOriginal}(w)\). Then \((v, \operatorname {originalLayer}) = (w, \operatorname {originalLayer})\), so by the extensionality of pairs, the first components are equal: \(v = w\).
Every sparsified vertex \(p \in \operatorname {SparsifiedVertex}(V, R)\) belongs to a unique layer: there exists a unique \(i \in \operatorname {Fin}(R+1)\) such that \(p \in \operatorname {layerVertices}(i)\).
For any \(p = (v, j)\), we take \(i = p_2 = j\). Then \(p \in \operatorname {layerVertices}(j)\) since \(p_2 = j\). For uniqueness, if \(p \in \operatorname {layerVertices}(k)\), then \(p_2 = k\) by the filter condition, so \(k = j\).
For distinct layers \(i \neq j\), the layer vertex sets are disjoint:
We prove disjointness via \(\operatorname {Finset.disjoint\_ left}\). Suppose \(x \in \operatorname {layerVertices}(i)\) and \(x \in \operatorname {layerVertices}(j)\). By the filter conditions, \(x_2 = i\) and \(x_2 = j\), hence \(i = j\), contradicting \(i \neq j\).
An intra-layer edge between sparsified vertices \(p\) and \(q\) is defined by
i.e., \(p\) and \(q\) are in the same layer and the corresponding original vertices are adjacent in \(G\). The original graph edges are replicated in every layer.
An inter-layer edge between sparsified vertices \(p\) and \(q\) is defined by
i.e., they represent the same original vertex in consecutive layers.
The auxiliary recursive function \(\operatorname {zigzagGo}\) takes a vertex array \(\mathit{vs} : \operatorname {Fin}(n) \to V\), left and right indices, a Boolean alternation flag \(\mathit{fromLeft}\), and a fuel parameter. It produces zigzag diagonal pairs by alternating between:
If \(\mathit{fromLeft}\) is true: emit \((\mathit{vs}[\mathit{left}],\; \mathit{vs}[\mathit{right}-1])\) and recurse with \(\mathit{right}' = \mathit{right} - 1\) and flag false.
If \(\mathit{fromLeft}\) is false: emit \((\mathit{vs}[\mathit{right}],\; \mathit{vs}[\mathit{left}+1])\) and recurse with \(\mathit{left}' = \mathit{left} + 1\) and flag true.
The recursion terminates when \(\mathit{right} \le \mathit{left} + 1\) or fuel is exhausted.
Given a list of cycle vertices \([v_1, v_2, \ldots , v_m]\), the zigzag diagonals are the cellulation diagonal pairs produced by the zigzag pattern:
For \(m {\lt} 4\), no diagonals are needed (the polygon is a triangle or simpler). For \(m = 4\) (square), one diagonal \((v_1, v_3)\). For \(m = 5\) (pentagon), two diagonals: \((v_1, v_4)\) and \((v_4, v_2)\).
Formally, if \(|\mathit{vs}| \ge 4\), define \(\mathit{arr}(i) = \mathit{vs}[i]\) and return \(\operatorname {zigzagGo}(\mathit{arr}, 0, |\mathit{vs}|-1, \ldots , \operatorname {true}, |\mathit{vs}|)\); otherwise return the empty list.
A triangulation edge between sparsified vertices \(p\) and \(q\) exists when there is a cycle \(c\) such that:
The cycle \(c\) is assigned to a non-original layer: \(\operatorname {cycleAssignment}(c) \neq \operatorname {originalLayer}\).
Both \(p\) and \(q\) are in the layer assigned to \(c\): \(p_2 = q_2 = \operatorname {cycleAssignment}(c)\).
The pair \((p_1, q_1)\) or \((q_1, p_1)\) is a zigzag diagonal of \(c\)’s vertex list.
If \((p, q)\) is an intra-layer edge, then so is \((q, p)\).
From \(p_2 = q_2\) we get \(q_2 = p_2\) by symmetry, and from \(G.\operatorname {Adj}(p_1, q_1)\) we get \(G.\operatorname {Adj}(q_1, p_1)\) by the symmetry of the simple graph adjacency relation.
If \((p, q)\) is an inter-layer edge, then so is \((q, p)\).
From \(p_1 = q_1\) we get \(q_1 = p_1\), and the disjunction \(p_2 + 1 = q_2 \lor q_2 + 1 = p_2\) is symmetric under swapping \(p\) and \(q\).
If \((p, q)\) is a triangulation edge, then so is \((q, p)\).
Decomposing the hypothesis, we obtain a cycle \(c\) with \(\operatorname {cycleAssignment}(c) \neq \operatorname {originalLayer}\), \(p_2 = \operatorname {cycleAssignment}(c)\), \(q_2 = \operatorname {cycleAssignment}(c)\), and \((p_1, q_1)\) or \((q_1, p_1)\) is a zigzag diagonal. We use the same cycle \(c\), swap the layer equalities, and note that the disjunction on diagonal membership is symmetric.
No vertex has an intra-layer edge to itself: \(\neg \operatorname {isIntraLayerEdge}_G(p, p)\).
Suppose \(\operatorname {isIntraLayerEdge}_G(p, p)\) holds. Then \(G.\operatorname {Adj}(p_1, p_1)\), which contradicts the loopless property of simple graphs.
No vertex has an inter-layer edge to itself: \(\neg \operatorname {isInterLayerEdge}(p, p)\).
Suppose \(\operatorname {isInterLayerEdge}(p, p)\) holds. Then the layer condition gives \(p_2 + 1 = p_2\) or \(p_2 + 1 = p_2\), which is impossible by integer arithmetic (omega).
The adjacency relation of the sparsified graph combines all three edge types:
The sparsified adjacency relation is symmetric: if \(\operatorname {sparsifiedAdj}_G(p, q)\), then \(\operatorname {sparsifiedAdj}_G(q, p)\).
From \(p \neq q\) we get \(q \neq p\). We then case split on the three edge types and apply the respective symmetry theorems: \(\operatorname {isIntraLayerEdge\_ symm}\), \(\operatorname {isInterLayerEdge\_ symm}\), or \(\operatorname {isTriangulationEdge\_ symm}\).
The sparsified adjacency relation is irreflexive: \(\neg \operatorname {sparsifiedAdj}_G(p, p)\).
Suppose \(\operatorname {sparsifiedAdj}_G(p, p)\) holds. The first condition requires \(p \neq p\), which is a contradiction.
The cycle-sparsified graph \(\overline{\overline{G}}\) is defined as a \(\operatorname {SimpleGraph}\) on \(\operatorname {SparsifiedVertex}(V, R)\) with adjacency given by \(\operatorname {sparsifiedAdj}\), symmetry given by \(\operatorname {sparsifiedAdj\_ symm}\), and the loopless property given by \(\operatorname {sparsifiedAdj\_ irrefl}\).
If \(v\) and \(w\) are adjacent in the original graph \(G\), then their embeddings in layer \(0\) are adjacent in the sparsified graph:
We need to show \(p \neq q\) and that an edge type holds. For distinctness, if \((v, \operatorname {originalLayer}) = (w, \operatorname {originalLayer})\) then \(v = w\) by the first component, contradicting the loopless property \(\neg G.\operatorname {Adj}(v, v)\). For the edge type, we use the intra-layer edge: both are in the same layer \(0\) and \(G.\operatorname {Adj}(v, w)\).
For any vertex \(v \in V\) and layer \(i {\lt} R\), the vertices \((v, i)\) and \((v, i+1)\) are adjacent in the sparsified graph.
Let \(i_0 = \langle i, \ldots \rangle \) and \(i_1 = \langle i+1, \ldots \rangle \) be the consecutive layer indices. For distinctness, \((v, i_0) = (v, i_1)\) would imply \(i = i+1\) by the second component, a contradiction. For the edge type, we use the inter-layer edge: \(p_1 = q_1 = v\) and \(i_0 + 1 = i_1\).
If \((p, q)\) is a triangulation edge, then \(p\) and \(q\) are in the same layer: \(p_2 = q_2\).
Decomposing the hypothesis, we get \(p_2 = \operatorname {cycleAssignment}(c)\) and \(q_2 = \operatorname {cycleAssignment}(c)\) for some cycle \(c\). Hence \(p_2 = q_2\).
If \((p, q)\) is a triangulation edge, then \(p_2 \neq \operatorname {originalLayer}\).
From the hypothesis, \(p_2 = \operatorname {cycleAssignment}(c)\) and \(\operatorname {cycleAssignment}(c) \neq \operatorname {originalLayer}\), so \(p_2 \neq \operatorname {originalLayer}\).
Every edge in the sparsified graph is either an intra-layer edge, an inter-layer edge, or a triangulation edge:
This follows directly from the second component of \(\operatorname {sparsifiedAdj}\), which is the disjunction of the three edge types.
If \(p_2 \neq q_2\), then \((p, q)\) is not an intra-layer edge.
Suppose \(\operatorname {isIntraLayerEdge}_G(p, q)\) holds. Then \(p_2 = q_2\), contradicting the hypothesis \(p_2 \neq q_2\).
If \(p_1 \neq q_1\), then \((p, q)\) is not an inter-layer edge.
Suppose \(\operatorname {isInterLayerEdge}(p, q)\) holds. Then \(p_1 = q_1\), contradicting the hypothesis \(p_1 \neq q_1\).
Given an edge \((v, u) \in E(G)\) and a layer index \(i {\lt} R\), the four vertices \((v, i)\), \((v, i{+}1)\), \((u, i{+}1)\), \((u, i)\) form a 4-cycle in the sparsified graph:
First note \(v \neq u\), since \(G.\operatorname {Adj}(v, u)\) and \(G\) is loopless. We verify each of the four edges:
\((v, i) \to (v, i{+}1)\): distinctness holds since \(i \neq i+1\); this is an inter-layer edge with \(p_1 = q_1 = v\) and \(p_2 + 1 = q_2\).
\((v, i{+}1) \to (u, i{+}1)\): distinctness holds since \(v \neq u\); this is an intra-layer edge with same layer \(i+1\) and \(G.\operatorname {Adj}(v, u)\).
\((u, i{+}1) \to (u, i)\): distinctness holds since \(i+1 \neq i\); this is an inter-layer edge with \(p_1 = q_1 = u\) and \(q_2 + 1 = p_2\).
\((u, i) \to (v, i)\): distinctness holds since \(u \neq v\); this is an intra-layer edge with same layer \(i\) and \(G.\operatorname {Adj}(u, v)\) (by symmetry of \(G\)).
Every pair \((a, b)\) in the output of \(\operatorname {zigzagGo}(\mathit{vs}, \mathit{left}, \mathit{right}, \ldots )\) satisfies: \(a = \mathit{vs}(i)\) and \(b = \mathit{vs}(j)\) for some indices \(i, j \in \operatorname {Fin}(n)\).
We proceed by induction on the fuel parameter. In the base case (fuel \(= 0\)), \(\operatorname {zigzagGo}\) returns the empty list, so there is nothing to prove. In the inductive step (fuel \(= k + 1\)), we first check if \(\mathit{right} \le \mathit{left} + 1\); if so, the result is empty. Otherwise, we split on the \(\mathit{fromLeft}\) flag. In the fromLeft case, the emitted pair is \((\mathit{vs}[\mathit{left}], \mathit{vs}[\mathit{right}-1])\), which clearly consists of values of \(\mathit{vs}\); for the remaining pairs we apply the induction hypothesis. The fromRight case is symmetric: the emitted pair is \((\mathit{vs}[\mathit{right}], \mathit{vs}[\mathit{left}+1])\), and the tail follows by the induction hypothesis.
Every vertex appearing in a zigzag diagonal pair belongs to the original cycle list: if \((a, b) \in \operatorname {zigzagDiagonals}(\mathit{vs})\), then \(a \in \mathit{vs}\) and \(b \in \mathit{vs}\).
We unfold \(\operatorname {zigzagDiagonals}\). If \(|\mathit{vs}| {\lt} 4\), the result is empty and there is nothing to prove. Otherwise, we apply \(\operatorname {zigzagGo\_ mem\_ range}\) to obtain indices \(i, j\) with \(\mathit{vs}(i) = a\) and \(\mathit{vs}(j) = b\). Since \(\mathit{vs}(i)\) is the \(i\)-th element of \(\mathit{vs}\), it is a member of the list, and similarly for \(j\).
When the gap is closed (\(\mathit{right} \le \mathit{left} + 1\)), \(\operatorname {zigzagGo}\) returns the empty list.
We case split on fuel. If fuel \(= 0\), \(\operatorname {zigzagGo}\) returns \([]\) by definition. If fuel \(= k + 1\), the first branch of the match checks \(\mathit{right} \le \mathit{left} + 1\), which holds by hypothesis, so it returns \([]\).
When \(\mathit{left} + 1 {\lt} \mathit{right}\) and fuel \(\ge \mathit{right} - \mathit{left} - 1\), the output of \(\operatorname {zigzagGo}\) has exactly \(\mathit{right} - \mathit{left} - 1\) pairs.
We proceed by induction on fuel. The base case (fuel \(= 0\)) is impossible since \(\mathit{right} - \mathit{left} - 1 \le 0\) contradicts \(\mathit{left} + 1 {\lt} \mathit{right}\) (by omega). For the inductive step (fuel \(= k + 1\)), we unfold \(\operatorname {zigzagGo}\) and note the condition \(\mathit{right} \le \mathit{left} + 1\) is false. We split on the \(\mathit{fromLeft}\) flag:
If fromLeft: one pair is emitted and we recurse with \(\mathit{right}' = \mathit{right} - 1\). If \(\mathit{left} + 1 {\lt} \mathit{right} - 1\), the induction hypothesis gives length \(\mathit{right} - 1 - \mathit{left} - 1\), so total length is \(1 + (\mathit{right} - \mathit{left} - 2) = \mathit{right} - \mathit{left} - 1\). If \(\mathit{left} + 1 \ge \mathit{right} - 1\), then \(\operatorname {zigzagGo\_ nil}\) gives length \(0\), so total length is \(1\), and \(\mathit{right} - \mathit{left} - 1 = 1\) by arithmetic.
If not fromLeft: symmetric argument with \(\mathit{left}' = \mathit{left} + 1\).
For a cycle of length \(m \ge 4\), the zigzag cellulation produces exactly \(m - 2\) diagonals:
This corresponds to decomposing an \(m\)-gon into \(m - 2\) triangles.
We unfold \(\operatorname {zigzagDiagonals}\) and note \(|\mathit{vs}| \ge 4\), so the branch selecting the non-empty case is taken. We apply \(\operatorname {zigzagGo\_ exact\_ length}\) with \(\mathit{left} = 0\), \(\mathit{right} = |\mathit{vs}| - 1\), and fuel \(= |\mathit{vs}|\). The conditions \(0 + 1 {\lt} |\mathit{vs}| - 1\) and \(|\mathit{vs}| - 1 - 0 - 1 \le |\mathit{vs}|\) are verified by omega. The result is \((|\mathit{vs}| - 1) - 0 - 1 = |\mathit{vs}| - 2\).
For a cycle \(c\) assigned to layer \(i {\gt} 0\), if \((a, b)\) is a zigzag diagonal of \(c\) with \(a \neq b\), then \((a, i)\) and \((b, i)\) are adjacent in the sparsified graph.
Distinctness \((a, i) \neq (b, i)\) follows from \(a \neq b\) via the first component. The edge is a triangulation edge witnessed by the cycle \(c\): \(\operatorname {cycleAssignment}(c) \neq \operatorname {originalLayer}\), both vertices are in layer \(i = \operatorname {cycleAssignment}(c)\), and \((a, b)\) is a zigzag diagonal of \(c\).
If consecutive vertices \(u, v\) of a cycle are adjacent in \(G\) with \(u \neq v\), then \((u, i)\) and \((v, i)\) are adjacent in the sparsified graph for any layer \(i\).
Distinctness \((u, i) \neq (v, i)\) follows from \(u \neq v\). This is an intra-layer edge: both vertices are in layer \(i\) and \(G.\operatorname {Adj}(u, v)\).
For a cycle \(c\) assigned to layer \(i {\gt} 0\), if \((a, b)\) is a zigzag diagonal of \(c\) and \(x\) is a common neighbor with \(G.\operatorname {Adj}(a, x)\) and \(G.\operatorname {Adj}(b, x)\), then the three vertices \((a, i)\), \((b, i)\), \((x, i)\) form a triangle in the sparsified graph:
This establishes the paper’s claim that cellulation decomposes cycles into triangles of weight \(3\).
The three edges are verified by applying the previous results:
\((a, i) \sim (b, i)\): by \(\operatorname {cellulation\_ adj\_ of\_ diagonal}\) applied to the diagonal \((a, b)\) with \(a \neq b\) and \(\operatorname {cycleAssignment}(c) \neq \operatorname {originalLayer}\).
\((a, i) \sim (x, i)\): by \(\operatorname {cellulation\_ adj\_ of\_ cycle\_ edge}\) applied to \(a \neq x\) and \(G.\operatorname {Adj}(a, x)\).
\((b, i) \sim (x, i)\): by \(\operatorname {cellulation\_ adj\_ of\_ cycle\_ edge}\) applied to \(b \neq x\) and \(G.\operatorname {Adj}(b, x)\).
The edge cycle degree in layer \(i\) counts how many original cycles assigned to layer \(i\) contain a given edge \(e\):
This is the per-layer edge participation count; the purpose of distributing cycles across layers is to make this quantitysmall.
The per-layer cycle-degree bound states that for every edge \(e\) and every layer \(i\), the number of cycles assigned to layer \(i\) containing edge \(e\) is at most \(\mathit{bound}\):
The global edge-cycle degree is the total number of generating cycles containing edge \(e\) across all layers:
The global edge-cycle degree is bounded by the total number of cycles:
This follows from \(\operatorname {Finset.card\_ filter\_ le}\): the cardinality of a filtered subset of \(\operatorname {univ}\) is at most \(|\operatorname {univ}| = |C|\).
If the per-layer cycle-degree bound is \(\mathit{bound}\), then the global edge-cycle degree satisfies:
We unfold \(\operatorname {edgeCycleDegree}\) and rewrite the set \(\{ c \mid e \in \mathit{cycles}(c)\} \) as the union over all layers \(i\) of \(\{ c \mid f(c) = i \land e \in \mathit{cycles}(c)\} \). By extensionality: forward, given \(e \in \mathit{cycles}(c)\), take \(i = f(c)\); backward, the condition \(e \in \mathit{cycles}(c)\) is preserved.
After rewriting, we compute:
where the first inequality is \(\operatorname {Finset.card\_ biUnion\_ le}\), the second uses the per-layer bound hypothesis \(\operatorname {hbound}(e, i)\), and the final equality follows from the sum of a constant over \(\operatorname {Fin}(R'+1)\).
The complete data for a cycle-sparsified graph construction is a structure consisting of:
\(\operatorname {numLayers} : \mathbb {N}\) — the number of additional layers \(R\).
\(\operatorname {cycleAssignment} : C \to \operatorname {Fin}(R+1)\) — assigns each cycle to a layer.
\(\operatorname {cycleVerts} : C \to \operatorname {List}(V)\) — the vertex list of each cycle.
\(\operatorname {cycleBound} : \mathbb {N}\) — the per-layer cycle-degree bound.
\(\operatorname {bound\_ holds}\) — proof that \(\operatorname {LayerCycleDegreeBound}(\mathit{cycles}, \operatorname {cycleAssignment}, \operatorname {cycleBound})\) holds.
Given sparsification data, the associated sparsified graph is
The minimum number of layers \(R_G^c\) for cycle-sparsification with per-layer cycle-degree bound \(\mathit{bound}\) is the smallest \(R\) such that there exists a cycle assignment \(f : C \to \operatorname {Fin}(R+1)\) achieving \(\operatorname {LayerCycleDegreeBound}(\mathit{cycles}, f, \mathit{bound})\). Formally, it is defined using \(\operatorname {Nat.find}\) applied to the existence hypothesis.
The minimum layers value achieves the bound: there exists an assignment \(f : C \to \operatorname {Fin}(\operatorname {minLayers} + 1)\) such that \(\operatorname {LayerCycleDegreeBound}(\mathit{cycles}, f, \mathit{bound})\).
We unfold \(\operatorname {minLayers}\) and apply \(\operatorname {Nat.find\_ spec}\) to the existence hypothesis.
No smaller number of layers suffices: for any \(R' {\lt} \operatorname {minLayers}\),
We unfold \(\operatorname {minLayers}\) and apply \(\operatorname {Nat.find\_ min}\) to \(R' {\lt} \operatorname {minLayers}\).
For lists of length less than \(4\), no diagonals are produced: if \(|\mathit{vs}| {\lt} 4\), then \(\operatorname {zigzagDiagonals}(\mathit{vs}) = []\).
By simplification: the definition of \(\operatorname {zigzagDiagonals}\) checks \(|\mathit{vs}| {\lt} 4\) and returns \([]\) in that case.
The \(\operatorname {zigzagGo}\) function produces at most \(\mathit{fuel}\) diagonal pairs:
We proceed by induction on fuel, generalizing over left, right, and the Boolean flag.
Base case (fuel \(= 0\)): \(\operatorname {zigzagGo}\) returns \([]\), which has length \(0 \le 0\).
Inductive step (fuel \(= k + 1\)): We unfold \(\operatorname {zigzagGo}\). If \(\mathit{right} \le \mathit{left} + 1\), the result is \([]\) with length \(0 \le k + 1\). Otherwise, whether fromLeft or not, one pair is emitted and the tail has length \(\le k\) by the induction hypothesis, so the total length is \(\le k + 1\).