A good truncated ExRec is correct for ideal decoders and *-decoders

Open

QAlgorithms.GottesmanIntro.good_truncated_exRec_correct

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

gottesman-introlecture-notesquantum-information

This lemma extends Theorem 6 to the truncated extended rectangles that appear when bad rectangles are pushed through in level reduction.

Fix an $[[n,1,2t+1]]$ code with ideal decoder $\mathcal D$ and fault-tolerant gadgets satisfying Definitions 2–5, with Pauli faults. A truncated ExRec is an ExRec of type $\kappa$ from which the trailing EC steps on a nonempty set $T$ of output blocks have been removed (Definition 10). Only ExRecs with trailing ECs can be truncated: gate, wait and preparation ExRecs. It is good if the remaining locations contain at most $t$ faults:

s_{\mathrm{lead}} + s_{\mathrm{gadget}} + \sum_{j\notin T} s_{\mathrm{trail},j} \le t .

Then:

the truncated ExRec is correct for the ideal decoder, i.e. diagrams (72)/(73) hold with the removed trailing EC steps deleted;
for every *-decoder $W$ of $\mathcal D$ , the truncated ExRec is correct for $W$ (eq. (83) and its preparation version, with the removed trailing EC steps deleted).

Formalization Note The truncation set is a nonempty Finset of output blocks. For a measurement ExRec there are no output blocks, so the hypothesis cannot hold, matching the source.

Preamble

import Definitions.Def_QAlgorithms_Defs_FTCircuit
set_option autoImplicit false

Formal statement

namespace QAlgorithms.GottesmanIntro




/-- Gottesman intro p.38, Lemma 3: "A good truncated ExRec is correct for both ideal decoders and
*-decoders." Let `P` be a fault-tolerant protocol (Defs. 2–5). For every ExRec type `κ`, every
nonempty set `trunc` of output blocks whose trailing EC is removed (a truncated ExRec, Def. 10;
measurement ExRecs have no trailing EC, so for them the hypothesis is void), and every Pauli
fault arrangement `F` with at most `t` faults in the remaining locations (good, Def. 10), the
truncated ExRec is correct for the ideal decoder, and it is correct for every *-decoder `W` of
the ideal decoder. -/
theorem good_truncated_exRec_correct (P : FTProtocol) (hP : P.IsFaultTolerant) (κ : LocKind)
    (F : ExRecFaults κ) (trunc : Finset (Fin κ.trailCount)) (htrunc : trunc.Nonempty)
    (hgood : F.count P trunc ≤ P.t) :
    ExRecCorrect P κ F trunc ∧
      ∀ (σ : ℕ) (W : Matrix (Bool × Fin σ) (Qubits P.n) ℂ), IsStarDecoder P.dec W →
        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 3. https://arxiv.org/pdf/0904.2557v1

Read-back

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

The data.

$P$ . A protocol (code $\mathcal C\subseteq\mathbb C^{2^n}$ $C \subseteq C^{2^{n}}$ , encoder, decoder $\mathrm{dec}$ $dec$ , gadgets $G_\kappa$ $G_{κ}$ , EC circuit $G_{\mathrm{EC}}$ $G_{EC}$ , classical decoding $\mathrm{md}$ $md$ , parameter $t$ $t$ ) satisfying the full fault-tolerance condition. This condition comprises:
- a 2-dimensional code detecting all operators on $\le 2t$ qubits;
- an isometric encoding onto $\mathcal C$ ;
- a Kraus-channel decoder that perfectly decodes encoded states hit by operators in the span of weight- $\le t$ Paulis;
- well-formed gadgets with the expected live-qubit flows;
- the properties Meas, Prep A/B, Gate A/B and EC A/B, whenever fault counts plus filter levels are $\le t$ .
$\kappa$ . Any location kind.
$F$ . ExRec fault data: leading EC arrangements $F^{\text{lead}}_i$ (none for prep), a gadget arrangement $F^{\text{gad}}$ , and trailing EC arrangements $F^{\text{trail}}_j$ (none for meas).
$\tau$ . A nonempty set of output-block indices.
- For meas there are no output blocks, so this hypothesis cannot hold and the statement is vacuous for $\kappa=$ meas.
- For prep it forces $\tau=\{0\}$ .
Hypothesis $h_{\text{good}}$ .

\textstyle\sum_i\#_{\mathrm{EC}}(F^{\text{lead}}_i)+\#_{G_\kappa}(F^{\text{gad}})+\sum_{j\notin\tau}\#_{\mathrm{EC}}(F^{\text{trail}}_j)\le t,

where $\#_G(f)$ is the number of locations of $G$ at which $f$ places a Pauli pair.

Conclusion, part 1: the truncated ExRec is correct.

prep: $\mathrm{dec}(\mathrm{Prep}_{F^{\text{gad}}})=|0\rangle\langle0|$ . The trailing EC is omitted, since $0\in\tau$ .
gate/wait ( $H$ , $T$ , CNOT, wait):

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

Here:

$\mathrm{Tr}_\tau$ applies the identity on blocks $j\in\tau$ and $\mathrm{EC}_{F^{\text{trail}}_j}$ on the others;
the gadget maps run the gadget under the Pauli faults with ancillas in $|0\rangle$ , sum over measurement records, and trace out the ancillas;
$\mathcal U_\kappa$ is conjugation by $H$ , $T=\mathrm{diag}(1,e^{i\pi/4})$ , CNOT (first wire is the control), or $I$ .

Conclusion, part 2: the $*$ -version holds for every $*$ -decoder. Take every $\sigma\in\mathbb N$ and every $(2\sigma)\times2^n$ matrix $W$ with $W^\dagger W=I$ , $WW^\dagger=I$ and $\mathrm{Tr}_2(W\rho W^\dagger)=\mathrm{dec}(\rho)$ for all $\rho$ . Then:

prep: there is a density matrix $\tau_0$ on $\mathbb C^\sigma$ with $W\,\mathrm{Prep}_{F^{\text{gad}}}\,W^\dagger=|0\rangle\langle0|\otimes\tau_0$ .
gate/wait: there is a Kraus channel $V$ on the $\sigma$ -parts 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}$ applies $V$ to the joint $\sigma$ -parts and conjugates the joint bit-parts by $U_\kappa$ .

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