Rem_1: Stabilizer Code Convention

Statement

Throughout this work, we consider an $[[n,k,d]]$ quantum low-density parity-check (qLDPC) stabilizer code on $n$ physical qubits, encoding $k$ logical qubits with distance $d$. The code is specified by a set of stabilizer checks $\{s_i\}$. A logical operator $L$ is a Pauli operator that commutes with all stabilizers but is not itself a stabilizer. By choosing an appropriate single-qubit basis for each physical qubit, we ensure that the logical operator $L$ being measured is a product of Pauli-$X$ matrices: $L = \prod_{v \in \text{supp}(L)} X_v$, where $\text{supp}(L)$ denotes the set of qubits on which $L$ acts non-trivially.

Main Definitions

• StabPauliType : The four single-qubit Pauli operators (I, X, Y, Z)
• PauliOp : A Pauli operator on n qubits (tensor product of single-qubit Paulis)
• StabilizerCode : An [[n,k,d]] stabilizer code specification
• LogicalOp : A logical operator (commutes with stabilizers, not a stabilizer)
• XTypeLogical : A logical operator that is purely X-type (convention for L)

Key Properties

• XTypeLogical.support_eq : L acts as X on exactly supp(L)
• XTypeLogical.commutes_with_stabilizers : L commutes with all stabilizers
• XTypeLogical.not_in_stabilizer_group : L is not itself a stabilizer

Pauli Operators

inductive StabPauliType : Type

The four single-qubit Pauli operators

• I : StabPauliType
• X : StabPauliType
• Y : StabPauliType
• Z : StabPauliType

instance instDecidableEqStabPauliType : DecidableEq StabPauliType

Equations

• instDecidableEqStabPauliType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instReprStabPauliType : Repr StabPauliType

Equations

• instReprStabPauliType = { reprPrec := instReprStabPauliType.repr }

def instReprStabPauliType.repr : StabPauliType → ℕ → Std.Format

Equations

• instReprStabPauliType.repr StabPauliType.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "StabPauliType.I")).group prec✝
• instReprStabPauliType.repr StabPauliType.X prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "StabPauliType.X")).group prec✝
• instReprStabPauliType.repr StabPauliType.Y prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "StabPauliType.Y")).group prec✝
• instReprStabPauliType.repr StabPauliType.Z prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "StabPauliType.Z")).group prec✝

def instInhabitedStabPauliType.default : StabPauliType

Equations

• instInhabitedStabPauliType.default = StabPauliType.I

instance instInhabitedStabPauliType : Inhabited StabPauliType

Equations

• instInhabitedStabPauliType = { default := instInhabitedStabPauliType.default }

def StabPauliType.mul : StabPauliType → StabPauliType → StabPauliType

Multiplication of Pauli types (ignoring phase)

Equations

• StabPauliType.I.mul x✝ = x✝
• x✝.mul StabPauliType.I = x✝
• StabPauliType.X.mul StabPauliType.X = StabPauliType.I
• StabPauliType.Y.mul StabPauliType.Y = StabPauliType.I
• StabPauliType.Z.mul StabPauliType.Z = StabPauliType.I
• StabPauliType.X.mul StabPauliType.Y = StabPauliType.Z
• StabPauliType.Y.mul StabPauliType.X = StabPauliType.Z
• StabPauliType.Y.mul StabPauliType.Z = StabPauliType.X
• StabPauliType.Z.mul StabPauliType.Y = StabPauliType.X
• StabPauliType.Z.mul StabPauliType.X = StabPauliType.Y
• StabPauliType.X.mul StabPauliType.Z = StabPauliType.Y

instance StabPauliType.instMul : Mul StabPauliType

Equations

• StabPauliType.instMul = { mul := StabPauliType.mul }

@[simp]

theorem StabPauliType.mul_I (p : StabPauliType) : p * I = p

@[simp]

theorem StabPauliType.I_mul (p : StabPauliType) : I * p = p

@[simp]

theorem StabPauliType.mul_self (p : StabPauliType) : p * p = I

