Remark 6: Noncommuting Operators Cannot Be Deformed

Statement

A Pauli operator P that does not commute with L cannot be deformed to commute with all Gauss's law operators A_v. The boundary condition ∂γ = S_Z(P)|_V has no solution when CommutesWithLogical(P) fails, and multiplying P by Z_e operators or commuting stabilizers cannot change this.

Main Results

• noncommuting_cannot_be_deformed : ¬CommutesWithLogical(P) → ¬∃ γ, BoundaryCondition(G, P, γ)
• zSupportOnVertices_sum_mul : Z-support sum is additive under multiplication
• mul_commuting_preserves_commutesWithLogical : CommutesWithLogical is closed under mul
• commutesWithLogical_mul_iff : CommutesWithLogical(P*Q) ↔ CommutesWithLogical(P) when Q commutes
• no_modification_helps : ¬CommutesWithLogical(P) ∧ CommutesWithLogical(Q) → ¬CommutesWithLogical(P*Q)
• no_modified_deformation_exists : no boundary condition for P*Q either
• zSupport_not_in_boundary_range : zSupportOnVertices(P) ∉ range(∂)
• boundaryCondition_exists_iff_in_image : boundary condition ↔ membership in range(∂)

Corollaries

• singleZ (pauliZ) flips CommutesWithLogical
• Stabilizers preserve non-commuting status

Main Theorem: Noncommuting Operators Cannot Be Deformed

