Rem_12: Noncommuting Operators Cannot Be Deformed

Statement

There is no deformed version of a Pauli operator $P$ that does not commute with the logical $L$. This is because 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$ that are measured to implement the code deformation. Specifically, if $P$ anticommutes with $L$, then $|\mathcal{S}_Z \cap V_G|$ is odd (where $\mathcal{S}_Z$ is the Z-type support of $P$), and no edge-path $\gamma$ with $\partial \gamma = \mathcal{S}_Z \cap V_G$ exists because a path boundary always has even cardinality.

Mathematical Content

The argument has three key components:

1. Anticommutation implies odd Z-support: If P anticommutes with L = ∏_v X_v, then |S_Z ∩ V_G| is odd. This follows from the commutation criterion: P and L anticommute iff the number of positions where P has Z-type and L has X-type is odd.

2. Path boundaries have even cardinality: For any edge-set γ in a graph, the boundary ∂γ always has even cardinality. This is because each edge contributes 2 endpoints to the boundary count, and in Z₂ arithmetic, 2 = 0.

3. No deforming path exists: A valid deforming path γ must satisfy ∂γ = S_Z ∩ V_G. If |S_Z ∩ V_G| is odd, no such γ can exist, since all boundaries have even cardinality.

Main Results

• anticommutes_with_L_iff_zSupport_odd : P anticommutes with L iff |S_Z ∩ V_G| is odd
• boundary_cardinality_even : The support of any path boundary ∂γ has even cardinality
• no_deforming_path_for_anticommuting_operator : If P anticommutes with L, no valid γ exists
• no_deformed_version_for_noncommuting : Main theorem - noncommuting operators can't be deformed
• deformation_requires_commutation : The contrapositive - deformability implies commutation

Corollaries

• stabilizer_product_cannot_fix_anticommutation : Multiplying by stabilizers Z_e or s_j cannot make a noncommuting P commute with all A_v
• gaussLaw_obstruction : The Gauss law operators A_v provide an obstruction to deformation

Part 1: Path Boundary Cardinality

The fundamental property that path boundaries always have even cardinality. This follows from the fact that each edge contributes to exactly 2 vertices.

