Correctness for the ideal decoder implies correctness for a *-decoder

Open

QAlgorithms.GottesmanIntro.exRecCorrectStar_of_exRecCorrect

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

gottesman-introlecture-notesquantum-information

This lemma lets the level-reduction argument keep track of error syndromes.

Fix a fault-tolerant protocol for an $[[n,1,2t+1]]$ code with ideal decoder $\mathcal D$ . A *-decoder is a unitary $W$ from one code block to one qubit together with a syndrome register $S$ , such that discarding the syndrome gives the ideal decoder:

\operatorname{Tr}_S\bigl(W\rho W^\dagger\bigr) = \mathcal D(\rho) \quad \text{for all } \rho .

Let an ExRec of any type be given, with a fixed Pauli fault arrangement, either full or with some trailing EC steps removed. If the ExRec is correct for the ideal decoder, then it is correct for $W$ :

Gate or wait ExRec with gate $U$ on $k$ blocks: there is a quantum operation $V$ on the $k$ syndrome registers such that $\mathcal W^{\otimes k}\circ \mathrm{EC}^{\mathrm{trail}}\circ G_U\circ \mathrm{EC}^{\mathrm{lead}} = (\mathcal U\otimes V)\circ \mathcal W^{\otimes k}\circ \mathrm{EC}^{\mathrm{lead}}$ , with $\mathcal W(\rho) = W\rho W^\dagger$ (eq. (83)). The operation $V$ may depend on the faults and on $U$ .
Preparation ExRec: $W\,\mathrm{EC}^{\mathrm{trail}}(\rho_{\mathrm{prep}})\,W^\dagger = |0\rangle\langle 0|\otimes\tau$ for some syndrome state $\tau$ .
Measurement ExRec: the syndrome is discarded immediately, so the condition is diagram (74) with $\operatorname{Tr}_S(W\cdot W^\dagger)$ in place of $\mathcal D$ .

All equalities are of superoperators.

Formalization Note The truncation set may be empty (the lemma as stated) or not: the source says on p.39 that Lemma 2 'also works for truncated ExRecs', and Lemma 3 uses it that way. The fault-tolerance hypothesis on the protocol is the section's standing context (the ExRec is built from fault-tolerant gadgets).

Preamble

import Definitions.Def_QAlgorithms_Defs_FTCircuit
set_option autoImplicit false

Formal statement

namespace QAlgorithms.GottesmanIntro



