Definition 3: Deformed Operator

Statement

A Pauli operator P that commutes with the logical operator L = ∏{v ∈ V} X_v can be written as P̃ = P · ∏{e ∈ γ} Z_e on the extended qubit system V ⊕ E, where γ is an edge-path satisfying the boundary condition ∂γ = S_Z(P)|_V.

Main Results

• zSupportOnVertices : Z-support of P restricted to graph vertices
• CommutesWithLogical : sum of Z-support on V is 0 in ZMod 2
• BoundaryCondition : ∂γ = zSupportOnVertices(P)
• deformedOpExt : the deformed operator on V ⊕ E
• deformedOpExt_comm_gaussLaw : P̃ commutes with A_v when boundary condition holds
• deformedOpExt_mul_self : P̃ is self-inverse
• boundaryCondition_implies_commutes : boundary condition ⟹ commutes with logical
• deformedOperator : anchor definition bundling P, γ, and boundary condition proof

Corollaries

• Vertex/edge evaluation @[simp] lemmas
• X/Z-support characterizations
• Compatibility with multiplication

Z-Support on Vertices

def DeformedOperator.zSupportOnVertices {V : Type u_1} (P : PauliOp V) : V → ZMod 2

The Z-support of a Pauli operator P restricted to the graph vertices V, expressed as a binary vector in ZMod 2^V. This is the characteristic function of S_Z(P) ∩ V: zSupportOnVertices(P)(v) = 1 if P has Z-action at v (i.e., P.zVec v ≠ 0), and 0 otherwise.

Equations

• DeformedOperator.zSupportOnVertices P v = if P.zVec v ≠ 0 then 1 else 0

Commutes With Logical

def DeformedOperator.CommutesWithLogical {V : Type u_1} [Fintype V] (P : PauliOp V) : Prop

A Pauli operator P commutes with the logical L = ∏_{v ∈ V} X_v if the sum of its Z-support on vertices is 0 in ZMod 2 (i.e., even number of vertices with Z-action).

Equations

• DeformedOperator.CommutesWithLogical P = (∑ v : V, DeformedOperator.zSupportOnVertices P v = 0)

Boundary Condition

def DeformedOperator.BoundaryCondition {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) : Prop

The boundary condition: ∂γ = zSupportOnVertices(P), i.e., the boundary of the edge-path γ equals the Z-support of P restricted to V. This is a condition on the choice of edge-path γ given P.

Equations

• DeformedOperator.BoundaryCondition G P γ = ((GraphMaps.boundaryMap G) γ = DeformedOperator.zSupportOnVertices P)

Deformed Operator on Extended Qubits

def DeformedOperator.deformedOpExt {V : Type u_1} (G : SimpleGraph V) (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) : PauliOp (GaussFlux.ExtQubit G)

The deformed operator P̃ on the extended qubit system V ⊕ G.edgeSet. Given a Pauli operator P on V and an edge-path γ (binary vector on edges):

• On vertex qubits: acts as P (preserves both xVec and zVec)
• On edge qubits: acts as Z_e if γ(e) = 1, identity if γ(e) = 0 (i.e., xVec = 0 on edges, zVec = γ(e) on edges)

Equations

• One or more equations did not get rendered due to their size.

Vertex and Edge Evaluation @[simp] Lemmas

@[simp]

theorem DeformedOperator.deformedOpExt_xVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) (v : V) : (deformedOpExt G P γ).xVec (Sum.inl v) = P.xVec v

The deformed operator's X-vector on vertex qubit v equals P's X-vector.

@[simp]

theorem DeformedOperator.deformedOpExt_zVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) (v : V) : (deformedOpExt G P γ).zVec (Sum.inl v) = P.zVec v

The deformed operator's Z-vector on vertex qubit v equals P's Z-vector.

@[simp]

theorem DeformedOperator.deformedOpExt_xVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) (e : ↑G.edgeSet) : (deformedOpExt G P γ).xVec (Sum.inr e) = 0

The deformed operator has no X-action on edge qubits: xVec is 0 on edges.

@[simp]

theorem DeformedOperator.deformedOpExt_zVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) (e : ↑G.edgeSet) : (deformedOpExt G P γ).zVec (Sum.inr e) = γ e

The deformed operator's Z-vector on edge qubit e equals γ(e).

Deforming with Special Inputs

theorem DeformedOperator.deformedOpExt_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (γ : ↑G.edgeSet → ZMod 2) : deformedOpExt G 1 γ = { xVec := fun (q : GaussFlux.ExtQubit G) => match q with | Sum.inl val => 0 | Sum.inr val => 0, zVec := fun (q : GaussFlux.ExtQubit G) => match q with | Sum.inl val => 0 | Sum.inr e => γ e }

Deforming the identity operator with edge-path γ gives a pure-Z edge operator.

theorem DeformedOperator.deformedOpExt_zero_path {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) : deformedOpExt G P 0 = { xVec := fun (q : GaussFlux.ExtQubit G) => match q with | Sum.inl v => P.xVec v | Sum.inr val => 0, zVec := fun (q : GaussFlux.ExtQubit G) => match q with | Sum.inl v => P.zVec v | Sum.inr val => 0 }

Deforming with the zero edge-path extends P trivially to edge qubits.

