MerLean-example

35 Rem 12: Noncommuting Operators Cannot Be Deformed

This chapter formalizes the observation that a Pauli operator \(P\) which does not commute with the logical operator \(L\) cannot have a deformed version. The obstruction is topological: if \(P\) anticommutes with \(L = \prod _v X_v\), then \(|\mathcal{S}_Z \cap V_G|\) is odd, but any path boundary \(\partial \gamma \) always has even cardinality, so no edge-path \(\gamma \) with \(\partial \gamma = \mathcal{S}_Z \cap V_G\) can exist.

Definition 1116 Vector Support
#

The support of a binary vector \(f : V' = V \to \mathbb {Z}_2\) is the set of vertices where \(f\) is nonzero:

\[ \mathrm{vectorSupport}(f) = \{ v \in V \mid f(v) \neq 0 \} . \]
Lemma 1117 ZMod 2 Nonzero Iff One

For any \(x \in \mathbb {Z}_2\), we have \(x \neq 0\) if and only if \(x = 1\).

Proof

We prove both directions. For the forward direction, assume \(x \neq 0\). We case-split on \(x \in \mathbb {Z}_2\): if \(x = 0\) we reach a contradiction with the assumption, so \(x = 1\) and this holds by reflexivity. For the reverse direction, assume \(x = 1\); rewriting, \(1 \neq 0\) holds by computation.

Definition 1118 Boundary Support

The boundary support of an edge-path \(\gamma \) is the set of vertices where the boundary is nonzero:

\[ \mathrm{boundarySupport}(G, \gamma ) = \{ v \in V \mid \partial \gamma (v) \neq 0 \} . \]
Lemma 1119 Boundary Support Equals Filter by One

For any edge-path \(\gamma \), the boundary support equals the set of vertices where the boundary value is \(1\):

\[ \mathrm{boundarySupport}(G, \gamma ) = \{ v \in V \mid \partial \gamma (v) = 1 \} . \]
Proof

By extensionality, it suffices to show membership equivalence for an arbitrary vertex \(v\). Simplifying the definition of boundary support, both directions follow from the equivalence \(x \neq 0 \Leftrightarrow x = 1\) in \(\mathbb {Z}_2\): the forward direction applies this equivalence, and the reverse direction rewrites with \(\partial \gamma (v) = 1\) and verifies \(1 \neq 0\) by computation.

Theorem 1120 Boundary Values Sum to Zero

For any edge-path \(\gamma \), the sum of boundary values over all vertices is zero:

\[ \sum _{v \in V} \partial \gamma (v) = 0. \]
Proof

This follows directly from boundary_sum_zero.

Theorem 1121 Boundary Cardinality is Even

For any edge-path \(\gamma \), the boundary support has even cardinality:

\[ |\mathrm{boundarySupport}(G, \gamma )| \equiv 0 \pmod{2}. \]

This captures the paper’s statement that “a path boundary always has even cardinality.”

Proof

We first establish that the sum of boundary values is zero: \(\sum _{v \in V} \partial \gamma (v) = 0\) (from boundary_values_sum_zero). We then show that this sum equals \(|\mathrm{boundarySupport}(G,\gamma )|\) in \(\mathbb {Z}_2\). To see this, we split the sum over \(V\) into the sum over vertices where \(\partial \gamma (v) \neq 0\) and vertices where \(\partial \gamma (v) = 0\). The latter sum is zero (each summand is zero). The filter for nonzero values is exactly the boundary support. On the boundary support, each value equals \(1\) (by the \(\mathbb {Z}_2\) characterization), so the sum equals \(|\mathrm{boundarySupport}(G,\gamma )| \cdot 1\). Combining, we get \(|\mathrm{boundarySupport}(G,\gamma )| = 0\) in \(\mathbb {Z}_2\). Extracting the \(\mathbb {Z}_2\) value via ZMod.val yields the result \(|\mathrm{boundarySupport}(G,\gamma )| \bmod 2 = 0\).

Theorem 1122 Boundary Support Has Even Cardinality – Alternative

For any edge-path \(\gamma \), \(|\mathrm{boundarySupport}(G, \gamma )|\) is even.

Proof

Rewriting the definition of Even using Nat.even_iff, this reduces to \(|\mathrm{boundarySupport}(G,\gamma )| \bmod 2 = 0\), which is exactly boundary_cardinality_even.

Theorem 1123 Valid Path Boundary Support Equals Target

If \(\gamma \) is a valid deforming path for a \(Z\)-support set \(S \subseteq V\), then

\[ \mathrm{boundarySupport}(G, \gamma ) = S. \]
Proof

By extensionality, it suffices to show membership equivalence for arbitrary \(v\). Simplifying the boundary support definition and using the characterization of valid deforming paths (which gives \(\partial \gamma (v) = \chi _S(v)\) for all \(v\)), we rewrite the boundary value. We then show equivalence with membership in \(S\) using the \(Z\)-support vector: if \(v \notin S\), then \(\chi _S(v) = 0\) and \(0 \neq 0\) is false; if \(v \in S\), then \(\chi _S(v) = 1\) and \(1 \neq 0\) holds by computation.

Theorem 1124 Odd Set Cannot Be a Boundary Support

If \(|S| \bmod 2 = 1\) (i.e., \(S\) has odd cardinality), then \(S\) is not the boundary support of any edge-path:

\[ |S| \bmod 2 = 1 \implies \nexists \gamma ,\; \mathrm{boundarySupport}(G,\gamma ) = S. \]
Proof

Suppose for contradiction there exists \(\gamma \) with \(\mathrm{boundarySupport}(G,\gamma ) = S\). By boundary_cardinality_even, \(|\mathrm{boundarySupport}(G,\gamma )| \bmod 2 = 0\). Rewriting with the equality gives \(|S| \bmod 2 = 0\), contradicting \(|S| \bmod 2 = 1\) by integer arithmetic.

Definition 1125 Anticommutes with \(L\)

A Pauli operator \(P\) (represented by its \(Z\)-support on \(V\)) anticommutes with \(L\) if its \(Z\)-support has odd cardinality:

\[ \mathrm{anticommutesWithL}(\mathcal{S}_Z) \iff |\mathcal{S}_Z| \bmod 2 = 1. \]
Definition 1126 Commutes with \(L\)
#

A Pauli operator \(P\) (represented by its \(Z\)-support on \(V\)) commutes with \(L\) if its \(Z\)-support has even cardinality:

\[ \mathrm{commutesWithL}(\mathcal{S}_Z) \iff |\mathcal{S}_Z| \bmod 2 = 0. \]
Theorem 1127 Commutes or Anticommutes

For any \(Z\)-support set, either \(P\) commutes with \(L\) or \(P\) anticommutes with \(L\):

\[ \mathrm{commutesWithL}(\mathcal{S}_Z) \lor \mathrm{anticommutesWithL}(\mathcal{S}_Z). \]
Proof

Unfolding the definitions, both conditions concern \(|\mathcal{S}_Z| \bmod 2\) being \(0\) or \(1\). The result follows by integer arithmetic (a natural number modulo \(2\) is either \(0\) or \(1\)).

Theorem 1128 Not Commuting Iff Anticommuting

A Pauli operator does not commute with \(L\) if and only if it anticommutes with \(L\):

\[ \neg \mathrm{commutesWithL}(\mathcal{S}_Z) \iff \mathrm{anticommutesWithL}(\mathcal{S}_Z). \]
Proof

Unfolding the definitions, this reduces to \(|\mathcal{S}_Z| \bmod 2 \neq 0 \Leftrightarrow |\mathcal{S}_Z| \bmod 2 = 1\), which holds by integer arithmetic.

Theorem 1129 Not Anticommuting Iff Commuting

A Pauli operator does not anticommute with \(L\) if and only if it commutes with \(L\):

\[ \neg \mathrm{anticommutesWithL}(\mathcal{S}_Z) \iff \mathrm{commutesWithL}(\mathcal{S}_Z). \]
Proof

Unfolding the definitions, this reduces to \(|\mathcal{S}_Z| \bmod 2 \neq 1 \Leftrightarrow |\mathcal{S}_Z| \bmod 2 = 0\), which holds by integer arithmetic.

Theorem 1130 No Deforming Path for Anticommuting Operator

If a Pauli operator \(P\) anticommutes with \(L\) (i.e., \(|\mathcal{S}_Z \cap V_G|\) is odd), then no valid deforming path exists:

\[ \mathrm{anticommutesWithL}(\mathcal{S}_Z) \implies \nexists \gamma ,\; \mathrm{IsValidDeformingPath}(G, \mathcal{S}_Z, \gamma ). \]

This formalizes the remark’s central claim: there is no deformed version of a Pauli operator that does not commute with the logical \(L\).

Proof

Suppose for contradiction there exists \(\gamma \) with \(\mathrm{IsValidDeformingPath}(G, \mathcal{S}_Z, \gamma )\). By valid_path_boundary_support_eq, we have \(\mathrm{boundarySupport}(G,\gamma ) = \mathcal{S}_Z\). By boundary_cardinality_even, \(|\mathrm{boundarySupport}(G,\gamma )| \bmod 2 = 0\). Rewriting, \(|\mathcal{S}_Z| \bmod 2 = 0\). But anticommutation gives \(|\mathcal{S}_Z| \bmod 2 = 1\), a contradiction by integer arithmetic.

Theorem 1131 No Deforming Path – Alternative via Def 4

Restatement of the above using the existing theorem no_valid_path_if_odd from Def 4:

\[ \mathrm{anticommutesWithL}(\mathcal{S}_Z) \implies \nexists \gamma ,\; \mathrm{IsValidDeformingPath}(G, \mathcal{S}_Z, \gamma ). \]
Proof

This follows directly from no_valid_path_if_odd.

Theorem 1132 Deformation Requires Commutation

The contrapositive: existence of a valid deforming path implies \(P\) commutes with \(L\):

\[ \mathrm{IsValidDeformingPath}(G, \mathcal{S}_Z, \gamma ) \implies \mathrm{commutesWithL}(\mathcal{S}_Z). \]
Proof

Unfolding the definition of commutesWithL, we need \(|\mathcal{S}_Z| \bmod 2 = 0\). This follows directly from zSupport_even_of_valid_path_exists applied to \(G\), \(\mathcal{S}_Z\), and \(\gamma \).

Theorem 1133 Stabilizer Product Cannot Fix Anticommutation

If \(P\) anticommutes with \(L\), then for every edge-path \(\gamma \), \(\gamma \) is not a valid deforming path for \(\mathcal{S}_Z\). This captures the paper’s claim: “there is no way to multiply such a \(P\) with stabilizers \(Z_e\) and \(s_j\) to make it commute with all the Gauss’s law operators \(A_v\).”

\[ \mathrm{anticommutesWithL}(\mathcal{S}_Z) \implies \forall \gamma ,\; \neg \mathrm{IsValidDeformingPath}(G, \mathcal{S}_Z, \gamma ). \]
Proof

Let \(\gamma \) be an arbitrary edge-path. From no_deforming_path_for_anticommuting_operator, we know there is no valid deforming path at all. If \(\gamma \) were valid, it would witness the existence of such a path, yielding a contradiction.

Theorem 1134 Gauss Law Obstruction

The Gauss law operators \(A_v\) form an obstruction: if \(P\) anticommutes with \(L\), then for any edge-path \(\gamma \), either there exists a vertex \(v\) at which the deformed Gauss law symplectic condition fails (i.e., the symplectic inner product is not even), or \(\gamma \) is not a valid deforming path:

\[ \mathrm{anticommutesWithL}(\mathcal{S}_Z) \implies \bigl(\exists v,\; \omega (A_v, \tilde{P})_v \not\equiv 0 \pmod{2}\bigr) \lor \neg \mathrm{IsValidDeformingPath}(G, \mathcal{S}_Z, \gamma ). \]
Proof

We take the right disjunct. By stabilizer_product_cannot_fix_anticommutation, \(\gamma \) is not a valid deforming path for \(\mathcal{S}_Z\).

Theorem 1135 No Deformed Version for Noncommuting Operators

Complete formalization of Remark 12: There is no deformed version of a Pauli operator \(P\) that does not commute with the logical \(L\). Specifically:

  1. If \(P\) anticommutes with \(L\), then \(|\mathcal{S}_Z \cap V_G|\) is odd.

  2. A path boundary \(\partial \gamma \) always has even cardinality.

  3. Therefore no edge-path \(\gamma \) with \(\partial \gamma = \mathcal{S}_Z \cap V_G\) exists.

  4. Hence \(P\) has no well-defined deformed version.

\[ \mathrm{anticommutesWithL}(\mathcal{S}_Z) \implies \nexists \gamma ,\; \mathrm{IsValidDeformingPath}(G, \mathcal{S}_Z, \gamma ). \]
Proof

This follows directly from no_deforming_path_for_anticommuting_operator.

The logical structure of the argument consists of four parts, all holding simultaneously:

  1. \(\mathrm{anticommutesWithL}(\mathcal{S}_Z) \implies |\mathcal{S}_Z| \bmod 2 = 1\).

  2. \(\forall \gamma ,\; |\mathrm{boundarySupport}(G,\gamma )| \bmod 2 = 0\).

  3. \(\forall \gamma ,\; \mathrm{IsValidDeformingPath}(G,\mathcal{S}_Z,\gamma ) \implies \mathrm{boundarySupport}(G,\gamma ) = \mathcal{S}_Z\).

  4. \(\mathrm{anticommutesWithL}(\mathcal{S}_Z) \implies \nexists \gamma ,\; \mathrm{IsValidDeformingPath}(G,\mathcal{S}_Z,\gamma )\).

Proof

We verify each part. Part 1: the anticommutation hypothesis is exactly the statement that \(|\mathcal{S}_Z| \bmod 2 = 1\), so this holds by the identity function. Part 2: this is exactly boundary_cardinality_even. Part 3: this is exactly valid_path_boundary_support_eq. Part 4: this is exactly no_deforming_path_for_anticommuting_operator.

Theorem 1137 Valid Path Implies Commutes with \(L\)

If there exists a valid deforming path for \(\mathcal{S}_Z\), then \(P\) must commute with \(L\):

\[ (\exists \gamma ,\; \mathrm{IsValidDeformingPath}(G,\mathcal{S}_Z,\gamma )) \implies \mathrm{commutesWithL}(\mathcal{S}_Z). \]
Proof

From the hypothesis, we obtain \(\gamma \) and \(h_\gamma \) witnessing the valid deforming path. We then apply deformation_requires_commutation to \(G\), \(\mathcal{S}_Z\), \(\gamma \), and \(h_\gamma \).

Theorem 1138 Valid Path Exists Implies Commutation

The existence of a valid deforming path implies commutation:

\[ (\exists \gamma ,\; \mathrm{IsValidDeformingPath}(G,\mathcal{S}_Z,\gamma )) \implies \mathrm{commutesWithL}(\mathcal{S}_Z). \]
Proof

Assume the hypothesis. This follows directly from valid_path_implies_commutes_with_L.

Theorem 1139 Noncommuting Implies No Deformation

The forward direction, which is the key result of the remark: if \(P\) anticommutes with \(L\), then no valid deforming path exists.

Proof

This follows directly from no_deforming_path_for_anticommuting_operator.