By definition of \(\operatorname {cleanedOp}\) and the multiplication rule for Pauli operators, we simplify using the \(\mathbf{x}\)-vector multiplication formula and pointwise addition. The result follows directly.

This follows by simplification using the definition of \(\operatorname {cleanedOp}\), the Pauli multiplication rule for \(\mathbf{x}\)-vectors, and pointwise addition.

By extensionality, for an arbitrary qubit \(q\), we expand the definition of \(\operatorname {cleanedOp}\) and use the Pauli multiplication rule for \(\mathbf{z}\)-vectors. Since \(\operatorname {gaussSubsetProduct}(G, c)\) is pure \(X\), its \(\mathbf{z}\)-component is zero, and the result follows by simplification using pointwise addition.

Let \(e\) be an arbitrary edge. Rewriting using the cleaned operator X-vector formula on edges, we get \(L'.\mathbf{x}(\operatorname {inr}(e)) + \delta (c)(e)\). By the hypothesis \(\delta (c)(e) = L'.\mathbf{x}(\operatorname {inr}(e))\), this equals \(L'.\mathbf{x}(\operatorname {inr}(e)) + L'.\mathbf{x}(\operatorname {inr}(e)) = 0\) over \(\mathbb {Z}/2\mathbb {Z}\).

We unfold the symplectic inner product and decompose the sum over \(V \oplus E\) into vertex and edge contributions using \(\sum _{V \oplus E} = \sum _V + \sum _E\).

For the edge contribution: each summand involves \(\bar{L}.\mathbf{x}(\operatorname {inr}(e))\), which is zero by hypothesis, and the \(\mathbf{x}\)-component of the deformed check on edges, which can be simplified using the definitions. The entire edge sum equals zero.

For the vertex contribution: by the definitions of \(\operatorname {restrictToV}\) and \(\operatorname {deformedOriginalChecks}\), each vertex summand for \(\bar{L}\) agrees with the corresponding summand for \(\operatorname {restrictToV}(\bar{L})\) and \(s_j\).

Combining, we rewrite with the vertex equality and the zero edge sum, and the result follows by adding zero.

Unfolding the definition of Pauli commutation, we rewrite the symplectic inner product \(\langle \operatorname {restrictToV}(\bar{L}), s_j \rangle \) as \(\langle \bar{L}, \tilde{s}_j \rangle \) using the symplectic inner product lemma for operators with no X on edges. The result then follows directly from the commutativity hypothesis \(\langle \bar{L}, \tilde{s}_j \rangle = 0\).

Let \(j\) be an arbitrary check index. We apply the single-check commutation lemma to the hypothesis that \(\bar{L}\) commutes with \(\tilde{s}_j\).

We first rewrite \(\operatorname {gaussSubsetProduct}(G, c)\) as \(\operatorname {gaussSubsetProduct}(G, \mathbf{1}_S)\) where \(S = \{ v \mid c(v) = 1\} \), using the fact that any \(\mathbb {Z}/2\mathbb {Z}\)-valued function equals the indicator of its support. We then rewrite using the product formula \(\operatorname {gaussSubsetProduct}(G, \mathbf{1}_S) = \prod _{v \in S} A_v\). Each \(A_v\) commutes with \(\tilde{s}_j\) by the boundary condition (since each Gauss law operator commutes with each deformed check). Since a product of operators that each commute with \(R\) also commutes with \(R\), the result follows.

Unfolding Pauli commutation and the symplectic inner product, we decompose the sum over \(V \oplus E\). For the edge contribution: the \(\mathbf{z}\)-components of both \(\operatorname {gaussSubsetProduct}(G, c)\) and the Gauss law check vanish on edges (since both are pure \(X\) operators on their respective supports). The edge sum is zero. For the vertex contribution: similarly, both \(\mathbf{z}\)-components vanish on vertices. The vertex sum is also zero. Combining, the total symplectic inner product is \(0 + 0 = 0\).

