Definition 4: Deformed Code

Statement

The deformed code is the stabilizer code defined on the extended qubit system V ⊕ E(G), whose generating checks are:

1. Gauss's law operators {A_v : v ∈ V} — X-type checks from Definition 2
2. Flux operators {B_p : p ∈ C} — Z-type checks from Definition 2
3. Deformed checks {s̃_j} — each original stabilizer check s_j is deformed

Main Results

• deformedCheck : individual deformed check
• DeformedCodeData : edge-paths with boundary conditions for all checks
• gaussLawChecks, fluxChecks, deformedOriginalChecks : the three families of checks
• CheckIndex : the index type V ⊕ C ⊕ J
• allChecks : the full check map
• allChecks_commute : all checks pairwise commute
• allChecks_self_inverse : all checks are self-inverse
• deformedCodeChecks : anchor definition

Corollaries

• Pure X/Z type classification
• Product of Gauss's law checks equals the logical
• Weight of flux checks

Deformed Check

def DeformedCode.deformedCheck {V : Type u_1} (G : SimpleGraph V) (s : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) : PauliOp (GaussFlux.ExtQubit G)

Given an original check s and an edge-path γ satisfying the boundary condition, the deformed check is the deformed operator extension of s by γ.

Equations

• DeformedCode.deformedCheck G s γ = DeformedOperator.deformedOpExt G s γ

