This follows directly from the constant degree edge bound (Theorem 378).

From the edge count upper bound we have \(2|E| \le \Delta \cdot |V|\). The result follows by integer arithmetic (dividing both sides by \(2\)).

From the hypothesis \(|C| + |V| = |E| + 1\) and \(|V| {\gt} 0\), the result follows by integer arithmetic (\(|C| = |E| + 1 - |V| \le |E|\)).

We first establish \(|C| \le |E|\) from the cycle rank property. Then we apply the edge count half bound \(|E| \le \Delta \cdot |V| / 2\). The result follows by integer arithmetic.

This follows from the definition of \(M\) as the supremum of \(d_e\) over all edges \(e\), applied at the element \(e \in \operatorname {univ}\).

We apply \(\operatorname {sup\_ le}\): for each edge \(e\), we have \(d_e \le |C|\) by Theorem 442.

We use the one-per-layer construction: let \(\operatorname {equiv} : C \simeq \operatorname {Fin}(|C|)\) be the canonical equivalence and assign each cycle \(c\) to layer \(\operatorname {equiv}(c)\). Then \(R = |C|\) and \(R \le |C|\) trivially. For the layer-cycle-degree bound, observe that each layer contains at most one cycle (by injectivity of \(\operatorname {equiv}\)), so the per-layer edge-cycle degree is at most \(1 \le b\).

Define the packed assignment \(f(\gamma ) = \lfloor f_0(\gamma ) / c \rfloor \). This maps into \(\operatorname {Fin}(M/c + 1)\) since \(f_0(\gamma ) / c \le M / c\).

To verify the per-layer bound \(c\), fix an edge \(e\) and a packed layer \(i\). Let \(S\) be the set of cycles \(\gamma \) with \(f(\gamma ) = i\) and \(e \in \gamma \). We construct an injection \(\varphi : S \to \operatorname {Fin}(c)\) by \(\varphi (\gamma ) = f_0(\gamma ) \bmod c\).

To show \(\varphi \) is injective on \(S\): suppose \(\gamma _1, \gamma _2 \in S\) with \(f_0(\gamma _1) \bmod c = f_0(\gamma _2) \bmod c\). Since both are in layer \(i\), we have \(f_0(\gamma _1) / c = f_0(\gamma _2) / c\). By the division algorithm (combining the equal quotients and equal remainders), \(f_0(\gamma _1) = f_0(\gamma _2)\), so \(f_0(\gamma _1) = f_0(\gamma _2)\) as elements of \(\operatorname {Fin}(M+1)\). Since the original assignment \(f_0\) has per-layer bound \(1\), the set of cycles in the original layer \(f_0(\gamma _1)\) passing through \(e\) has cardinality at most \(1\). Both \(\gamma _1\) and \(\gamma _2\) belong to this set, so \(\gamma _1 = \gamma _2\).

Therefore \(|S| \le |\operatorname {Fin}(c)| = c\).

We obtain \(f\) from the layer packing lemma (Theorem 459) applied to \(f_0\), \(M\), and \(c\). This gives a layer assignment with per-layer bound \(c\) using \(M/c + 1\) layers, hence \(R = M/c \le M/c\).

We unfold \(\operatorname {minLayers}\) as \(\operatorname {Nat.find}\). By the one-per-layer construction, there exists a layer assignment with \(|C|\) layers achieving any positive per-layer bound. Applying \(\operatorname {Nat.find\_ le}\) at \(|C|\) gives the result.

We have \(R_G^b \le |C|\) from the decongestion layers bound, and \(|C| \le \Delta \cdot |V| / 2\) from the cycle count bound. The result follows by integer arithmetic.

This follows directly from the Cheeger inequality for edge boundaries (Theorem 79), applied to the set \(B(v,r)\) with \(h = h(G)\).

By extensionality, for any \(u\) we have \(u \in B(v, |V|-1)\) if and only if \(\operatorname {dist}_G(v, u) \le |V| - 1\), which holds by the connected distance bound.

Part (1) follows from the connected diameter bound (Theorem ??). Part (2) follows from the BFS ball growth from expansion (Theorem 464), noting that \(B(v,r)\) is nonempty since it always contains \(v\).

We obtain a layer assignment \(f\) from the one-per-layer construction with \(R = |C|\) layers. The bound \(R \le \Delta \cdot |V| / 2\) follows from the cycle count bound (since \(|V| \ge 2 {\gt} 0\)).

We take \(K = \Delta \), which is positive by hypothesis. For any graph \(G'\) satisfying the conditions, we apply the constructive coarse bound to obtain \(R\) and \(f\) with \(R \le \Delta \cdot W / 2\). Since \(\Delta \cdot W / 2 \le \Delta \cdot W\) (by \(\operatorname {Nat.div\_ le\_ self}\)), the result follows.

We apply the greedy packing bound (Theorem 460) to \(f_0\), \(M\), and \(c\), obtaining \(R\) and \(f\) with \(R \le M/c\). Since \(M \le K \cdot \log _2^2(W)\), we have \(R \le M/c \le K \cdot \log _2^2(W) / c\) by monotonicity of integer division.

We apply the main decongestion lemma (Theorem 469) to obtain \(R \le K \cdot \log _2^2(W) / c\). Since \(K \cdot \log _2^2(W) / c \le K \cdot \log _2^2(W)\) by \(\operatorname {Nat.div\_ le\_ self}\), the result follows.

This follows from \(R \le K \cdot \log _2^2(W)\) by monotonicity of multiplication on the right: \((R+1) \cdot W \le (K \cdot \log _2^2(W) + 1) \cdot W\).

This follows from \(R \le K \cdot \log _2^2(W)\) by monotonicity of multiplication on the right.

Part (1) follows from the constructive coarse bound (Theorem 467). Part (2) follows from the greedy packing bound (Theorem 460). Part (3) follows from the cycle count bound (Theorem 454), noting \(W \ge 2 {\gt} 0\). Part (4) follows from the expander diameter bound from BFS (Theorem 466), noting \(W \ge 2 {\gt} 0\).