Every error syndrome of a stabilizer is realized by a Pauli error

Proved

QAlgorithms.GottesmanIntro.exists_pauli_of_syndrome

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 and let $g_1,\dots,g_a\in\mathcal P_n$ generate a stabilizer $S=\langle g_1,\dots,g_a\rangle$ , that is, an Abelian subgroup of $\mathcal P_n$ with $-I\notin S$ , and suppose the generators are independent, i.e. $|S|=2^a$ . The error syndrome of a Pauli operator $E$ is the vector in $\mathbb F_2^a$ whose $i$ -th bit is $0$ if $g_i$ commutes with $E$ and $1$ if it anticommutes.

Then for every $v\in\mathbb F_2^a$ there is $E\in\mathcal P_n$ with syndrome $v$ :

g_iE=Eg_i\ \text{ if } v_i=0,\qquad g_iE=-Eg_i\ \text{ if } v_i=1\qquad(i=1,\dots,a).

This lemma is the step in the proof of the dimension count of stabilizer codes (Theorem 5) that shows all $2^a$ syndrome subspaces are nonempty.

Formalization Note The syndrome is relative to the generator list, as in the source's proof; the independence of the generators (used in the proof as linear independence of their binary vectors) is the hypothesis $|S|=2^a$ . The anticommutation clause is stated explicitly.

Preamble

import Definitions.Def_QAlgorithms_Defs_QECC
set_option autoImplicit false

Formal statement

namespace QAlgorithms.GottesmanIntro

open Stabilizer


/-- Gottesman intro p.12–13, Lemma 1: given a stabilizer `S` (an Abelian subgroup of `P_n`
with `−1 ∉ S`) with independent generators `g_1, …, g_a` (so `|S| = 2^a`), every error syndrome
`v ∈ F_2^a` is the syndrome of some Pauli operator `E`: `E` commutes with `g_i` when `v_i = 0`
and anticommutes with `g_i` when `v_i = 1`. -/
theorem exists_pauli_of_syndrome (n a : ℕ) (g : Fin a → Matrix.unitaryGroup (Qubits n) ℂ)
    (hS : IsStabilizerGroup (Subgroup.closure (Set.range g)))
    (hcard : Nat.card (Subgroup.closure (Set.range g)) = 2 ^ a) (v : Fin a → ZMod 2) :
    ∃ E ∈ pauliGroup n, ∀ i : Fin a,
      (v i = 0 → (g i : Matrix (Qubits n) (Qubits n) ℂ) * E = E * g i) ∧
      (v i = 1 → (g i : Matrix (Qubits n) (Qubits n) ℂ) * E = -((E : Matrix (Qubits n) (Qubits n) ℂ) * g i)) := by
  sorry

end QAlgorithms.GottesmanIntro

Source

Daniel Gottesman, An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation, 2009, v1, PDF p. 12, Lemma 1. 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$ and $a$ . Let $g_1,\dots,g_a$ be unitary $2^n\times 2^n$ complex matrices, indexed by $0,\dots,a-1$ in the code, with rows and columns indexed by $\{0,1\}^n$ . Let $G = \langle g_1,\dots,g_a\rangle$ be the subgroup of the unitary group they generate.

Pauli group. $\mathcal P_n$ is the subgroup of the unitary group generated by all matrices of the form

i^{c}\,P_1\otimes\cdots\otimes P_n,\qquad c\in\mathbb Z/4,\ P_q\in\{I,X,Y,Z\}.

Hypotheses.

$G$ is a stabilizer group.
- $G \le \mathcal P_n$ .
- $G$ is abelian.
- No element of $G$ equals $-I$ .
Size of $G$ . $G$ has exactly $2^a$ elements. This forces $G$ to be finite.

Conclusion. For every binary vector $v \in (\mathbb Z/2)^a$ there exists $E \in \mathcal P_n$ such that, for each $i$ :

v_i = 0 \;\Longrightarrow\; g_i E = E g_i, \qquad v_i = 1 \;\Longrightarrow\; g_i E = -\,E g_i,

as matrix equalities.

Degenerate case. When $a = 0$ there are no generators. Then $G$ is trivial, the size hypothesis reads $1 = 2^0$ , and the conclusion holds for any $E \in \mathcal P_n$ , e.g. the identity.

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