Notation: Stabilizer Codes

Statement

An [[n,k,d]] stabilizer code encodes k logical qubits into n physical qubits with code distance d. The code is specified by a set of commuting Pauli operators called stabilizer checks {s_i} that generate the stabilizer group S. The codespace is the simultaneous +1 eigenspace of all stabilizer checks. A logical operator is a Pauli operator that commutes (in the full Pauli group) with all stabilizers but is not itself a stabilizer (i.e., lies in the centralizer C(S) but not in S). The distance d is the minimum weight of a non-trivial logical operator. A quantum low-density parity-check (qLDPC) code is a stabilizer code where each check has weight bounded by a constant w and each qubit participates in at most a constant number c of checks.

Main Results

• PauliOp.symplecticInner: symplectic inner product determining commutation
• PauliOp.PauliCommute: two Pauli operators commute iff symplectic inner product is 0
• StabilizerCode: stabilizer code structure with checks and commutativity condition
• StabilizerCode.stabilizerGroup: the stabilizer group generated by the checks
• StabilizerCode.inCentralizer: centralizer membership predicate
• StabilizerCode.isLogicalOp: predicate for non-trivial logical operators
• StabilizerCode.distance: the code distance
• IsQLDPC: predicate characterizing quantum LDPC codes

Corollaries

• Basic properties of symplectic inner product
• Stabilizer group contained in centralizer
• Check weight and qubit degree characterizations

Symplectic inner product

In the full Pauli group (with phases), two Pauli operators P, Q commute iff their symplectic inner product ⟨P, Q⟩ = Σ_v (P.x_v · Q.z_v + P.z_v · Q.x_v) = 0 in ZMod 2.

def PauliOp.symplecticInner {V : Type u_1} [Fintype V] (P Q : PauliOp V) : ZMod 2

The symplectic inner product of two Pauli operators, determining commutation in the full Pauli group: P and Q commute iff symplecticInner P Q = 0.

Equations

• P.symplecticInner Q = ∑ v : V, (P.xVec v * Q.zVec v + P.zVec v * Q.xVec v)

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

Two Pauli operators commute (in the full Pauli group, including phases) iff their symplectic inner product vanishes.

Equations

• P.PauliCommute Q = (P.symplecticInner Q = 0)

@[simp]

theorem PauliOp.symplecticInner_self {V : Type u_1} [Fintype V] (P : PauliOp V) : P.symplecticInner P = 0

theorem PauliOp.pauliCommute_self {V : Type u_1} [Fintype V] (P : PauliOp V) : P.PauliCommute P

theorem PauliOp.pauliCommute_comm {V : Type u_1} [Fintype V] (P Q : PauliOp V) : P.PauliCommute Q ↔ Q.PauliCommute P

@[simp]

theorem PauliOp.symplecticInner_one_left {V : Type u_1} [Fintype V] (Q : PauliOp V) : symplecticInner 1 Q = 0

@[simp]

theorem PauliOp.symplecticInner_one_right {V : Type u_1} [Fintype V] (P : PauliOp V) : P.symplecticInner 1 = 0

theorem PauliOp.pauliCommute_one_left {V : Type u_1} [Fintype V] (Q : PauliOp V) : PauliCommute 1 Q

theorem PauliOp.pauliCommute_one_right {V : Type u_1} [Fintype V] (P : PauliOp V) : P.PauliCommute 1

theorem PauliOp.symplecticInner_mul_left {V : Type u_1} [Fintype V] (P Q R : PauliOp V) : (P * Q).symplecticInner R = P.symplecticInner R + Q.symplecticInner R

Symplectic inner product is additive in the first argument (over ZMod 2).

theorem PauliOp.symplecticInner_mul_right {V : Type u_1} [Fintype V] (P Q R : PauliOp V) : P.symplecticInner (Q * R) = P.symplecticInner Q + P.symplecticInner R

Symplectic inner product is additive in the second argument (over ZMod 2).

Stabilizer Code

structure StabilizerCode (V : Type u_2) [DecidableEq V] [Fintype V] : Type (max u_2 (u_3 + 1))

A stabilizer code on qubits labeled by type V, specified by a finite index type I for stabilizer checks and a map from I to Pauli operators, with the condition that all checks pairwise commute (in the full Pauli group).

• I : Type u_3

  Index type for stabilizer checks

• instFintypeI : Fintype self.I

  Finite type instance for check indices

• check : self.I → PauliOp V

  The stabilizer checks: each index i gives a Pauli operator s_i

• checks_commute (i j : self.I) : (self.check i).PauliCommute (self.check j)

  All stabilizer checks pairwise commute in the full Pauli group

The stabilizer group

def StabilizerCode.stabilizerGroup {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) : Subgroup (PauliOp V)

