This follows directly by integer arithmetic from the hypothesis \(2N \leq \Delta \cdot N\).

We apply monotonicity of multiplication on the left by \(2\) and on the right by \(W\). It suffices to show \(R + 1 \leq K \cdot (\log _2 W)^2 + 1\), which follows by integer arithmetic from the hypothesis \(R \leq K \cdot (\log _2 W)^2\).

Rewriting \((R+1) \cdot W / W = R + 1\) using the cancellation lemma (since \(W {\gt} 0\)), the result follows by integer arithmetic from \(R \leq K \cdot (\log _2 W)^2\).

The four conclusions are established as a conjunction:

1. All desiderata follow directly from construction_satisfies_all_desiderata applied to \(G\), the cycles, checks, \(\Delta \), the \(Z\)-support adjacency hypothesis, the sufficient expansion, the low-weight cycle basis, and the constant degree bound.

2. The \(O(\log ^2 W)\) layer count follows from decongestion_log_squared applied to \(G\), \(\Delta \), the constant degree, connectivity, vertex count bound, the positivity of the expansion constant, the cycles, \(c\), the cycle rank property, and the König-Freedman-Hastings bound.

3. The edge overhead bound \(2|E| \leq \Delta \cdot |V|\) follows from constant_degree_bounds_edges.

4. The expansion-based boundary bound follows from expansion_gives_boundary_bound applied to each nonempty subset \(S\) with \(2|S| \leq |V|\).

The bound on Gauss law check weights follows from gaussLaw_checks_weight_bounded applied to \(G\), \(\Delta \), and the constant degree hypothesis. The bound on flux check weights follows from flux_checks_weight_bounded applied to \(G\), the cycles, \(4\), and the low-weight cycle basis hypothesis.

The distance bound \(d \leq d^*\) follows directly from deformed_distance_ge_d_sufficient_expansion applied to \(G\), the cycles, checks, the original code, the identification of check indices, the deformed code data, the cycle parity condition, the commutativity of checks, connectivity, the vertex count bound, the exactness conditions, the sufficient expansion, the logical operator hypothesis, and the existence of deformed logicals. The edge overhead bound follows from constant_degree_bounds_edges.

We prove each of the seven conclusions:

1. All desiderata follow from construction_satisfies_all_desiderata applied to \(G\), the cycles, checks, \(\Delta \), the \(Z\)-support adjacency, the sufficient expansion, the low-weight cycle basis, and the constant degree.

2. The layer count bound follows from decongestion_log_squared applied to \(G\), \(\Delta \), the constant degree, connectivity, vertex count bound, positivity of the expansion constant, the cycles, \(c\), the cycle rank property, and the König-Freedman-Hastings bound inputs.

3. The edge overhead bound \(2|E| \leq \Delta \cdot |V|\) follows from constant_degree_bounds_edges.

4. The distance preservation \(d \leq d^*\) follows from deformed_distance_ge_d_sufficient_expansion applied with the original code, the identification of check indices, the deformed code data, the cycle parity condition, the commutativity of checks, connectivity, the vertex count bound, the exactness conditions, the sufficient expansion, the logical operator hypothesis, and the existence of deformed logicals.

5. The Gauss law check weight bound follows from gaussLaw_checks_weight_bounded for each vertex \(v\).

6. The flux check weight bound follows from flux_checks_weight_bounded for each cycle \(p\).

7. For the vertex overhead, let \(R \leq K \cdot (\log _2 W)^2/c\). We apply monotonicity of multiplication on the right by \(W\), and the bound \(R + 1 \leq K \cdot (\log _2 W)^2/c + 1\) follows by integer arithmetic.

We first establish that \(R + 1 \leq K \cdot (\log _2 W)^2/c + 1\) by integer arithmetic from \(R \leq K \cdot (\log _2 W)^2/c\). Then \(\Delta \cdot (R+1) \cdot W \leq \Delta \cdot (K \cdot (\log _2 W)^2/c + 1) \cdot W\) by monotonicity of multiplication on the left by \(\Delta \) and on the right by \(W\). The result follows by integer arithmetic combining with the hypothesis \(2|E| \leq \Delta \cdot (R+1) \cdot W\).

The codespace dimension change follows directly from codespace_dimension_change_after_gauging applied to \(G\), the cycles, checks, the deformed code data, the cycle parity condition, the commutativity of checks, \(n\), \(k\), the cardinality identification, the dimension formula, \(k \geq 1\), and the cycle rank property. The edge overhead bound follows from constant_degree_bounds_edges.

This follows by integer arithmetic from \(R \leq K \cdot (\log _2 W)^2/c\).

From constant_degree_bounds_edges, we have \(2|E| \leq \Delta \cdot |V|\). Then \(2(|V| + |E|) = 2|V| + 2|E| \leq 2|V| + \Delta \cdot |V| = (2 + \Delta ) \cdot |V|\), which follows by nonlinear arithmetic using the distributivity \((2 + \Delta ) \cdot |V| = 2 \cdot |V| + \Delta \cdot |V|\).

We apply monotonicity of multiplication on the right by \(W\). The bound \(R + 1 \leq K \cdot (\log _2 W)^2/c + 1\) follows by integer arithmetic from the hypothesis \(R \leq K \cdot (\log _2 W)^2/c\).

We apply monotonicity of multiplication on the left by \(\Delta \) and then on the right by \(W\). The inner bound \(R + 1 \leq K \cdot (\log _2 W)^2/c + 1\) follows by integer arithmetic from the hypothesis.

Rewriting the number of qubits of the deformed code using deformedStabilizerCode_numQubits, which gives \(n_{\text{deformed}} = |V| + |E|\), and applying the edge overhead bound \(2|E| \leq \Delta \cdot |V|\) from constant_degree_bounds_edges, we obtain \(|E| \leq \Delta \cdot |V|/2\) and thus \(n_{\text{deformed}} \leq |V| + \Delta \cdot |V|/2\) by integer arithmetic.