def StabPauliType.isNontrivial (p : StabPauliType) : Bool

A Pauli type acts nontrivially iff it is not the identity

Equations

• StabPauliType.I.isNontrivial = false
• p.isNontrivial = true

def StabPauliType.isXType (p : StabPauliType) : Bool

A Pauli is X-type if it involves X (i.e., is X or Y)

Equations

• StabPauliType.X.isXType = true
• StabPauliType.Y.isXType = true
• p.isXType = false

def StabPauliType.isZType (p : StabPauliType) : Bool

A Pauli is Z-type if it involves Z (i.e., is Z or Y)

Equations

• StabPauliType.Z.isZType = true
• StabPauliType.Y.isZType = true
• p.isZType = false

def StabPauliType.commutes (p q : StabPauliType) : Bool

Two Paulis commute iff they are equal, one is identity, or they are both in {X,Z}

Equations

• StabPauliType.I.commutes q = true
• p.commutes StabPauliType.I = true
• StabPauliType.X.commutes StabPauliType.X = true
• StabPauliType.Y.commutes StabPauliType.Y = true
• StabPauliType.Z.commutes StabPauliType.Z = true
• StabPauliType.X.commutes StabPauliType.Z = false
• StabPauliType.Z.commutes StabPauliType.X = false
• StabPauliType.X.commutes StabPauliType.Y = false
• StabPauliType.Y.commutes StabPauliType.X = false
• StabPauliType.Y.commutes StabPauliType.Z = false
• StabPauliType.Z.commutes StabPauliType.Y = false

theorem StabPauliType.commutes_comm (p q : StabPauliType) : p.commutes q = q.commutes p

Multi-qubit Pauli Operators

structure PauliOp (n : ℕ) : Type

A Pauli operator on n qubits is a function from qubit indices to Pauli types, together with a global phase (±1, ±i represented as ZMod 4)

• paulis : Fin n → StabPauliType

  The Pauli type on each qubit

• phase : ZMod 4

  The global phase: 0 = +1, 1 = +i, 2 = -1, 3 = -i

theorem PauliOp.ext {n : ℕ} {x y : PauliOp n} (paulis : x.paulis = y.paulis) (phase : x.phase = y.phase) : x = y

theorem PauliOp.ext_iff {n : ℕ} {x y : PauliOp n} : x = y ↔ x.paulis = y.paulis ∧ x.phase = y.phase