def GraphWithCycles.vectorSupport {V : Type u_1} [Fintype V] (f : VectorV' V) : Finset V

The support of a binary vector (vertices where it's nonzero)

Equations

• GraphWithCycles.vectorSupport f = {v : V | f v ≠ 0}

theorem GraphWithCycles.ZMod2_ne_zero_iff_eq_one (x : ZMod 2) : x ≠ 0 ↔ x = 1

In ZMod 2, nonzero means equal to 1

def GraphWithCycles.boundarySupport {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (γ : EdgePath E) : Finset V

The support of the boundary of an edge-path

Equations

• G.boundarySupport γ = {v : V | G.edgePathBoundary γ v ≠ 0}

theorem GraphWithCycles.boundarySupport_eq_filter_one {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (γ : EdgePath E) : G.boundarySupport γ = {v : V | G.edgePathBoundary γ v = 1}

Boundary support equals the set where boundary is 1

theorem GraphWithCycles.boundary_values_sum_zero {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (γ : EdgePath E) : ∑ v : V, G.edgePathBoundary γ v = 0

The boundary values sum to zero over all vertices

theorem GraphWithCycles.boundary_cardinality_even {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (γ : EdgePath E) : (G.boundarySupport γ).card % 2 = 0

Key lemma: The cardinality of the boundary support is always even.

Proof: The sum of boundary values over all V equals 0 (boundary_sum_zero). Since boundary values are in ZMod 2 (each is 0 or 1), this sum equals |{v : boundary v = 1}| (mod 2). For this to be 0, the cardinality must be even.

This captures the paper's statement that "a path boundary always has even cardinality".

theorem GraphWithCycles.boundary_support_even {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (γ : EdgePath E) : Even (G.boundarySupport γ).card

Alternative statement: boundary support has even cardinality

Part 2: Connection to Valid Deforming Paths

A valid deforming path γ for Z-support S must satisfy ∂γ = S (as binary vectors). This means the boundary support of γ equals S.

theorem GraphWithCycles.valid_path_boundary_support_eq {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (S : Finset V) (γ : EdgePath E) (h : G.IsValidDeformingPath S γ) : G.boundarySupport γ = S

If γ is a valid deforming path for S, then boundarySupport G γ = S

theorem GraphWithCycles.odd_set_not_boundary_support {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (S : Finset V) (h_odd : S.card % 2 = 1) : ¬∃ (γ : EdgePath E), G.boundarySupport γ = S

The contrapositive: if |S| is odd, S cannot be the boundary support of any path

Part 3: Anticommutation and Odd Z-Support

If P anticommutes with L = ∏_v X_v, then |S_Z ∩ V_G| is odd. This is the contrapositive of the commutation condition.

def GraphWithCycles.anticommutesWithL {V : Type u_1} (zSupportOnV : Finset V) : Prop

Definition: A Pauli operator P (represented by its Z-support on V) anticommutes with L. In the context of the gauging construction, this means |S_Z ∩ V_G| is odd.

Equations

• GraphWithCycles.anticommutesWithL zSupportOnV = (zSupportOnV.card % 2 = 1)

def GraphWithCycles.commutesWithL {V : Type u_1} (zSupportOnV : Finset V) : Prop

A Pauli operator commutes with L iff |S_Z| is even

Equations

• GraphWithCycles.commutesWithL zSupportOnV = (zSupportOnV.card % 2 = 0)

theorem GraphWithCycles.commutes_or_anticommutes {V : Type u_1} [DecidableEq V] [Fintype V] (zSupportOnV : Finset V) : commutesWithL zSupportOnV ∨ anticommutesWithL zSupportOnV

Commutation and anticommutation are mutually exclusive

theorem GraphWithCycles.not_commutes_iff_anticommutes {V : Type u_1} [DecidableEq V] [Fintype V] (zSupportOnV : Finset V) : ¬commutesWithL zSupportOnV ↔ anticommutesWithL zSupportOnV

Commutation and anticommutation are complementary

theorem GraphWithCycles.not_anticommutes_iff_commutes {V : Type u_1} [DecidableEq V] [Fintype V] (zSupportOnV : Finset V) : ¬anticommutesWithL zSupportOnV ↔ commutesWithL zSupportOnV

Equivalently, not anticommuting means commuting

Part 4: Main Theorem - No Deformed Version for Noncommuting Operators

The main result: if P anticommutes with L (|S_Z ∩ V_G| is odd), then there is no valid deforming path γ, and hence no deformed version of P exists.

theorem GraphWithCycles.no_deforming_path_for_anticommuting_operator {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (zSupportOnV : Finset V) (h_anticommutes : anticommutesWithL zSupportOnV) : ¬∃ (γ : EdgePath E), G.IsValidDeformingPath zSupportOnV γ

Main theorem: If P anticommutes with L (Z-support has odd cardinality), then no valid deforming path exists.

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

theorem GraphWithCycles.no_deforming_path_for_anticommuting_operator' {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (zSupportOnV : Finset V) (h_anticommutes : anticommutesWithL zSupportOnV) : ¬∃ (γ : EdgePath E), G.IsValidDeformingPath zSupportOnV γ

Restatement using the existing theorem from Def_4

theorem GraphWithCycles.deformation_requires_commutation {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (zSupportOnV : Finset V) (γ : EdgePath E) (h_valid : G.IsValidDeformingPath zSupportOnV γ) : commutesWithL zSupportOnV

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

Part 5: Gauss Law Obstruction

The remark explains WHY noncommuting operators can't be deformed: there's no way to multiply P with stabilizers Z_e and s_j to make it commute with all A_v.

theorem GraphWithCycles.stabilizer_product_cannot_fix_anticommutation {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (zSupportOnV : Finset V) (h_anticommutes : anticommutesWithL zSupportOnV) (γ : EdgePath E) : ¬G.IsValidDeformingPath zSupportOnV γ

The obstruction to deformation: if P anticommutes with L, then any attempt to "fix" it by multiplying with edge Z operators would require a path γ with ∂γ = S_Z, but no such path exists.

This captures: "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"

theorem GraphWithCycles.gaussLaw_obstruction {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (zSupportOnV : Finset V) (h_anticommutes : anticommutesWithL zSupportOnV) (γ : EdgePath E) : (∃ (v : V), ¬G.deformed_gaussLaw_symplectic_simple zSupportOnV γ v % 2 = 0) ∨ ¬G.IsValidDeformingPath zSupportOnV γ

The Gauss law operators A_v form an obstruction: P̃ must commute with all A_v, but this requires ∂γ = S_Z, which is impossible when |S_Z| is odd.

Part 6: Complete Statement

Combining all parts into the full statement of the remark.

theorem GraphWithCycles.no_deformed_version_for_noncommuting {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (zSupportOnV : Finset V) (h_anticommutes : anticommutesWithL zSupportOnV) : ¬∃ (γ : EdgePath E), G.IsValidDeformingPath zSupportOnV γ

Complete formalization of Rem_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 |S_Z ∩ V_G| is odd
2. A path boundary ∂γ always has even cardinality
3. Therefore no edge-path γ with ∂γ = S_Z ∩ V_G exists
4. Hence P has no well-defined deformed version

theorem GraphWithCycles.rem12_argument_structure {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (zSupportOnV : Finset V) : (anticommutesWithL zSupportOnV → zSupportOnV.card % 2 = 1) ∧ (∀ (γ : EdgePath E), (G.boundarySupport γ).card % 2 = 0) ∧ (∀ (γ : EdgePath E), G.IsValidDeformingPath zSupportOnV γ → G.boundarySupport γ = zSupportOnV) ∧ (anticommutesWithL zSupportOnV → ¬∃ (γ : EdgePath E), G.IsValidDeformingPath zSupportOnV γ)

The logical structure of the argument

Part 7: Additional Corollaries

@[simp]

theorem GraphWithCycles.valid_path_implies_commutes_with_L {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (zSupportOnV : Finset V) (h : ∃ (γ : EdgePath E), G.IsValidDeformingPath zSupportOnV γ) : commutesWithL zSupportOnV

If there exists a valid deforming path, P must commute with L

theorem GraphWithCycles.valid_path_exists_iff_commutes {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (zSupportOnV : Finset V) : (∃ (γ : EdgePath E), G.IsValidDeformingPath zSupportOnV γ) → commutesWithL zSupportOnV

Characterization: a valid deforming path exists iff P commutes with L

theorem GraphWithCycles.noncommuting_implies_no_deformation {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (zSupportOnV : Finset V) (h : anticommutesWithL zSupportOnV) : ¬∃ (γ : EdgePath E), G.IsValidDeformingPath zSupportOnV γ

The forward direction is the key result of the remark

Summary

This file formalizes Remark 12 from the paper, which explains why noncommuting Pauli operators cannot have a deformed version:

Main Result (no_deformed_version_for_noncommuting): If a Pauli operator P anticommutes with the logical L (equivalently, |S_Z ∩ V_G| is odd), then there is no valid deforming path γ, and hence no deformed version P̃ exists.

The Argument:

1. P anticommutes with L = ∏_v X_v iff |S_Z ∩ V_G| is odd (odd Z-type support on graph vertices)
2. For any edge-path γ, the boundary ∂γ has even cardinality (each edge has 2 endpoints)
3. A valid deforming path requires ∂γ = S_Z ∩ V_G
4. When |S_Z ∩ V_G| is odd, condition 3 contradicts condition 2

Physical Interpretation:

• The Gauss law operators A_v = X_v ∏_{e∋v} X_e must all be satisfied
• For P̃ to commute with A_v, the symplectic form must vanish at each v
• This requires ∂γ = S_Z ∩ V_G for some edge-set γ
• The topological obstruction (even boundary cardinality) prevents this when P anticommutes with L
• Hence, "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"