Stabilizer codes: an Abelian S of order 2^a without -1 gives an [[n, n-a, d]] code

Open

QAlgorithms.GottesmanIntro.stabilizerCode_params

by Goku · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

gottesman-introlecture-notesquantum-information

Let $\mathcal P_n$ be the $n$ -qubit Pauli group: the operators $i^c\,\sigma_1\otimes\cdots\otimes\sigma_n$ with $c\in\{0,1,2,3\}$ and $\sigma_j\in\{I,X,Y,Z\}$ . The weight $\mathrm{wt}(Q)$ of a Pauli operator is the number of its tensor factors different from $I$ .

Let $S\le\mathcal P_n$ be an Abelian subgroup of order $|S|=2^a$ with $-I\notin S$ , and let

T(S)=\{\,|\psi\rangle : M|\psi\rangle=|\psi\rangle\ \text{for all } M\in S\,\}

be its stabilized space. Let $N(S)$ be the set of Pauli operators commuting with every element of $S$ (the normalizer of $S$ in $\mathcal P_n$ , which equals its centralizer), and suppose

d=\min\{\mathrm{wt}(Q) : Q\in N(S),\ Q\notin\{i^cM : M\in S,\ c\in\{0,1,2,3\}\}\}

exists (the set is nonempty). Then $T(S)$ is an $[[n,n-a,d]]$ quantum code:

$\dim T(S)=2^{n-a}$ ;
every operator $E$ acting on at most $d-1$ qubits is detectable, i.e. $\langle\psi|E|\psi\rangle$ takes the same value $C(E)$ for every normalized $|\psi\rangle\in T(S)$ ;
some operator acting on at most $d$ qubits is not detectable, so the distance is exactly $d$ .

This is the basic theorem of the stabilizer formalism: it reads the parameters of a quantum code off a group of commuting Pauli operators.

Formalization Note The source writes $N(S)\setminus S$ ; taken literally this set always contains $-I$ (weight $0$ ), so, following the standard convention the source cites, Pauli operators equal to a phase times an element of $S$ are removed. The minimum is encoded with IsLeast, which also excludes the case $a=n$ where the set is empty and the source's $d$ is undefined.

Preamble

import Definitions.Def_QAlgorithms_Defs_QECC
set_option autoImplicit false

Formal statement

namespace QAlgorithms.GottesmanIntro

open Stabilizer

/-- Gottesman intro p.10, Theorem 5: let `S` be an Abelian subgroup of order `2^a` of the
`n`-qubit Pauli group with `−1 ∉ S`, and let `d` be the minimum weight of a Pauli operator in
the normalizer `N(S)` (= the centralizer of `S` in `P_n`, p.10) that is not a phase times an
element of `S`. Then the stabilized space `T(S)` is an `[[n, n − a, d]]` code: it has dimension
`2^(n−a)`, every operator acting on at most `d − 1` qubits satisfies (34) on it, and some
operator acting on `d` qubits does not. The weight of a Pauli operator is the number of
non-identity tensor factors (p.4). The phases `±1, ±i` are removed from `N(S) \ S` since
otherwise `−I` (weight 0) would always lie in it. -/
theorem stabilizerCode_params (n a d : ℕ) (S : Subgroup (Matrix.unitaryGroup (Qubits n) ℂ))
    (hS : IsStabilizerGroup S) (hcard : Nat.card S = 2 ^ a)
    (hd : IsLeast {w : ℕ | ∃ Q ∈ pauliCentralizer S, Q ∉ phaseMultiples S ∧
      ∃ P : PauliString n, (Q : Matrix (Qubits n) (Qubits n) ℂ) = P.toMatrix ∧ P.weight = w} d) :
    IsQCode n (n - a) d (stabilizedSpace S) ∧ HasDistance (stabilizedSpace S) d := by
  sorry


end QAlgorithms.GottesmanIntro

Source