def instDecidableEqPauliOp.decEq {n✝ : ℕ} (x✝ x✝¹ : PauliOp n✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqPauliOp.decEq { paulis := a, phase := a_1 } { paulis := b, phase := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance instDecidableEqPauliOp {n✝ : ℕ} : DecidableEq (PauliOp n✝)

Equations

• instDecidableEqPauliOp = instDecidableEqPauliOp.decEq

def PauliOp.identity (n : ℕ) : PauliOp n

The identity operator on n qubits

Equations

• PauliOp.identity n = { paulis := fun (x : Fin n) => StabPauliType.I, phase := 0 }

def PauliOp.support {n : ℕ} (P : PauliOp n) : Finset (Fin n)

The support of a Pauli operator: qubits where it acts nontrivially

Equations

• P.support = {i : Fin n | P.paulis i ≠ StabPauliType.I}

def PauliOp.xSupport {n : ℕ} (P : PauliOp n) : Finset (Fin n)

The X-type support: qubits where P acts as X or Y

Equations

• P.xSupport = {i : Fin n | (P.paulis i).isXType = true}

def PauliOp.zSupport {n : ℕ} (P : PauliOp n) : Finset (Fin n)

The Z-type support: qubits where P acts as Z or Y

Equations

• P.zSupport = {i : Fin n | (P.paulis i).isZType = true}

def PauliOp.commutes {n : ℕ} (P Q : PauliOp n) : Prop

Two Pauli operators commute (ignoring global phase) iff they have an even number of positions where their Pauli types anticommute

Equations

• P.commutes Q = ({i : Fin n | (!(P.paulis i).commutes (Q.paulis i)) = true}.card % 2 = 0)

def PauliOp.isPurelyXType {n : ℕ} (P : PauliOp n) : Prop

A Pauli operator is purely X-type if it only contains I and X

Equations

• P.isPurelyXType = ∀ (i : Fin n), P.paulis i = StabPauliType.I ∨ P.paulis i = StabPauliType.X

def PauliOp.pureX {n : ℕ} (S : Finset (Fin n)) : PauliOp n

Construct a pure X-type operator from a set of qubits

Equations

• PauliOp.pureX S = { paulis := fun (i : Fin n) => if i ∈ S then StabPauliType.X else StabPauliType.I, phase := 0 }

@[simp]

theorem PauliOp.pureX_paulis_mem {n : ℕ} (S : Finset (Fin n)) (i : Fin n) (h : i ∈ S) : (pureX S).paulis i = StabPauliType.X

@[simp]

theorem PauliOp.pureX_paulis_not_mem {n : ℕ} (S : Finset (Fin n)) (i : Fin n) (h : i ∉ S) : (pureX S).paulis i = StabPauliType.I

theorem PauliOp.pureX_isPurelyXType {n : ℕ} (S : Finset (Fin n)) : (pureX S).isPurelyXType

@[simp]

theorem PauliOp.pureX_support {n : ℕ} (S : Finset (Fin n)) : (pureX S).support = S

@[simp]

theorem PauliOp.pureX_xSupport {n : ℕ} (S : Finset (Fin n)) : (pureX S).xSupport = S

@[simp]

theorem PauliOp.pureX_zSupport {n : ℕ} (S : Finset (Fin n)) : (pureX S).zSupport = ∅

Stabilizer Codes

structure StabilizerGroup (n : ℕ) : Type

A stabilizer group on n qubits is a subgroup of the Pauli group. For simplicity, we represent it as a set of generators (the stabilizer checks).

• generators : Set (PauliOp n)

  The generating stabilizer checks

• finite_generators : self.generators.Finite

  Generators are finite

• generators_commute (s₁ s₂ : PauliOp n) : s₁ ∈ self.generators → s₂ ∈ self.generators → s₁.commutes s₂

  All generators mutually commute

structure StabilizerCode : Type

An [[n, k, d]] stabilizer code specification

• n : ℕ

  Number of physical qubits

• k : ℕ

  Number of logical qubits encoded

• d : ℕ

  Code distance

• stabilizers : StabilizerGroup self.n

  The stabilizer group

• n_ge_k : self.n ≥ self.k

  Basic constraint: n ≥ k

• d_pos : self.d > 0

  Distance is positive

def StabilizerCode.commutesWithStabilizers (C : StabilizerCode) (P : PauliOp C.n) : Prop

A Pauli operator commutes with the stabilizer group iff it commutes with all generators

Equations

• C.commutesWithStabilizers P = ∀ s ∈ C.stabilizers.generators, P.commutes s

def StabilizerCode.centralizer (C : StabilizerCode) : Set (PauliOp C.n)

The centralizer: all Paulis that commute with all stabilizers

Equations

• C.centralizer = {P : PauliOp C.n | C.commutesWithStabilizers P}

def StabilizerCode.inStabilizerGroup (C : StabilizerCode) (P : PauliOp C.n) : Prop

A Pauli is in the stabilizer group if it can be generated by products of generators

Equations

• C.inStabilizerGroup P = ∃ (gens : Finset (PauliOp C.n)), ↑gens ⊆ C.stabilizers.generators ∧ (gens = ∅ → P = PauliOp.identity C.n) ∧ P ∈ C.stabilizers.generators ∨ P = PauliOp.identity C.n

Logical Operators

structure LogicalOp (C : StabilizerCode) : Type

A logical operator for a stabilizer code:

• Commutes with all stabilizers
• Is not itself in the stabilizer group

• op : PauliOp C.n

  The underlying Pauli operator

• commutes_with_stabilizers : C.commutesWithStabilizers self.op

  Commutes with all stabilizers

• not_in_stabilizer_group : ¬C.inStabilizerGroup self.op

  Not in the stabilizer group

def LogicalOp.support {C : StabilizerCode} (L : LogicalOp C) : Finset (Fin C.n)

The support of a logical operator

Equations

• L.support = L.op.support

def LogicalOp.xSupport {C : StabilizerCode} (L : LogicalOp C) : Finset (Fin C.n)

The X-type support of a logical operator

Equations

• L.xSupport = L.op.xSupport

def LogicalOp.zSupport {C : StabilizerCode} (L : LogicalOp C) : Finset (Fin C.n)

The Z-type support of a logical operator

Equations

• L.zSupport = L.op.zSupport

X-Type Logical Operator Convention

structure XTypeLogical (C : StabilizerCode) extends LogicalOp C : Type

An X-type logical operator: a logical that is purely X-type (only I and X Paulis). This captures the convention: L = ∏_{v ∈ supp(L)} X_v

• op : PauliOp C.n
• commutes_with_stabilizers : C.commutesWithStabilizers self.op
• not_in_stabilizer_group : ¬C.inStabilizerGroup self.op
• is_purely_xtype : self.op.isPurelyXType

  The operator is purely X-type

@[simp]

theorem XTypeLogical.support_eq_xSupport {C : StabilizerCode} (L : XTypeLogical C) : L.support = L.xSupport

For an X-type logical, supp(L) = X-type support

@[simp]

theorem XTypeLogical.zSupport_empty {C : StabilizerCode} (L : XTypeLogical C) : L.zSupport = ∅

For an X-type logical, the Z-type support is empty

def XTypeLogical.fromSupport (C : StabilizerCode) (S : Finset (Fin C.n)) (h_commutes : C.commutesWithStabilizers (PauliOp.pureX S)) (h_not_stab : ¬C.inStabilizerGroup (PauliOp.pureX S)) : XTypeLogical C

Construct an X-type logical from a support set (assuming the properties hold)

Equations

• XTypeLogical.fromSupport C S h_commutes h_not_stab = { op := PauliOp.pureX S, commutes_with_stabilizers := h_commutes, not_in_stabilizer_group := h_not_stab, is_purely_xtype := ⋯ }

@[simp]

theorem XTypeLogical.fromSupport_support (C : StabilizerCode) (S : Finset (Fin C.n)) (h₁ : C.commutesWithStabilizers (PauliOp.pureX S)) (h₂ : ¬C.inStabilizerGroup (PauliOp.pureX S)) : (fromSupport C S h₁ h₂).support = S

theorem XTypeLogical.product_representation {C : StabilizerCode} (L : XTypeLogical C) : L.op.paulis = (PauliOp.pureX L.support).paulis

The representation theorem: L = ∏_{v ∈ supp(L)} X_v (ignoring global phase). The Pauli content of L on each qubit matches pureX of the support.

LDPC Property

structure IsLDPC (C : StabilizerCode) : Type

A code is Low-Density Parity-Check (LDPC) if there's a constant bound on:

• The weight of each stabilizer check
• The number of checks each qubit participates in

• max_check_weight : ℕ

  Maximum weight of any stabilizer check

• max_qubit_degree : ℕ

  Maximum number of checks any qubit is in

• check_weight_bound (s : PauliOp C.n) : s ∈ C.stabilizers.generators → s.support.card ≤ self.max_check_weight

  All checks have bounded weight

• qubit_degree_bound (i : Fin C.n) : {s ∈ ⋯.toFinset | i ∈ s.support}.card ≤ self.max_qubit_degree

  All qubits have bounded degree

Summary of Convention

The key convention established:

1. We work with [[n,k,d]] qLDPC stabilizer codes
2. Codes are specified by stabilizer checks {sᵢ}
3. Logical operators commute with stabilizers but aren't stabilizers themselves
4. The logical L being measured is always X-type: L = ∏_{v ∈ supp(L)} Xᵥ
5. supp(L) is exactly the qubits where L acts nontrivially