Lemma 1: Deformed Code Checks

Statement

The operators listed in Definition 4 (Deformed Code) form a valid generating set of commuting checks for a stabilizer code (or subsystem code).

Specifically:

1. All A_v operators commute with each other.
2. All B_p operators commute with each other.
3. All s̃_j operators commute with each other.
4. The A_v operators commute with the B_p operators.
5. The A_v operators commute with the s̃_j operators.
6. The B_p operators commute with the s̃_j operators.

Main Results

• deformedStabilizerCode : the deformed code as a StabilizerCode
• gaussLaw_gaussLaw_commute : [A_v, A_w] = 0
• flux_flux_commute : [B_p, B_q] = 0
• deformed_deformed_commute : [s̃_i, s̃_j] = 0
• gaussLaw_flux_commute : [A_v, B_p] = 0
• gaussLaw_deformed_commute : [A_v, s̃_j] = 0
• flux_deformed_commute : [B_p, s̃_j] = 0
• deformedCodeChecks_allCommute : all checks pairwise commute
• deformedCodeChecks_allSelfInverse : all checks are self-inverse

Corollaries

• deformedStabilizerCode_check_eq : check of the stabilizer code equals deformedCodeChecks
• deformedStabilizerCode_numQubits : number of physical qubits
• deformedStabilizerCode_numChecks : number of stabilizer checks

The Six Commutation Relations

theorem DeformedCodeChecks.gaussLaw_gaussLaw_commute {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v w : V) : (DeformedCode.gaussLawChecks G v).PauliCommute (DeformedCode.gaussLawChecks G w)

(1) All Gauss's law operators commute with each other: A_v and A_w are both pure X-type, so they commute.

theorem DeformedCodeChecks.flux_flux_commute {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (p q : C) : (DeformedCode.fluxChecks G cycles p).PauliCommute (DeformedCode.fluxChecks G cycles q)

(2) All flux operators commute with each other: B_p and B_q are both pure Z-type, so they commute.

theorem DeformedCodeChecks.deformed_deformed_commute {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (i j : J) : (DeformedCode.deformedOriginalChecks G checks data i).PauliCommute (DeformedCode.deformedOriginalChecks G checks data j)

(3) All deformed checks commute with each other: On edges both are pure Z-type; on vertices commutation is inherited from the original checks.

theorem DeformedCodeChecks.gaussLaw_flux_commute {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (v : V) (p : C) : (DeformedCode.gaussLawChecks G v).PauliCommute (DeformedCode.fluxChecks G cycles p)

(4) Gauss's law operators commute with flux operators: The symplectic inner product counts the overlap of X-support(A_v) with Z-support(B_p), which is the number of edges in p incident to v. For a valid cycle, this is always even (0 or 2).

theorem DeformedCodeChecks.gaussLaw_deformed_commute {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (v : V) (j : J) : (DeformedCode.gaussLawChecks G v).PauliCommute (DeformedCode.deformedOriginalChecks G checks data j)

(5) Gauss's law operators commute with deformed checks: The boundary condition ensures the anticommutation signs cancel.

theorem DeformedCodeChecks.flux_deformed_commute {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (p : C) (j : J) : (DeformedCode.fluxChecks G cycles p).PauliCommute (DeformedCode.deformedOriginalChecks G checks data j)

(6) Flux operators commute with deformed checks: B_p is pure Z-type and acts only on edges; s̃_j has no X-support on edges. Since Z commutes with Z and B_p doesn't act on vertex qubits, they commute.

Combined Commutation and Self-Inverse

theorem DeformedCodeChecks.deformedCodeChecks_allCommute {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (a b : DeformedCode.CheckIndex V C J) : (DeformedCode.deformedCodeChecks G cycles checks data a).PauliCommute (DeformedCode.deformedCodeChecks G cycles checks data b)

All deformed code checks pairwise commute.

theorem DeformedCodeChecks.deformedCodeChecks_allSelfInverse {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (a : DeformedCode.CheckIndex V C J) : DeformedCode.deformedCodeChecks G cycles checks data a * DeformedCode.deformedCodeChecks G cycles checks data a = 1

All deformed code checks are self-inverse.

The Deformed Code as a StabilizerCode

def DeformedCodeChecks.deformedStabilizerCode {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) : StabilizerCode (GaussFlux.ExtQubit G)

The deformed code forms a valid stabilizer code on the extended qubit system V ⊕ E(G). The check index type is CheckIndex V C J = V ⊕ C ⊕ J, and the checks are the deformed code checks from Definition 4.

Equations

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

Properties of the Deformed Stabilizer Code

@[simp]

theorem DeformedCodeChecks.deformedStabilizerCode_check_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (a : DeformedCode.CheckIndex V C J) : (deformedStabilizerCode G cycles checks data hcyc hcomm).check a = DeformedCode.deformedCodeChecks G cycles checks data a

theorem DeformedCodeChecks.deformedStabilizerCode_numQubits {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) : (deformedStabilizerCode G cycles checks data hcyc hcomm).numQubits = Fintype.card V + Fintype.card ↑G.edgeSet

The number of physical qubits in the deformed code is |V| + |E|.

theorem DeformedCodeChecks.deformedStabilizerCode_numChecks {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) : (deformedStabilizerCode G cycles checks data hcyc hcomm).numChecks = Fintype.card V + Fintype.card C + Fintype.card J

The number of checks in the deformed code is |V| + |C| + |J|.

Gauss's Law Checks in the Stabilizer Code

theorem DeformedCodeChecks.gaussLaw_mem_stabilizerGroup {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (v : V) : DeformedCode.gaussLawChecks G v ∈ (deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup

Gauss's law checks are in the stabilizer group.

theorem DeformedCodeChecks.flux_mem_stabilizerGroup {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (p : C) : DeformedCode.fluxChecks G cycles p ∈ (deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup

Flux checks are in the stabilizer group.

theorem DeformedCodeChecks.deformed_mem_stabilizerGroup {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (j : J) : DeformedCode.deformedOriginalChecks G checks data j ∈ (deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup

Deformed original checks are in the stabilizer group.

Centralizer Properties

theorem DeformedCodeChecks.gaussLaw_inCentralizer {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (v : V) : (deformedStabilizerCode G cycles checks data hcyc hcomm).inCentralizer (DeformedCode.gaussLawChecks G v)

Gauss's law checks are in the centralizer of the deformed code.

theorem DeformedCodeChecks.flux_inCentralizer {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (p : C) : (deformedStabilizerCode G cycles checks data hcyc hcomm).inCentralizer (DeformedCode.fluxChecks G cycles p)

Flux checks are in the centralizer of the deformed code.

theorem DeformedCodeChecks.deformed_inCentralizer {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (j : J) : (deformedStabilizerCode G cycles checks data hcyc hcomm).inCentralizer (DeformedCode.deformedOriginalChecks G checks data j)

Deformed checks are in the centralizer of the deformed code.

Type Classification in the Stabilizer Code

theorem DeformedCodeChecks.deformedStabilizerCode_gaussLaw_pure_X {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (v : V) : ((deformedStabilizerCode G cycles checks data hcyc hcomm).check (DeformedCode.CheckIndex.gaussLaw v)).zVec = 0

Gauss's law checks in the deformed stabilizer code are pure X-type.

theorem DeformedCodeChecks.deformedStabilizerCode_flux_pure_Z {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (p : C) : ((deformedStabilizerCode G cycles checks data hcyc hcomm).check (DeformedCode.CheckIndex.flux p)).xVec = 0

Flux checks in the deformed stabilizer code are pure Z-type.

theorem DeformedCodeChecks.deformedStabilizerCode_deformed_noXOnEdges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (j : J) (e : ↑G.edgeSet) : ((deformedStabilizerCode G cycles checks data hcyc hcomm).check (DeformedCode.CheckIndex.deformed j)).xVec (Sum.inr e) = 0

Deformed checks in the deformed stabilizer code have no X-support on edge qubits.

The Logical Operator and the Stabilizer Code

theorem DeformedCodeChecks.deformedStabilizerCode_gaussLaw_product {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) : ∏ v : V, (deformedStabilizerCode G cycles checks data hcyc hcomm).check (DeformedCode.CheckIndex.gaussLaw v) = GaussFlux.logicalOp G

The product of all Gauss's law checks in the deformed stabilizer code equals the logical operator L = ∏_{v ∈ V} X_v.