theorem DeformedCode.deformedCheck_of_noZSupport {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (s : PauliOp V) (_h : DeformedOperator.HasNoZSupportOnV s) : deformedCheck G s 0 = DeformedOperator.deformedOpExt G s 0

If s has no Z-support on V, the deformed check with γ = 0 acts as s on vertex qubits and as identity on edge qubits.

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

The deformed check commutes with Gauss's law when boundary condition holds.

theorem DeformedCode.deformedCheck_mul_self {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (s : PauliOp V) (γ : ↑G.edgeSet → ZMod 2) : deformedCheck G s γ * deformedCheck G s γ = 1

The deformed check is self-inverse.

Deformed Code Data

structure DeformedCode.DeformedCodeData {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] {J : Type u_3} (checks : J → PauliOp V) : Type (max u_1 u_3)

The deformed code data: for each original check j, an edge-path γ_j and a proof that the boundary condition ∂γ_j = S_Z(s_j)|_V holds.

• edgePath : J → ↑G.edgeSet → ZMod 2
• boundary_condition (j : J) : DeformedOperator.BoundaryCondition G (checks j) (self.edgePath j)

The Three Families of Checks

def DeformedCode.gaussLawChecks {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (v : V) : PauliOp (GaussFlux.ExtQubit G)

Gauss's law checks on the extended system: A_v for each vertex v ∈ V.

Equations

• DeformedCode.gaussLawChecks G v = GaussFlux.gaussLawOp G v

def DeformedCode.fluxChecks {V : Type u_1} (G : SimpleGraph V) {C : Type u_2} (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (p : C) : PauliOp (GaussFlux.ExtQubit G)

Flux checks on the extended system: B_p for each cycle p ∈ C.

Equations

• DeformedCode.fluxChecks G cycles p = GaussFlux.fluxOp G cycles p

def DeformedCode.deformedOriginalChecks {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] {J : Type u_3} (checks : J → PauliOp V) (data : DeformedCodeData G checks) (j : J) : PauliOp (GaussFlux.ExtQubit G)

Deformed original checks: s̃_j for each j ∈ J, using the edge-paths from data.

Equations

• DeformedCode.deformedOriginalChecks G checks data j = DeformedCode.deformedCheck G (checks j) (data.edgePath j)

Check Index Type

inductive DeformedCode.CheckIndex (V : Type u_4) (C : Type u_5) (J : Type u_6) : Type (max (max u_4 u_5) u_6)

The type of all checks in the deformed code: V ⊕ C ⊕ J.

• gaussLaw {V : Type u_4} {C : Type u_5} {J : Type u_6} : V → CheckIndex V C J
• flux {V : Type u_4} {C : Type u_5} {J : Type u_6} : C → CheckIndex V C J
• deformed {V : Type u_4} {C : Type u_5} {J : Type u_6} : J → CheckIndex V C J

def DeformedCode.instDecidableEqCheckIndex.decEq {V✝ : Type u_4} {C✝ : Type u_5} {J✝ : Type u_6} [DecidableEq V✝] [DecidableEq C✝] [DecidableEq J✝] (x✝ x✝¹ : CheckIndex V✝ C✝ J✝) : Decidable (x✝ = x✝¹)

Equations

• DeformedCode.instDecidableEqCheckIndex.decEq (DeformedCode.CheckIndex.gaussLaw a) (DeformedCode.CheckIndex.gaussLaw b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• DeformedCode.instDecidableEqCheckIndex.decEq (DeformedCode.CheckIndex.gaussLaw a) (DeformedCode.CheckIndex.flux a_1) = isFalse ⋯
• DeformedCode.instDecidableEqCheckIndex.decEq (DeformedCode.CheckIndex.gaussLaw a) (DeformedCode.CheckIndex.deformed a_1) = isFalse ⋯
• DeformedCode.instDecidableEqCheckIndex.decEq (DeformedCode.CheckIndex.flux a) (DeformedCode.CheckIndex.gaussLaw a_1) = isFalse ⋯
• DeformedCode.instDecidableEqCheckIndex.decEq (DeformedCode.CheckIndex.flux a) (DeformedCode.CheckIndex.flux b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• DeformedCode.instDecidableEqCheckIndex.decEq (DeformedCode.CheckIndex.flux a) (DeformedCode.CheckIndex.deformed a_1) = isFalse ⋯
• DeformedCode.instDecidableEqCheckIndex.decEq (DeformedCode.CheckIndex.deformed a) (DeformedCode.CheckIndex.gaussLaw a_1) = isFalse ⋯
• DeformedCode.instDecidableEqCheckIndex.decEq (DeformedCode.CheckIndex.deformed a) (DeformedCode.CheckIndex.flux a_1) = isFalse ⋯
• DeformedCode.instDecidableEqCheckIndex.decEq (DeformedCode.CheckIndex.deformed a) (DeformedCode.CheckIndex.deformed b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance DeformedCode.instDecidableEqCheckIndex {V✝ : Type u_4} {C✝ : Type u_5} {J✝ : Type u_6} [DecidableEq V✝] [DecidableEq C✝] [DecidableEq J✝] : DecidableEq (CheckIndex V✝ C✝ J✝)

Equations

• DeformedCode.instDecidableEqCheckIndex = DeformedCode.instDecidableEqCheckIndex.decEq

instance DeformedCode.instFintypeCheckIndex {V : Type u_1} {C : Type u_2} {J : Type u_3} [Fintype V] [Fintype C] [Fintype J] : Fintype (CheckIndex V C J)

Equations

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

All Checks Map

def DeformedCode.allChecks {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] {C : Type u_2} (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} (checks : J → PauliOp V) (data : DeformedCodeData G checks) : CheckIndex V C J → PauliOp (GaussFlux.ExtQubit G)

The full set of checks for the deformed code.

Equations

• DeformedCode.allChecks G cycles checks data (DeformedCode.CheckIndex.gaussLaw v) = DeformedCode.gaussLawChecks G v
• DeformedCode.allChecks G cycles checks data (DeformedCode.CheckIndex.flux p) = DeformedCode.fluxChecks G cycles p
• DeformedCode.allChecks G cycles checks data (DeformedCode.CheckIndex.deformed j) = DeformedCode.deformedOriginalChecks G checks data j

Pairwise Commutation: Gauss-Gauss

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

Gauss's law checks commute with each other.

Pairwise Commutation: Flux-Flux

theorem DeformedCode.allChecks_pairwise_commute_flux_flux {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) : (fluxChecks G cycles p).PauliCommute (fluxChecks G cycles q)

Flux checks commute with each other.

Pairwise Commutation: Gauss-Flux

theorem DeformedCode.allChecks_pairwise_commute_gaussLaw_flux {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) : (gaussLawChecks G v).PauliCommute (fluxChecks G cycles p)

Gauss's law and flux checks commute.

Pairwise Commutation: Gauss-Deformed

theorem DeformedCode.allChecks_pairwise_commute_gaussLaw_deformed {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 : DeformedCodeData G checks) (v : V) (j : J) : (gaussLawChecks G v).PauliCommute (deformedOriginalChecks G checks data j)

Gauss's law checks commute with deformed original checks.

Pairwise Commutation: Deformed-Flux

theorem DeformedCode.allChecks_pairwise_commute_deformed_flux {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 : DeformedCodeData G checks) (j : J) (p : C) : (deformedOriginalChecks G checks data j).PauliCommute (fluxChecks G cycles p)

Deformed and flux checks commute. This holds because flux operators are pure Z-type and deformed checks have no X-support on edges.

Pairwise Commutation: Deformed-Deformed

theorem DeformedCode.allChecks_pairwise_commute_deformed_deformed {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 : DeformedCodeData G checks) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (i j : J) : (deformedOriginalChecks G checks data i).PauliCommute (deformedOriginalChecks G checks data j)

Deformed checks commute if the original checks commute. On edges both are pure Z-type (Z commutes with Z); on vertices the commutation is inherited from the original checks.

All Checks Commute

theorem DeformedCode.allChecks_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 : 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 : CheckIndex V C J) : (allChecks G cycles checks data a).PauliCommute (allChecks G cycles checks data b)

All checks in the deformed code pairwise commute.

Self-Inverse Properties

theorem DeformedCode.gaussLawChecks_mul_self {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : gaussLawChecks G v * gaussLawChecks G v = 1

Gauss's law checks are self-inverse: A_v * A_v = 1.

theorem DeformedCode.fluxChecks_mul_self {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 : C) : fluxChecks G cycles p * fluxChecks G cycles p = 1

Flux checks are self-inverse: B_p * B_p = 1.

theorem DeformedCode.deformedOriginalChecks_mul_self {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 : DeformedCodeData G checks) (j : J) : deformedOriginalChecks G checks data j * deformedOriginalChecks G checks data j = 1

Deformed original checks are self-inverse: s̃_j * s̃_j = 1.

theorem DeformedCode.allChecks_self_inverse {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 : DeformedCodeData G checks) (a : CheckIndex V C J) : allChecks G cycles checks data a * allChecks G cycles checks data a = 1

All checks in the deformed code are self-inverse.

Type Classification

theorem DeformedCode.gaussLawChecks_pure_X {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : (gaussLawChecks G v).zVec = 0

Gauss's law checks are pure X-type: no Z-support.

theorem DeformedCode.fluxChecks_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] (p : C) : (fluxChecks G cycles p).xVec = 0

Flux checks are pure Z-type: no X-support.

theorem DeformedCode.deformedOriginalChecks_no_xSupport_on_edges {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 : DeformedCodeData G checks) (j : J) (e : ↑G.edgeSet) : (deformedOriginalChecks G checks data j).xVec (Sum.inr e) = 0

Deformed checks have no X-support on edge qubits.

Product of Gauss's Law Checks Equals Logical

theorem DeformedCode.gaussLawChecks_product_eq_logical {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : ∏ v : V, gaussLawChecks G v = GaussFlux.logicalOp G

The product of all Gauss's law checks equals the logical operator L.

Constructors for DeformedCodeData

def DeformedCode.mkDeformedCodeData {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] {J : Type u_3} (checks : J → PauliOp V) (edgePaths : J → ↑G.edgeSet → ZMod 2) (hbc : ∀ (j : J), DeformedOperator.BoundaryCondition G (checks j) (edgePaths j)) : DeformedCodeData G checks

Constructor: given edge-paths and boundary proofs, build DeformedCodeData.

Equations

• DeformedCode.mkDeformedCodeData G checks edgePaths hbc = { edgePath := edgePaths, boundary_condition := hbc }

def DeformedCode.mkDeformedCodeData_noZSupport {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {J : Type u_3} (checks : J → PauliOp V) (hnoZ : ∀ (j : J), DeformedOperator.HasNoZSupportOnV (checks j)) : DeformedCodeData G checks

Constructor for when all original checks have no Z-support on V: set all edge-paths to zero.

Equations

• DeformedCode.mkDeformedCodeData_noZSupport G checks hnoZ = { edgePath := fun (x : J) => 0, boundary_condition := ⋯ }

Weight of Flux Checks

theorem DeformedCode.fluxChecks_weight {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 : C) : (fluxChecks G cycles p).weight = {e : ↑G.edgeSet | e ∈ cycles p}.card

The weight of flux check B_p equals the number of edges in the cycle p.

Anchor Definition: deformedCodeChecks

def DeformedCode.deformedCodeChecks {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] {C : Type u_2} (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} (checks : J → PauliOp V) (data : DeformedCodeData G checks) : CheckIndex V C J → PauliOp (GaussFlux.ExtQubit G)

The generating checks for the deformed code on the extended qubit system V ⊕ E(G). This is the main definition from Definition 4 of the paper.

Equations

• DeformedCode.deformedCodeChecks G cycles checks data = DeformedCode.allChecks G cycles checks data

@[simp]

theorem DeformedCode.deformedCodeChecks_gaussLaw {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 : DeformedCodeData G checks) (v : V) : deformedCodeChecks G cycles checks data (CheckIndex.gaussLaw v) = gaussLawChecks G v

@[simp]

theorem DeformedCode.deformedCodeChecks_flux {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 : DeformedCodeData G checks) (p : C) : deformedCodeChecks G cycles checks data (CheckIndex.flux p) = fluxChecks G cycles p

@[simp]

theorem DeformedCode.deformedCodeChecks_deformed {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 : DeformedCodeData G checks) (j : J) : deformedCodeChecks G cycles checks data (CheckIndex.deformed j) = deformedOriginalChecks G checks data j