X-Support and Z-Support Characterization

theorem DeformedOperator.deformedOpExt_xSupport_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) (v : V) : (deformedOpExt G P γ).xVec (Sum.inl v) ≠ 0 ↔ P.xVec v ≠ 0

The deformed operator preserves X-support on vertex qubits.

theorem DeformedOperator.deformedOpExt_zSupport_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) (v : V) : (deformedOpExt G P γ).zVec (Sum.inl v) ≠ 0 ↔ P.zVec v ≠ 0

The Z-support of the deformed operator on vertex qubits matches P.

theorem DeformedOperator.deformedOpExt_zSupport_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) (e : ↑G.edgeSet) : (deformedOpExt G P γ).zVec (Sum.inr e) ≠ 0 ↔ γ e ≠ 0

The Z-support of the deformed operator on edge qubits matches γ.

theorem DeformedOperator.deformedOpExt_hasZAction_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) (e : ↑G.edgeSet) : (deformedOpExt G P γ).zVec (Sum.inr e) ≠ 0 ↔ γ e = 1

The Z-action on edges is exactly γ(e) = 1.

Self-Inverse Property

theorem DeformedOperator.deformedOpExt_mul_self {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) : deformedOpExt G P γ * deformedOpExt G P γ = 1

The deformed operator is self-inverse: P̃ · P̃ = 1.

Sum of Z-Support Equals Cardinality

theorem DeformedOperator.sum_zSupportOnVertices_eq_card {V : Type u_1} [Fintype V] [DecidableEq V] (P : PauliOp V) : ∑ v : V, zSupportOnVertices P v = ↑{v : V | P.zVec v ≠ 0}.card

The sum of the Z-support indicator equals the cardinality of the Z-support finset cast to ZMod 2.

Commutativity Iff Even Z-Support

theorem DeformedOperator.commutesWithLogical_iff_even_zSupport {V : Type u_1} [Fintype V] [DecidableEq V] (P : PauliOp V) : CommutesWithLogical P ↔ Even {v : V | P.zVec v ≠ 0}.card

The commutativity condition holds iff the Z-support on V has even cardinality.

Boundary Condition Implies Commutativity

theorem DeformedOperator.boundary_sum_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (γ : ↑G.edgeSet → ZMod 2) : ∑ v : V, (GraphMaps.boundaryMap G) γ v = 0

The sum of the boundary map over all vertices is 0, since each edge contributes to exactly two vertices.

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

If the boundary condition ∂γ = S_Z(P)|_V holds, then the commutativity condition holds. This is because Σ_v (∂γ)_v = 0 in ZMod 2, since each edge contributes to exactly two vertices.

Commutation with Gauss's Law

theorem DeformedOperator.deformedOpExt_comm_gaussLaw {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) (hbc : BoundaryCondition G P γ) (v : V) : (deformedOpExt G P γ).PauliCommute (GaussFlux.gaussLawOp G v)

The deformed operator P̃ commutes with the Gauss's law operator A_v when the boundary condition ∂γ = S_Z(P)|_V holds.

Compatibility with Multiplication

theorem DeformedOperator.deformedOpExt_mul {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P Q : PauliOp V) (γ₁ γ₂ : ↑G.edgeSet → ZMod 2) : deformedOpExt G P γ₁ * deformedOpExt G Q γ₂ = deformedOpExt G (P * Q) (γ₁ + γ₂)

Deforming a product of Pauli operators with the sum of edge-paths gives the product of deformed operators.

Boundary Condition Compatible with Multiplication

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

zSupportOnVertices is additive for Pauli multiplication.

theorem DeformedOperator.boundaryCondition_mul {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P Q : PauliOp V) (γ₁ γ₂ : ↑G.edgeSet → ZMod 2) (h₁ : BoundaryCondition G P γ₁) (h₂ : BoundaryCondition G Q γ₂) : BoundaryCondition G (P * Q) (γ₁ + γ₂)

The boundary condition is compatible with multiplication.

No Z-Support on V

def DeformedOperator.HasNoZSupportOnV {V : Type u_1} (P : PauliOp V) : Prop

A check P has no Z-support on V if its Z-support on vertices is the zero vector.

Equations

• DeformedOperator.HasNoZSupportOnV P = (DeformedOperator.zSupportOnVertices P = 0)

theorem DeformedOperator.noZSupport_boundary_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp V) (h : HasNoZSupportOnV P) : BoundaryCondition G P 0

For a check with no Z-support on V, the boundary condition is satisfied by γ = 0.

Anchor Definition: Deformed Operator

def DeformedOperator.deformedOperator {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] (P : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) (_hbc : BoundaryCondition G P γ) : PauliOp (GaussFlux.ExtQubit G)

The deformed operator P̃ = P · ∏_{e ∈ γ} Z_e on the extended qubit system V ⊕ G.edgeSet. This is the main definition from Definition 3 of the paper. Given P on V and an edge-path γ with ∂γ = S_Z(P)|_V:

• On vertex qubits: acts as P.
• On edge qubits: acts as Z_e if γ(e) = 1, identity otherwise. Commutes with all Gauss's law operators A_v.

Equations

• DeformedOperator.deformedOperator G P γ _hbc = DeformedOperator.deformedOpExt G P γ