theorem NoncommutingOperatorsCannotBeDeformed.noncommuting_cannot_be_deformed {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (hP : ¬DeformedOperator.CommutesWithLogical P) : ¬∃ (γ : ↑G.edgeSet → ZMod 2), DeformedOperator.BoundaryCondition G P γ

If ¬CommutesWithLogical(P), then no edge-path γ satisfies the boundary condition. This is the contrapositive of boundaryCondition_implies_commutes.

Z-Support Sum Additivity

theorem NoncommutingOperatorsCannotBeDeformed.zSupportOnVertices_sum_mul {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) : ∑ v : V, DeformedOperator.zSupportOnVertices (P * Q) v = ∑ v : V, DeformedOperator.zSupportOnVertices P v + ∑ v : V, DeformedOperator.zSupportOnVertices Q v

The sum of zSupportOnVertices is additive under Pauli multiplication.

CommutesWithLogical Preserved Under Multiplication

theorem NoncommutingOperatorsCannotBeDeformed.mul_commuting_preserves_commutesWithLogical {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) (hP : DeformedOperator.CommutesWithLogical P) (hQ : DeformedOperator.CommutesWithLogical Q) : DeformedOperator.CommutesWithLogical (P * Q)

If CommutesWithLogical(P) and CommutesWithLogical(Q), then CommutesWithLogical(P * Q).

theorem NoncommutingOperatorsCannotBeDeformed.mul_commuting_contrapositive {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) (hPQ : ¬DeformedOperator.CommutesWithLogical (P * Q)) (hQ : DeformedOperator.CommutesWithLogical Q) : ¬DeformedOperator.CommutesWithLogical P

Contrapositive: if ¬CommutesWithLogical(P * Q) and CommutesWithLogical(Q), then ¬CommutesWithLogical(P).

singleZ (pauliZ) and CommutesWithLogical

theorem NoncommutingOperatorsCannotBeDeformed.zSupportOnVertices_singleZ_sum {V : Type u_1} [Fintype V] [DecidableEq V] (v : V) : ∑ w : V, DeformedOperator.zSupportOnVertices (PauliOp.pauliZ v) w = 1

The sum of zSupportOnVertices of pauliZ(v) is 1.

theorem NoncommutingOperatorsCannotBeDeformed.singleZ_not_commutesWithLogical {V : Type u_1} [Fintype V] [DecidableEq V] (v : V) : ¬DeformedOperator.CommutesWithLogical (PauliOp.pauliZ v)

pauliZ(v) does not commute with L.

theorem NoncommutingOperatorsCannotBeDeformed.singleZ_flips_commutesWithLogical {V : Type u_1} [Fintype V] [DecidableEq V] (P : PauliOp V) (v : V) : DeformedOperator.CommutesWithLogical (P * PauliOp.pauliZ v) ↔ ¬DeformedOperator.CommutesWithLogical P

Multiplying by pauliZ(v) flips CommutesWithLogical.

Z-Support Restricted to Vertices on the Extended System

def NoncommutingOperatorsCannotBeDeformed.zSupportRestricted {V : Type u_1} [Fintype V] (G : SimpleGraph V) (P : PauliOp (GaussFlux.ExtQubit G)) : ZMod 2

The Z-support sum restricted to vertex qubits of a Pauli operator on the extended system V ⊕ G.edgeSet. This captures CommutesWithLogical for the extended system.

Equations

• NoncommutingOperatorsCannotBeDeformed.zSupportRestricted G P = ∑ v : V, if P.zVec (Sum.inl v) ≠ 0 then 1 else 0

def NoncommutingOperatorsCannotBeDeformed.CommutesWithLogical' {V : Type u_1} [Fintype V] (G : SimpleGraph V) (P : PauliOp (GaussFlux.ExtQubit G)) : Prop

CommutesWithLogical on the extended system, restricted to vertex qubits.

Equations

• NoncommutingOperatorsCannotBeDeformed.CommutesWithLogical' G P = (NoncommutingOperatorsCannotBeDeformed.zSupportRestricted G P = 0)

theorem NoncommutingOperatorsCannotBeDeformed.singleZ_edge_preserves_commutesWithLogical' {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp (GaussFlux.ExtQubit G)) (e : ↑G.edgeSet) : CommutesWithLogical' G (P * PauliOp.pauliZ (Sum.inr e)) ↔ CommutesWithLogical' G P

Multiplying a Pauli operator on the extended system V ⊕ E by Z on an edge qubit does not change the CommutesWithLogical' condition. This is because pauliZ on an edge qubit (Sum.inr e) has zero Z-support on vertex qubits (Sum.inl v).

Stabilizer Preserves Non-Commuting Status

theorem NoncommutingOperatorsCannotBeDeformed.stabilizer_preserves_noncommuting {V : Type u_1} [Fintype V] [DecidableEq V] (P s : PauliOp V) (hP : ¬DeformedOperator.CommutesWithLogical P) (hs : DeformedOperator.CommutesWithLogical s) : ¬DeformedOperator.CommutesWithLogical (P * s)

If ¬CommutesWithLogical(P) and CommutesWithLogical(s), then ¬CommutesWithLogical(P * s).

No Deformation Exists

theorem NoncommutingOperatorsCannotBeDeformed.no_deformation_exists {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (hP : ¬DeformedOperator.CommutesWithLogical P) (γ : ↑G.edgeSet → ZMod 2) : ¬DeformedOperator.BoundaryCondition G P γ

For every edge-path γ, the boundary condition fails when ¬CommutesWithLogical(P).

CommutesWithLogical Invariant Under Commuting Multiplication

theorem NoncommutingOperatorsCannotBeDeformed.commutesWithLogical_mul_iff {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) (hQ : DeformedOperator.CommutesWithLogical Q) : DeformedOperator.CommutesWithLogical (P * Q) ↔ DeformedOperator.CommutesWithLogical P

CommutesWithLogical(P * Q) ↔ CommutesWithLogical(P) when CommutesWithLogical(Q).

No Modification Helps

theorem NoncommutingOperatorsCannotBeDeformed.no_modification_helps {V : Type u_1} [Fintype V] [DecidableEq V] (P Q : PauliOp V) (hP : ¬DeformedOperator.CommutesWithLogical P) (hQ : DeformedOperator.CommutesWithLogical Q) : ¬DeformedOperator.CommutesWithLogical (P * Q)

If ¬CommutesWithLogical(P) and CommutesWithLogical(Q), then ¬CommutesWithLogical(P * Q). No product of Z_e operators and commuting stabilizers can help.

No Modified Deformation Exists

theorem NoncommutingOperatorsCannotBeDeformed.no_modified_deformation_exists {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P Q : PauliOp V) (hP : ¬DeformedOperator.CommutesWithLogical P) (hQ : DeformedOperator.CommutesWithLogical Q) (γ : ↑G.edgeSet → ZMod 2) : ¬DeformedOperator.BoundaryCondition G (P * Q) γ

If ¬CommutesWithLogical(P) and CommutesWithLogical(Q), then no boundary condition holds for P * Q either.

Z-Support Not in Range of Boundary Map

theorem NoncommutingOperatorsCannotBeDeformed.boundaryCondition_exists_iff_in_image {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) : (∃ (γ : ↑G.edgeSet → ZMod 2), DeformedOperator.BoundaryCondition G P γ) ↔ DeformedOperator.zSupportOnVertices P ∈ (GraphMaps.boundaryMap G).range

The boundary condition for P and γ is equivalent to zSupportOnVertices(P) being in the image of the boundary map applied to γ.

theorem NoncommutingOperatorsCannotBeDeformed.zSupport_not_in_boundary_range {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (hP : ¬DeformedOperator.CommutesWithLogical P) : DeformedOperator.zSupportOnVertices P ∉ (GraphMaps.boundaryMap G).range

If ¬CommutesWithLogical(P), then zSupportOnVertices(P) ∉ range(∂).