We use the vertex–edge weight decomposition. The edge contribution is zero: for every edge qubit \(e \in E(G)\), the lifted operator satisfies \(\operatorname {xVec}(\operatorname {liftToExtended}(P))(\operatorname {inr}(e)) = 0\) and \(\operatorname {zVec}(\operatorname {liftToExtended}(P))(\operatorname {inr}(e)) = 0\), so the filter over edges with non-trivial support is empty and has cardinality \(0\). Adding zero to the vertex weight, the vertex contribution equals \(\operatorname {weight}(P)\) by unfolding the definitions of weight and support and applying congruence.

By extensionality on each vertex \(v\), both the \(x\)-vector and \(z\)-vector components agree by simplification using the definitions of \(\operatorname {restrictToV}\), \(\operatorname {liftToExtended}\), and \(\operatorname {deformedOpExt}\).

By extensionality on each qubit \(q \in V \oplus E(G)\), case-splitting on whether \(q\) is a vertex or edge qubit, then simplifying using the definitions of \(\operatorname {liftToExtended}\), \(\operatorname {deformedOpExt}\), and the multiplication formulas for \(x\)-vectors and \(z\)-vectors.

By extensionality on each qubit \(q\), case-splitting on vertex or edge, and simplifying using the definitions and the formulas for \(\operatorname {xVec}\) and \(\operatorname {zVec}\) of the identity.

Suppose for contradiction that \(\operatorname {liftToExtended}(P) = \mathbf{1}\). Applying \(\operatorname {restrictToV}\) to both sides and using the fact that \(\operatorname {restrictToV}(\operatorname {liftToExtended}(P)) = P\) and \(\operatorname {restrictToV}(\mathbf{1}) = \mathbf{1}\), we obtain \(P = \mathbf{1}\), contradicting \(P \neq \mathbf{1}\).

We unfold \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\), then decompose the sum over the type \(V \oplus E(G)\) into vertex and edge parts. For the vertex sum: since flux checks are pure \(Z\) on edges and have trivial \(x\)-vector on vertices, each summand \(\operatorname {xVec}(\operatorname {lift}(P))(\operatorname {inl}(v)) \cdot \operatorname {zVec}(\operatorname {flux}(p))(\operatorname {inl}(v)) + \operatorname {zVec}(\operatorname {lift}(P))(\operatorname {inl}(v)) \cdot \operatorname {xVec}(\operatorname {flux}(p))(\operatorname {inl}(v))\) equals \(0\) by simplification. For the edge sum: since the lift has zero support on edges, each summand equals \(0\). Adding the two zero contributions gives \(0\).

We rewrite the commutation condition as \(\operatorname {symplecticInner}(\operatorname {liftToExtended}(P), \operatorname {deformedOriginalChecks}(j)) = 0\). Since the lift has no \(X\)-support on edges, we apply the lemma that symplectic inner products with deformed checks reduce to the restriction on \(V\). Rewriting using \(\operatorname {restrictToV}(\operatorname {liftToExtended}(P)) = P\), the result follows from the hypothesis that \(P\) commutes with \(\operatorname {checks}(j)\).

We unfold \(\operatorname {symplecticInner}\) and decompose the sum over \(V \oplus E(G)\). For the vertex sum: since \(A_v\) has \(\operatorname {zVec} = 0\) on vertices and \(\operatorname {xVec}(\operatorname {inl}(w)) = \delta _{v,w}\), we simplify each term and use single-element summation to extract the \(v\)-th term, obtaining \(P.\operatorname {zVec}(v)\). For the edge sum: since the lift has zero components on edges, each summand is zero. Adding the vertex sum and the zero edge sum gives the result.

Unfolding \(\operatorname {PauliCommute}\), the condition becomes \(\langle \operatorname {liftToExtended}(P), A_v \rangle _{\mathrm{symp}} = 0\). By the previous lemma, this equals \(P.\operatorname {zVec}(v) = 0\).

By the commutation criterion, it suffices to show \(P.\operatorname {zVec}(v) = 0\), which follows from evaluating the hypothesis \(P.\operatorname {zVec} = 0\) at \(v\).

Let \(a\) be an arbitrary check of the deformed code.We simplify using the structure of the deformed stabilizer code and case-split on the type of check \(a\):

• Gauss law check (\(a = \operatorname {gaussLaw}(v)\)): commutation follows from the pure-\(X\) Gauss law commutation lemma.

• Flux check (\(a = \operatorname {flux}(p)\)): commutation follows from the flux commutation lemma.

• Deformed original check (\(a = \operatorname {deformed}(j)\)): commutation follows from the deformed check commutation lemma, using the hypothesis that \(P\) commutes with the original check \(\operatorname {checks}(j)\).

This is a direct application of the theorem \(\texttt{deformed\_ distance\_ ge\_ d\_ sufficient\_ expansion}\).

Unfolding the definition of distance as an infimum, we apply \(\operatorname {Nat.sInf\_ le}\) using the witness \((L', \text{hlog}, \operatorname {rfl})\).

From the hypothesis that \(P\) is a logical operator, we extract that \(P\) is in the centralizer of the original code, \(P\) is not in the stabilizer group, and \(P \neq \mathbf{1}\). We verify the three conditions for \(\operatorname {liftToExtended}(P)\) being a logical of the deformed code:

1. Centralizer membership: Since \(P\) is pure-\(X\) and commutes with all original checks, we apply the centralizer lifting theorem.

2. Not in deformed stabilizer: This is given by hypothesis.

3. Non-identity: Since \(P \neq \mathbf{1}\), the lift is non-identity by injectivity of the lift.

We first establish that \(\operatorname {liftToExtended}(P)\) is a logical of the deformed code. Then:

where the first inequality uses the deformed distance bound, the first equality uses weight preservation of the lift, and the second equality uses the hypothesis \(\operatorname {weight}(P) = d\).

We apply antisymmetry of \(\leq \). The inequality \(d^* \leq d\) follows from Point 2 (deformed distance at most original). The inequality \(d \leq d^*\) follows from Point 1 (sufficient expansion gives \(d^* \geq d\)).

By the general bound from Lemma 3, \(d^* \geq \min (h(G), 1) \cdot d\). Since \(h(G) {\lt} 1\), we have \(\min (h(G), 1) = h(G)\), so rewriting gives \(d^* \geq h(G) \cdot d\). The result follows by casting to the appropriate type.

We compute:

where the strict inequality follows from \(h(G) {\lt} 1\) and \(d {\gt} 0\) (using multiplication by a positive right factor), and the equality is by the identity \(1 \cdot d = d\).

Since \(1 \leq h(G)\), we have \(\min (h(G), 1) = 1\), so the expression simplifies to \(1 \cdot d = d\).

Since \(h(G) {\gt} 1\) implies \(h(G) \geq 1\), this is a direct application of the sufficient expansion theorem.

We prove both conjuncts separately.

1. Assume \(h(G) \geq 1\). Then \(\min (h(G), 1) = 1\), so \(\min (h(G), 1) \cdot d = 1 \cdot d = d\).

2. Assume \(h(G) {\lt} 1\). Then \(\min (h(G), 1) = h(G)\) (since \(h(G) \leq h(G) {\lt} 1\)). We apply the lemma that \(h(G) \cdot d {\lt} d\) when \(d {\gt} 0\), \(h(G) {\gt} 0\), and \(h(G) {\lt} 1\).