The stabilizer group S is the subgroup of PauliOp V generated by the checks.

Equations

• C.stabilizerGroup = Subgroup.closure (Set.range C.check)

theorem StabilizerCode.check_mem_stabilizerGroup {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) (i : C.I) : C.check i ∈ C.stabilizerGroup

Centralizer: operators commuting with all stabilizers

def StabilizerCode.inCentralizer {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) (P : PauliOp V) : Prop

A Pauli operator P is in the centralizer of the stabilizer code if it commutes (in the full Pauli group) with every stabilizer check.

Equations

• C.inCentralizer P = ∀ (i : C.I), P.PauliCommute (C.check i)

def StabilizerCode.centralizerSet {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) : Set (PauliOp V)

The set of Pauli operators in the centralizer of the stabilizer code.

Equations

• C.centralizerSet = {P : PauliOp V | C.inCentralizer P}

theorem StabilizerCode.one_inCentralizer {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) : C.inCentralizer 1

theorem StabilizerCode.check_inCentralizer {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) (i : C.I) : C.inCentralizer (C.check i)

Logical operators

def StabilizerCode.isLogicalOp {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) (P : PauliOp V) : Prop

A Pauli operator P is a non-trivial logical operator if:

1. It commutes with all stabilizers (is in the centralizer)
2. It is not in the stabilizer group
3. It is not the identity

Equations

• C.isLogicalOp P = (C.inCentralizer P ∧ P ∉ C.stabilizerGroup ∧ P ≠ 1)

theorem StabilizerCode.isLogicalOp_inCentralizer {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) {P : PauliOp V} (h : C.isLogicalOp P) : C.inCentralizer P

theorem StabilizerCode.isLogicalOp_not_mem_stabilizerGroup {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) {P : PauliOp V} (h : C.isLogicalOp P) : P ∉ C.stabilizerGroup

theorem StabilizerCode.isLogicalOp_ne_one {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) {P : PauliOp V} (h : C.isLogicalOp P) : P ≠ 1

Code distance

noncomputable def StabilizerCode.distance {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) : ℕ

The code distance is the minimum weight of a non-trivial logical operator. Defined as the infimum of the set of weights. Returns 0 if no logical operators exist.

Equations

• C.distance = sInf {w : ℕ | ∃ (P : PauliOp V), C.isLogicalOp P ∧ P.weight = w}

def StabilizerCode.numQubits {V : Type u_2} [DecidableEq V] [Fintype V] (_C : StabilizerCode V) : ℕ

The number of physical qubits.

Equations

• _C.numQubits = Fintype.card V

def StabilizerCode.numChecks {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) : ℕ

The number of stabilizer checks.

Equations

• C.numChecks = Fintype.card C.I

Code parameters [[n, k, d]]

def StabilizerCode.HasParameters {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) (n k d : ℕ) : Prop

A stabilizer code has parameters [[n, k, d]] if it has n physical qubits, encodes k logical qubits, and has distance d.

Equations

• C.HasParameters n k d = (Fintype.card V = n ∧ n - C.numChecks = k ∧ C.distance = d)

Check weight and qubit participation

def StabilizerCode.checkWeight {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) (i : C.I) : ℕ

The weight of the i-th stabilizer check.

Equations

• C.checkWeight i = (C.check i).weight

noncomputable def StabilizerCode.qubitDegree {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) (v : V) : ℕ

The number of checks that act non-trivially on qubit v.

Equations

• C.qubitDegree v = {i : C.I | v ∈ (C.check i).support}.card

Quantum LDPC codes

def IsQLDPC {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) (w c : ℕ) : Prop

A quantum low-density parity-check (qLDPC) code is a stabilizer code where:

1. Each check has weight bounded by a constant w (each check acts on at most w qubits)
2. Each qubit participates in at most a constant number c of checks

Equations

• IsQLDPC C w c = ((∀ (i : C.I), C.checkWeight i ≤ w) ∧ ∀ (v : V), C.qubitDegree v ≤ c)

Basic properties

@[simp]

theorem StabilizerCode.numQubits_eq {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) : C.numQubits = Fintype.card V

@[simp]

theorem StabilizerCode.numChecks_eq {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) : C.numChecks = Fintype.card C.I

theorem StabilizerCode.not_isLogicalOp_one {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) : ¬C.isLogicalOp 1

The identity is not a logical operator.

theorem StabilizerCode.stabilizerGroup_subset_centralizer {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) (P : PauliOp V) : P ∈ C.stabilizerGroup → C.inCentralizer P

The stabilizer group is contained in the centralizer.

theorem StabilizerCode.not_isLogicalOp_check {V : Type u_2} [DecidableEq V] [Fintype V] (C : StabilizerCode V) (i : C.I) : ¬C.isLogicalOp (C.check i)

A check is not a logical operator.