/-- Gottesman intro p.38, Lemma 2: "If an ExRec is correct for an ideal decoder, it is correct
for a *-decoder." Let `P` be a fault-tolerant protocol and `W` a *-decoder for its ideal decoder
(a unitary from a block to one qubit ⊗ a syndrome register `Fin σ` whose syndrome-discarded
version is `P.dec`, p.37–38). For every ExRec type `κ`, every Pauli fault arrangement `F` and
every set `trunc` of removed trailing ECs (`∅` for a full ExRec; p.39: Lemma 2 "also works for
truncated ExRecs"), if the ExRec is correct for the ideal decoder then it is correct for `W`:
for a gate or wait ExRec, eq. (83) holds for some quantum operation `V` on the syndrome
registers (chosen after the faults); for a preparation ExRec, the *-decoded output is
`|0⟩⟨0| ⊗ τ` for some syndrome state `τ`; for a measurement ExRec, the syndrome is discarded. -/
theorem exRecCorrectStar_of_exRecCorrect (P : FTProtocol) (hP : P.IsFaultTolerant) {σ : ℕ}
    (W : Matrix (Bool × Fin σ) (Qubits P.n) ℂ) (hW : IsStarDecoder P.dec W) (κ : LocKind)
    (F : ExRecFaults κ) (trunc : Finset (Fin κ.trailCount)) (hcorr : ExRecCorrect P κ F trunc) :
    ExRecCorrectStar P W κ F trunc := by
  sorry


end QAlgorithms.GottesmanIntro

Source

Daniel Gottesman, An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation, 2009, v1, PDF p. 38, §5.2, Lemma 2. https://arxiv.org/pdf/0904.2557v1

Read-back

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

The protocol. $P$ is a protocol (code $\mathcal C\subseteq\mathbb C^{2^n}$ , encoder $\mathrm{enc}$ , decoder $\mathrm{dec}$ , gadgets $G_\kappa$ , EC circuit, classical decoding $\mathrm{md}$ , parameter $t$ ) satisfying the full fault-tolerance condition $h_P$ . This condition comprises:

the code is 2-dimensional and detects every operator supported on $\le 2t$ qubits;
$\mathrm{enc}$ is an isometry onto $\mathcal C$ ;
$\mathrm{dec}$ is a Kraus channel that perfectly decodes encoded states hit by any operator in the span of weight- $\le t$ Pauli strings, up to the factor $\|E\,\mathrm{enc}\,\psi\|^2$ ;
all gadgets are well-formed with the expected live-qubit flows;
the properties Meas, Prep A/B, Gate A/B and EC A/B hold under fault counts plus filter levels $\le t$ .

The matrix $W$ . $\sigma$ is a natural number and $W$ is a $(2\sigma)\times 2^n$ complex matrix, with rows indexed by pairs (bit, element of $\{0,\dots,\sigma-1\}$ ). The hypothesis $h_W$ says $W$ is a $*$ -decoder for $\mathrm{dec}$ :

$W^\dagger W=I$ and $WW^\dagger=I$ , so $W$ is unitary, which forces $2\sigma=2^n$ ;
$\mathrm{Tr}_2(W\rho W^\dagger)=\mathrm{dec}(\rho)$ for every $\rho$ , where $\mathrm{Tr}_2$ traces out the $\sigma$ -dimensional factor.

The remaining data. $\kappa$ is any location kind, and $F$ is ExRec fault data for $\kappa$ :

leading EC arrangements $F^{\text{lead}}_i$ , one per input block (none for prep);
a gadget arrangement $F^{\text{gad}}$ ;
trailing arrangements $F^{\text{trail}}_j$ , one per output block (none for meas).

$\tau$ is any truncation set of output blocks. The hypothesis $h_{\text{corr}}$ is that the ExRec is correct with truncation $\tau$ , meaning:

prep: $\mathrm{dec}(\Phi(\mathrm{Prep}_{F^{\text{gad}}}))=|0\rangle\langle0|$ , with $\Phi=\mathrm{id}$ if $0\in\tau$ and $\mathrm{EC}_{F^{\text{trail}}_0}$ otherwise.
meas: for both $\beta$ , $\mathrm{Meas}^\beta_{F^{\text{gad}}}\circ\mathrm{EC}_{F^{\text{lead}}_0}=\rho\mapsto\mathrm{dec}(\mathrm{EC}_{F^{\text{lead}}_0}\rho)_{\beta\beta}$ .
gate/wait:

\textstyle(\bigotimes\mathrm{dec})\circ\mathrm{Tr}_\tau\circ\mathrm{Gate}_{\kappa,F^{\text{gad}}}\circ\mathrm{Lead}=\mathcal U_\kappa\circ(\bigotimes\mathrm{dec})\circ\mathrm{Lead}.

The objects in these conditions are defined as follows.

$\mathrm{Lead}=\bigotimes_i\mathrm{EC}_{F^{\text{lead}}_i}$ . $\mathrm{EC}_f$ runs the EC gadget under the Pauli faults of $f$ , with ancillas in $|0\rangle$ ; it sums over measurement records and traces out the ancillas.
$\mathrm{Tr}_\tau=\bigotimes_j(\mathrm{id}\text{ if }j\in\tau\text{, else }\mathrm{EC}_{F^{\text{trail}}_j})$ .
$\mathrm{Gate}$ , $\mathrm{Prep}$ and $\mathrm{Meas}^\beta$ . These are the analogous gadget maps. $\mathrm{Meas}^\beta$ is the trace of the outcome weight over records decoding by $\mathrm{md}$ to $\beta$ .
$\mathcal U_\kappa$ . Conjugation by $H$ , $T=\mathrm{diag}(1,e^{i\pi/4})$ , CNOT (first wire is the control), or $I$ for wait.

Statement. The $*$ -ExRec is correct, i.e.:

prep: there is a density matrix $\tau_0$ on $\mathbb C^\sigma$ (PSD, trace 1) with

W\,\Phi(\mathrm{Prep}_{F^{\text{gad}}})\,W^\dagger=|0\rangle\langle0|\otimes\tau_0 .

meas: for both $\beta$ ,

\mathrm{Meas}^\beta_{F^{\text{gad}}}\circ\mathrm{EC}_{F^{\text{lead}}_0}=\rho\mapsto\big[\mathrm{Tr}_2(W\,\mathrm{EC}_{F^{\text{lead}}_0}(\rho)\,W^\dagger)\big]_{\beta\beta}.

gate/wait: there is a channel $V$ (finite Kraus form) on the $a_\kappa$ -fold product of $\sigma$ -dimensional systems such that

\textstyle(\bigotimes\mathcal W)\circ\mathrm{Tr}_\tau\circ\mathrm{Gate}_{\kappa,F^{\text{gad}}}\circ\mathrm{Lead}=\mathcal P_{U_\kappa,V}\circ(\bigotimes\mathcal W)\circ\mathrm{Lead}.

Here $\mathcal W(\rho)=W\rho W^\dagger$ on each block. $\mathcal P_{U,V}$ regroups the $a_\kappa$ pairs into (all bits, all $\sigma$ -parts), applies $\mathrm{id}\otimes V$ , conjugates by $U_\kappa\otimes I$ , and regroups back.

No bound on fault counts is assumed.

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