We rewrite \(\operatorname {gaussSubsetProduct}(G, c)\) as a product of Gauss law operators \(\prod _{v \in S} A_v\) using the indicator and product formula. Each Gauss law operator \(A_v\) commutes with each flux check \(B_p\) by the pairwise commutation relations between Gauss law and flux checks. Since a product of operators commuting with \(B_p\) also commutes with \(B_p\), the result follows.

We case-split on the check index \(a\):

• If \(a = \operatorname {gaussLaw}(v)\): apply the gaussSubsetProduct-commutes-with-Gauss-law result.

• If \(a = \operatorname {flux}(p)\): apply the gaussSubsetProduct-commutes-with-flux result.

• If \(a = \operatorname {deformed}(j)\): apply the gaussSubsetProduct-commutes-with-deformed-check result.

Let \(a\) be an arbitrary check index. The result follows directly from the fact that \(\operatorname {gaussSubsetProduct}(G, c)\) commutes with all deformed code checks.

We rewrite \(\operatorname {gaussSubsetProduct}(G, c)\) as \(\operatorname {gaussSubsetProduct}(G, \mathbf{1}_S)\) where \(S = \{ v \mid c(v) = 1\} \). Then we apply the product formula to express it as \(\prod _{v \in S} A_v\). Since the stabilizer group is a subgroup and each Gauss law operator \(A_v\) is in the stabilizer group of the deformed code, the product is also in the stabilizer group.

We unfold the weight as the cardinality of the support. The support over \(V \oplus E\) decomposes as the disjoint union of the vertex support (mapped via \(\operatorname {inl}\)) and the edge support (mapped via \(\operatorname {inr}\)). We establish this decomposition explicitly by showing that every element of \(V \oplus E\) in the support is either \(\operatorname {inl}(v)\) or \(\operatorname {inr}(e)\). The disjointness follows because \(\operatorname {inl}\) and \(\operatorname {inr}\) have disjoint images. Taking cardinalities of a disjoint union gives the sum of cardinalities.

Rewriting using the vertex-plus-edge weight decomposition, we observe that the vertex contribution equals the weight of \(\operatorname {restrictToV}(P)\) by congruence.

By extensionality on both the \(\mathbf{x}\) and \(\mathbf{z}\) components, this follows by simplification using the definitions of \(\operatorname {restrictToV}\), \(\operatorname {logicalOp}\), and \(\operatorname {logicalOpV}\).

Expanding \(\operatorname {cleanedOp}\), we have \(L' \cdot \operatorname {gaussSubsetProduct}(G, c + \mathbf{1})\). Using the additivity \(\operatorname {gaussSubsetProduct}(G, c + \mathbf{1}) = \operatorname {gaussSubsetProduct}(G, c) \cdot \operatorname {gaussSubsetProduct}(G, \mathbf{1})\) and the identity \(\operatorname {gaussSubsetProduct}(G, \mathbf{1}) = \operatorname {logicalOp}(G)\), together with associativity of multiplication, the result follows.

Rewriting the left-hand side using the complement-equals-multiply-by-logical lemma, then distributing \(\operatorname {restrictToV}\) over multiplication, and replacing \(\operatorname {restrictToV}(\operatorname {logicalOp}(G))\) by \(\operatorname {logicalOpV}\), the result follows.

Suppose for contradiction that \(\operatorname {cleanedOp}(L', c) = L' \cdot \operatorname {gaussSubsetProduct}(G, c) \in \mathcal{S}^*\). Since \(\operatorname {gaussSubsetProduct}(G, c) \in \mathcal{S}^*\), we can recover \(L' = \operatorname {cleanedOp}(L', c) \cdot (\operatorname {gaussSubsetProduct}(G, c))^{-1}\). Since \(\mathcal{S}^*\) is a subgroup, this product is in \(\mathcal{S}^*\), so \(L' \in \mathcal{S}^*\), contradicting \(L'\) being a logical operator (which requires \(L' \notin \mathcal{S}^*\)).

Suppose \(\operatorname {cleanedOp}(L', c) = L' \cdot \operatorname {gaussSubsetProduct}(G, c) = 1\). Then multiplying both sides on the right by \(\operatorname {gaussSubsetProduct}(G, c)\) and using self-inverseness (in \(\mathbb {Z}/2\mathbb {Z}\) Pauli algebra, \(P^2 = I\)), we obtain \(L' = \operatorname {gaussSubsetProduct}(G, c)\). Since \(\operatorname {gaussSubsetProduct}(G, c) \in \mathcal{S}^*\), we get \(L' \in \mathcal{S}^*\), contradicting \(L'\) being a logical operator.

We verify the three conditions for being a logical operator:

1. Centralizer membership: For any check index \(a\), unfolding Pauli commutation and using the symplectic inner product multiplicativity \(\langle P \cdot Q, R \rangle = \langle P, R \rangle + \langle Q, R \rangle \), the commutation of \(L'\) with all checks and the centralizer membership of \(\operatorname {gaussSubsetProduct}(G, c)\) give \(\langle L', \text{check}_a \rangle + \langle \operatorname {gaussSubsetProduct}(G, c), \text{check}_a \rangle = 0 + 0 = 0\).

2. Not in stabilizer group: This follows from the cleaned-operator-not-in-stabilizer-group theorem.

3. Not identity: This follows from the cleaned-operator-not-identity theorem.

Both cleaned operators \(\bar{L}_0 = \operatorname {cleanedOp}(L', c)\) and \(\bar{L}_1 = \operatorname {cleanedOp}(L', c + \mathbf{1})\) have no X-support on edges. For \(\bar{L}_0\), this follows from \(\delta (c) = \operatorname {edgeXSupport}(L')\). For \(\bar{L}_1\), since \(\delta (\mathbf{1}) = 0\) (the all-ones vector is in the kernel of the coboundary map), \(\delta (c + \mathbf{1}) = \delta (c) + 0 = \delta (c) = \operatorname {edgeXSupport}(L')\).

Both cleaned operators are logicals of the deformed code, so they commute with all deformed checks. Since they have no X on edges, their restrictions commute with all original checks, placing both restrictions in the centralizer of the original code.

The two restrictions differ by \(\operatorname {logicalOpV}\): \(\operatorname {restrictToV}(\bar{L}_1) = \operatorname {restrictToV}(\bar{L}_0) \cdot \operatorname {logicalOpV}\).

Suppose for contradiction that neither restriction is a logical. Each is in the centralizer but not a logical, so each is either in the original stabilizer group or equals \(1\). We consider four cases:

• Both in the stabilizer group: their quotient \(\operatorname {logicalOpV}\) would be in the stabilizer group, contradicting \(\operatorname {logicalOpV}\) being a logical.

• First in stabilizer, second is \(1\): then \(\operatorname {restrictToV}(\bar{L}_0) \cdot \operatorname {logicalOpV} = 1\), so \(\operatorname {logicalOpV} = \operatorname {restrictToV}(\bar{L}_0) \in \mathcal{S}\), a contradiction.

• First is \(1\), second in stabilizer: then \(\operatorname {logicalOpV} = \operatorname {restrictToV}(\bar{L}_1) \in \mathcal{S}\), a contradiction.

• Both equal \(1\): then \(\operatorname {logicalOpV} = 1\), contradicting \(\operatorname {logicalOpV}\) being a logical.

All cases lead to contradiction.

Unfolding the symplectic inner product and decomposing the sum over \(V \oplus E\): the vertex contribution is zero because the flux check \(B_p\) has both \(\mathbf{x}\) and \(\mathbf{z}\) components equal to zero on vertices (as \(B_p\) is supported only on edges). After adding zero, the edge sum is rewritten using the definitions of \(\operatorname {fluxChecks}\) and \(\operatorname {secondCoboundaryMap}\). Each edge summand matches by case analysis on whether the edge belongs to the cycle, giving the desired equality.

We must show \(\delta _2(\operatorname {edgeXSupport}(L')) = 0\). By extensionality, let \(p\) be an arbitrary cycle. Since \(L'\) is a logical of the deformed code, it commutes with the flux check \(B_p\), meaning \(\langle L', B_p \rangle = 0\). By the symplectic-inner-product-equals-second-coboundary theorem, \(\delta _2(\operatorname {edgeXSupport}(L'))(p) = \langle L', B_p \rangle = 0\).

Let \(S = \{ v \mid c(v) \neq 0\} \). We show that the edge boundary \(\partial _E(S)\) equals the set of coboundary-support edges (mapped via the subtype embedding) by establishing a bijection.

For the forward direction: given an edge \(e = s(a,b) \in \partial _E(S)\) (meaning \(|s(a,b).\operatorname {toFinset} \cap S| = 1\)), we show \(\delta (c)(e) \neq 0\). If \(\delta (c)(e) = 0\), then \(c(a) + c(b) = 0\) in \(\mathbb {Z}/2\mathbb {Z}\), so \(c(a) = c(b)\). If both are nonzero, the intersection has cardinality \(2\), contradicting \(|s(a,b).\operatorname {toFinset} \cap S| = 1\). If both are zero, the intersection is empty, also a contradiction.

For the backward direction: given \(e = s(a,b)\) with \(\delta (c)(e) = c(a) + c(b) \neq 0\), we have \(c(a) \neq c(b)\). In \(\mathbb {Z}/2\mathbb {Z}\), this means exactly one is \(0\) and the other is \(1\), so \(|s(a,b).\operatorname {toFinset} \cap S| = 1\), placing \(e\) in \(\partial _E(S)\).

We apply monotonicity of cardinality. For any edge \(e\) with \(\delta (c)(e) \neq 0\), substituting \(\delta (c) = \operatorname {edgeXSupport}(L')\) gives \(L'.\mathbf{x}(\operatorname {inr}(e)) \neq 0\), which implies the disjunction \(L'.\mathbf{x}(\operatorname {inr}(e)) \neq 0 \lor L'.\mathbf{z}(\operatorname {inr}(e)) \neq 0\).

The support of \(c + \mathbf{1}\) is the complement of the support of \(c\): for any \(v\), \(c(v) + 1 \neq 0\) if and only if \(c(v) = 0\) (since in \(\mathbb {Z}/2\mathbb {Z}\), if \(c(v) = 1\) then \(c(v) + 1 = 0\), and if \(c(v) = 0\) then \(c(v) + 1 = 1 \neq 0\)). The result follows from \(|S| + |S^c| = |V|\) for any \(S \subseteq V\).

By linearity of \(\delta \), \(\delta (c + \mathbf{1}) = \delta (c) + \delta (\mathbf{1})\). The all-ones vector \(\mathbf{1}\) is in the kernel of the coboundary map, so \(\delta (\mathbf{1}) = 0\). Thus \(\delta (c + \mathbf{1}) = \delta (c) + 0 = \delta (c)\).

By extensionality on both \(\mathbf{x}\) and \(\mathbf{z}\) components, this follows by simplification using the definitions of \(\operatorname {restrictToV}\), \(\operatorname {deformedOriginalChecks}\), \(\operatorname {deformedCheck}\), and \(\operatorname {deformedOpExt}\).

Since \(\delta \in \operatorname {im}(\partial _2)\), there exists \(\sigma : C \to \mathbb {Z}/2\mathbb {Z}\) with \(\delta = \partial _2(\sigma )\). We decompose \(\sigma = \sum _c \sigma (c) \cdot \mathbf{e}_c\) and apply the linearity of \(\partial _2\) to get \(\partial _2(\sigma ) = \sum _c \sigma (c) \cdot \partial _2(\mathbf{e}_c)\). Over \(\mathbb {Z}/2\mathbb {Z}\), \(\sigma (c) \cdot x\) equals \(x\) if \(\sigma (c) = 1\) and \(0\) otherwise, so the sum reduces to \(\sum _{c : \sigma (c) \neq 0} \mathbf{1}_{\text{cycle}(c)}\), where \(\mathbf{1}_{\text{cycle}(c)}\) is the indicator of cycle \(c\).

We show that \(\operatorname {pureZEdgeOp}\) of a sum equals the product of individual \(\operatorname {pureZEdgeOp}\)’s (by induction using the multiplication formula). Each \(\operatorname {pureZEdgeOp}(\mathbf{1}_{\text{cycle}(c)})\) equals the flux check \(B_c\), which is in the stabilizer group. Since the stabilizer group is closed under finite products, the result follows.

Let \(\bar{L} = \operatorname {cleanedOp}(L', c)\). Since \(\delta (c) = \operatorname {edgeXSupport}(L')\), \(\bar{L}\) has no X-support on edges. Since \(\operatorname {restrictToV}(\bar{L}) = 1\), we have \(\bar{L}.\mathbf{x}(\operatorname {inl}(v)) = 0\) and \(\bar{L}.\mathbf{z}(\operatorname {inl}(v)) = 0\) for all \(v\). Combined with zero X on edges, \(\bar{L} = \operatorname {pureZEdgeOp}(\delta )\) where \(\delta (e) = \bar{L}.\mathbf{z}(\operatorname {inr}(e))\).

Since \(\bar{L}\) is a logical of the deformed code, it commutes with all Gauss law checks. Computing the symplectic inner product \(\langle \bar{L}, A_v \rangle \) explicitly, the vertex contribution is zero (both components vanish on vertices) and the edge contribution reduces to \(\partial (\delta )(v)\). Thus \(\partial (\delta ) = 0\), i.e., \(\delta \in \ker (\partial )\).

By boundary exactness, \(\delta \in \operatorname {im}(\partial _2)\), so \(\operatorname {pureZEdgeOp}(\delta ) \in \mathcal{S}^*\). But \(\bar{L} = \operatorname {pureZEdgeOp}(\delta )\) is a logical and cannot be in \(\mathcal{S}^*\). Contradiction.

We proceed by induction on the structure of the stabilizer group (closure induction):

• Generator case: If \(s = s_j\) is an original check, we take \(\tilde{S} = \tilde{s}_j\) (the deformed original check). Then \(\tilde{s}_j \in \mathcal{S}^*\), \(\operatorname {restrictToV}(\tilde{s}_j) = s_j\), and \(\tilde{s}_j\) has no X on edges (by the definition of \(\operatorname {deformedOpExt}\)).

• Identity: Take \(\tilde{S} = 1\), which trivially satisfies all conditions.

• Product: Given \(\tilde{S}_1\) and \(\tilde{S}_2\) lifting \(S_1\) and \(S_2\) respectively, take \(\tilde{S} = \tilde{S}_1 \cdot \tilde{S}_2\). The product is in \(\mathcal{S}^*\) (subgroup closure), the restriction distributes over multiplication, and the no-X-on-edges condition is preserved under multiplication (since \(0 + 0 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\)).

• Inverse: Given \(\tilde{S}\) lifting \(S\), take \(\tilde{S}^{-1}\). In the \(\mathbb {Z}/2\mathbb {Z}\) Pauli algebra, \(P^{-1} = P\), so all conditions are inherited.

Let \(\bar{L} = \operatorname {cleanedOp}(L', c)\), which is a logical of the deformed code with no X on edges. We lift \(\operatorname {restrictToV}(\bar{L})\) to a deformed stabilizer \(\tilde{S}\) with \(\operatorname {restrictToV}(\tilde{S}) = \operatorname {restrictToV}(\bar{L})\) and no X on edges.

Consider \(Q = \bar{L} \cdot \tilde{S}\). Since \(\operatorname {restrictToV}(\bar{L}) = \operatorname {restrictToV}(\tilde{S})\) and Pauli operators are self-inverse, \(\operatorname {restrictToV}(Q) = 1\). Also \(Q\) has no X on edges.

We case-split:

• If \(Q = 1\): then \(\bar{L} = \tilde{S} \in \mathcal{S}^*\), contradicting \(\bar{L}\) being a logical.

• If \(Q \in \mathcal{S}^*\): then \(\bar{L} = Q \cdot \tilde{S} \in \mathcal{S}^*\), contradiction.

• Otherwise: \(Q\) is in the centralizer of the deformed code (since both \(\bar{L}\) and \(\tilde{S}\) commute with all checks), is not in \(\mathcal{S}^*\), and is not \(1\). So \(Q\) is a logical of the deformed code. Since \(Q\) has \(\operatorname {restrictToV}(Q) = 1\) and no X on edges, \(Q = \operatorname {pureZEdgeOp}(\delta _Q)\). By the same argument as in the identity case (commutation with Gauss law checks gives \(\partial (\delta _Q) = 0\), boundary exactness gives \(\delta _Q \in \operatorname {im}(\partial _2)\)), \(Q \in \mathcal{S}^*\). Contradiction.

Let \(\bar{L} = \operatorname {cleanedOp}(L', c)\), which is a logical of the deformed code with no X on edges. Since \(\bar{L}\) commutes with all deformed checks and has no X on edges, its restriction \(\operatorname {restrictToV}(\bar{L})\) is in the centralizer of the original code.

Suppose for contradiction that \(\operatorname {restrictToV}(\bar{L})\) is not a logical. Being in the centralizer, it must be either in the original stabilizer group or equal to \(1\):

• If it is in the stabilizer group: this contradicts the cleaned-not-stabilizer-on-V theorem.

• If it equals \(1\): this contradicts the cleaned-not-identity-on-V theorem.

Both cases lead to contradiction, so \(\operatorname {restrictToV}(\bar{L})\) must be a logical of the original code.

By Step 2, \(\operatorname {edgeXSupport}(L') \in \ker (\delta _2)\). By exactness of the first sequence (\(\ker (\delta _2) \subseteq \operatorname {im}(\delta )\)), there exists \(c_0\) with \(\delta (c_0) = \operatorname {edgeXSupport}(L')\). By the any-cleaning-gives-logical theorem, \(\operatorname {restrictToV}(\operatorname {cleanedOp}(L', c_0))\) is a logical.

If \(2 \cdot |\operatorname {supp}(c_0)| \leq |V|\), take \(c = c_0\). Otherwise, let \(c_1 = c_0 + \mathbf{1}\). Then \(\delta (c_1) = \delta (c_0)\) (since \(\delta (\mathbf{1}) = 0\)), and any cleaning gives a logical. The support partition \(|\operatorname {supp}(c_0)| + |\operatorname {supp}(c_1)| = |V|\) together with \(2 \cdot |\operatorname {supp}(c_0)| {\gt} |V|\) gives \(2 \cdot |\operatorname {supp}(c_1)| \leq |V|\). Take \(c = c_1\).

We case-split on whether \(h \geq 1\).

If \(h \geq 1\): then \(\min (h, 1) = 1\). From condition (2), \(|S| \leq h \cdot |S| \leq |\partial |\). Combined with conditions (1) and (3), \(w + |S| \geq d + |\partial |\) and \(|\partial | \leq w\), so \(d \leq w\).

If \(h {\lt} 1\): then \(\min (h, 1) = h\). We sub-case on \(|S| \leq d\) vs. \(|S| {\gt} d\).

• If \(|S| \leq d\): From condition (1), \(w \geq d + |\partial | - |S| \geq d + h \cdot |S| - |S| = d + (h-1) \cdot |S|\). Since \(h - 1 {\lt} 0\) and \(|S| \leq d\), \((h-1) \cdot |S| \geq (h-1) \cdot d\), so \(w \geq d + (h-1) \cdot d = h \cdot d\).

• If \(|S| {\gt} d\): From condition (3), \(w \geq |\partial | \geq h \cdot |S| {\gt} h \cdot d\).

We show that the support of the cleaned restriction is contained in the union of the support of \(\operatorname {restrictToV}(L')\) and the support of \(c\), then apply monotonicity and the union cardinality bound.

For any vertex \(v\) in the support of \(\operatorname {restrictToV}(\operatorname {cleanedOp}(L', c))\): either its \(\mathbf{x}\)-component is nonzero or its \(\mathbf{z}\)-component is nonzero. If the \(\mathbf{x}\)-component is nonzero and \(c(v) = 0\), the cleaning does not affect it, so \(v\) is in the support of \(\operatorname {restrictToV}(L')\). If \(c(v) \neq 0\), then \(v\) is in the support of \(c\). If the \(\mathbf{z}\)-component is nonzero, since cleaning preserves \(\mathbf{z}\)-vectors, \(v\) is in the support of \(\operatorname {restrictToV}(L')\).

By the WLOG construction, we obtain \(c\) with \(\delta (c) = \operatorname {edgeXSupport}(L')\), such that \(\operatorname {restrictToV}(\operatorname {cleanedOp}(L', c))\) is a logical of the original code and \(2|\operatorname {supp}(c)| \leq |V|\).

Let \(S = |\operatorname {supp}(c)|\) and \(E_{\text{supp}} = |\{ e \mid L'.\mathbf{x}(\operatorname {inr}(e)) \neq 0 \lor L'.\mathbf{z}(\operatorname {inr}(e)) \neq 0\} |\).

We verify the hypotheses of the core arithmetic lemma:

1. \(\operatorname {wt}(L') + S \geq d + E_{\text{supp}}\): The cleaned restriction is a logical, so its weight \(\geq d\). By the vertex-weight-plus-support bound, \(\operatorname {wt}(\operatorname {restrictToV}(L')) + S \geq \operatorname {wt}(\text{cleaned restriction}) \geq d\). By the weight decomposition, \(\operatorname {wt}(L') = \operatorname {wt}(\operatorname {restrictToV}(L')) + E_{\text{supp}}\).

2. \(h(G) \cdot S \leq E_{\text{supp}}\): If \(c = 0\) then \(S = 0\) and this holds trivially. Otherwise, by the Cheeger constant definition, \(h(G) \cdot S \leq |\partial _E(\operatorname {supp}(c))|\), which equals the coboundary support size (by the coboundary-equals-edge-boundary theorem), which is \(\leq E_{\text{supp}}\).

3. \(E_{\text{supp}} \leq \operatorname {wt}(L')\): This follows from the weight decomposition.

Applying the arithmetic lemma yields \(\operatorname {wt}(L') \geq \min (h(G), 1) \cdot d\).

By the per-operator bound, \(\operatorname {wt}(L') \geq \min (h(G), 1) \cdot d\). Since \(h(G) \geq 1\), \(\min (h(G), 1) = 1\), so \(\operatorname {wt}(L') \geq 1 \cdot d = d\).

The deformed code distance is \(d^* = \inf \{ \operatorname {wt}(P) \mid P \text{ is a logical of the deformed code}\} \). The set of weights is nonempty by hypothesis. For every weight \(w\) in this set with witnessing logical \(P\), the per-operator bound gives \(w = \operatorname {wt}(P) \geq \min (h(G), 1) \cdot d\).

Taking the ceiling of \(\min (h(G), 1) \cdot d\) and using the property that \(x \leq \lceil x \rceil \) for reals, together with \(\lceil x \rceil \leq w\) for all \(w\) in the set, we obtain \(\lceil \min (h(G), 1) \cdot d \rceil \leq \inf \{ w\} = d^*\). Thus \(\min (h(G), 1) \cdot d \leq d^*\).

By the deformed code distance bound, \(\min (h(G), 1) \cdot d \leq d^*\). Since \(h(G) \geq 1\), \(\min (h(G), 1) = 1\), so \(1 \cdot d = d \leq d^*\).