Daniel Gottesman, An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation, 2009, v1, PDF p. 10, Theorem 5. https://arxiv.org/pdf/0904.2557v1

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. Fix natural numbers $n, a, d$ . Let $\mathcal U_n$ be the group of unitary $2^n\times 2^n$ complex matrices, with rows and columns indexed by bit strings $\{0,1\}^n$ . Let $S \le \mathcal U_n$ be a subgroup.

Pauli strings, weight, Pauli group. A Pauli string $P$ consists of:

a phase $c \in \mathbb Z/4$ ;
factors $P_1,\dots,P_n \in \{I,X,Y,Z\}$ , where

X=\begin{pmatrix}0&1\\1&0\end{pmatrix},\quad Y=\begin{pmatrix}0&-i\\ i&0\end{pmatrix},\quad Z=\begin{pmatrix}1&0\\0&-1\end{pmatrix}.

Its matrix is $i^{c}\,P_1\otimes\cdots\otimes P_n$ , with factor $q$ acting on qubit $q$ . Its weight is the number of positions $q$ with $P_q \ne I$ ; the phase is ignored.

The Pauli group $\mathcal P_n \le \mathcal U_n$ is the subgroup generated by all unitaries that equal the matrix of some Pauli string.

Hypotheses.

$S$ is a stabilizer group.
- $S \le \mathcal P_n$ .
- $S$ is abelian.
- No element of $S$ equals the matrix $-I$ .
Size of $S$ . The cardinality of $S$ is $2^a$ . Here the cardinality is a natural number, which would be $0$ for an infinite set; this hypothesis forces $S$ to be finite.
Definition of $d$ . $d$ is the least element of the set $W$ of all $w \in \mathbb N$ for which there is some $Q$ with:
- $Q \in \mathcal P_n$ and $Q$ commutes with every element of $S$ , i.e. $Q$ lies in the Pauli group intersected with the centralizer of $S$ in $\mathcal U_n$ ;
- $Q$ is not of the form $i^{c} M$ with $c \in \mathbb Z/4$ and $M \in S$ ;
- $Q$ equals the matrix of some Pauli string $P$ of weight exactly $w$ .
"Least element" means $d \in W$ and $d \le w$ for all $w \in W$ . In particular, if $W$ is empty this hypothesis cannot be satisfied, and the theorem is vacuous.

The code space. Let

C = \{\psi \in \mathbb C^{2^n} : M\psi = \psi \text{ for all } M\in S\},

the common $+1$ eigenspace of $S$ .

Supporting notions.

Acts on at most $t$ qubits. A matrix $E$ on $n$ qubits does this if there is a set $F$ of at most $t$ wires, and an injective listing $w$ of $k$ wires all lying in $F$ , together with an arbitrary $2^k\times 2^k$ complex matrix $M$ , such that

E_{y,z} = \begin{cases} M_{y\circ w,\; z\circ w} & \text{if } y,z \text{ agree outside the image of } w,\\ 0 & \text{otherwise.}\end{cases}

In other words, $E$ is $M$ on those wires tensored with the identity elsewhere. $M$ need not be unitary.

Detectable. $E$ is detectable on $C$ if there is one constant $c\in\mathbb C$ with $\langle \psi, E\psi\rangle = \psi^\dagger E\psi = c$ for every unit vector $\psi \in C$ .

Conclusion. Both of the following hold.

$C$ is an $[[n,\, n-a,\, d]]$ code in the following sense:
- $\dim_{\mathbb C} C = 2^{\,n-a}$ , where $n-a$ is truncated subtraction, so it is $0$ if $a > n$ ;
- every matrix acting on at most $d-1$ qubits is detectable on $C$ , again with truncated subtraction, so $d-1=0$ when $d=0$ .
$C$ has distance $d$ :
- every matrix acting on at most $d-1$ qubits is detectable on $C$ ;
- there exists a matrix acting on at most $d$ qubits that is not detectable on $C$ .

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Goku · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph