A fault-tolerant circuit with only good ExRecs has the ideal output distribution

Open

QAlgorithms.GottesmanIntro.output_eq_of_all_good

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

gottesman-introlecture-notesquantum-information

This theorem says that a fault-tolerant simulation is exact as long as no extended rectangle has too many faults.

Let $C$ be a quantum circuit of preparation, gate ( $H$ , $R_{\pi/8}$ , CNOT), measurement and wait locations, organized in time steps as in Definition 6: it takes no input, every qubit is first prepared and finally measured, and at each time step every live qubit is in exactly one location. Fix an $[[n,1,2t+1]]$ code with ideal decoder and fault-tolerant gadgets satisfying Definitions 2–5, all location gadgets having the same depth. Let $C'$ be the fault-tolerant circuit for $C$ : each location replaced by its gadget, with EC gadgets inserted between consecutive locations.

Let a Pauli fault arrangement be given on $C'$ such that every extended rectangle of $C'$ contains at most $t$ faulty locations. Write $p_{C'}$ for the distribution of the measurement record of the faulty $C'$ , decoded classically to one bit per measurement location of $C$ by the measurement gadgets' classical decoding, and $p_C$ for the output distribution of the ideal circuit $C$ . Then

p_{C'} = p_C .

This is the first form of the statement that fault tolerance protects a computation; Theorem 8 extends it to circuits with bad extended rectangles.

Formalization Note The fault-tolerant circuit is ftCircuit P C; its measurement record is pushed forward along ftDecode P C. The common gadget depth (HasUniformDepth) is the layer's modelling hypothesis that lets the gadgets of one time step of $C$ run in parallel without extra unprotected waiting locations.

Preamble

import Definitions.Def_QAlgorithms_Defs_FTCircuit
set_option autoImplicit false

Formal statement

namespace QAlgorithms.GottesmanIntro


/-- Gottesman intro p.36, Theorem 7: "Suppose a fault-tolerant circuit for `C` contains only
good extended rectangles. Then the output distribution of the fault-tolerant protocol is the same
as the output distribution of `C`." Let `P` be a fault-tolerant protocol (Defs. 2–5) whose
location gadgets have a common depth, and `C` a circuit of preparation, gate, measurement and
wait locations as in Def. 6 (no input, every qubit prepared first and measured last). Let `fa`
be a Pauli fault arrangement on the fault-tolerant circuit `C′ = ftCircuit P C` such that every
(full) ExRec of `C′` contains at most `t` faulty locations. Then the distribution of the
measurement record of the faulty `C′`, decoded classically by the measurement gadgets'
decoding (`ftDecode`), equals the output distribution of the ideal circuit `C`. -/
theorem output_eq_of_all_good (P : FTProtocol) (hP : P.IsFaultTolerant)
    (hdepth : P.HasUniformDepth) {N : ℕ} (C : LocCircuit N) (hC : C.IsIdealCircuit)
    (fa : PauliArrangement)
    (hgood : ∀ ℓ ∈ C.locs, (faultyLocs (ftCircuit P C) fa ∩ exRecLocs P C ℓ ∅).card ≤ P.t) :
    pushDist (ftDecode P C) ((ftCircuit P C).outDist (pauliErr (ftCircuit P C) fa) 1) =
      C.idealOutDist := by
  sorry



end QAlgorithms.GottesmanIntro

Source

Daniel Gottesman, An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation, 2009, v1, PDF p. 36, §5.2, Theorem 7. 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 fault-tolerant protocol: a code $\mathcal C\subseteq\mathbb C^{2^n}$ , an encoding $\mathrm{enc}$ , a decoder $\mathrm{dec}$ , gadgets $G_\kappa$ for the six location kinds (prep, $H$ , $T$ , CNOT, meas, wait), an EC circuit $G_{\mathrm{EC}}$ on $n+A$ qubits, a classical decoding $\mathrm{md}$ , and a parameter $t$ .

The hypothesis $h_P$ . It is the full fault-tolerance condition:

$\mathcal C$ is 2-dimensional and every operator supported on $\le 2t$ qubits is detectable on it.
$\mathrm{enc}$ is an isometry onto $\mathcal C$ .
$\mathrm{dec}$ is a Kraus channel that, for every $E$ in the span of weight- $\le t$ Pauli strings, maps $|E\,\mathrm{enc}\,\psi\rangle\langle E\,\mathrm{enc}\,\psi|$ to $\|E\,\mathrm{enc}\,\psi\|^2|\psi\rangle\langle\psi|$ .
The gadgets are well-formed with the expected live-qubit flows (prep: none→data; meas: data→none; gates, wait and EC: data→data).
The properties Meas, Prep A/B, Gate A/B and EC A/B hold, stated with the $r$ -filters $\mathcal F_r$ (compression onto the span of weight- $\le r$ Paulis applied to $\mathcal C$ ) and the gadget superoperators under Pauli fault arrangements. Each such property holds whenever the relevant fault count, plus filter levels, is $\le t$ . For example, Gate B reads

\textstyle(\bigotimes\mathrm{dec})\circ\mathrm{Gate}_{\kappa,f}\circ\bigotimes\mathcal F_{r_i}=\mathcal U_\kappa\circ(\bigotimes\mathrm{dec})\circ\bigotimes\mathcal F_{r_i},

and EC B reads $\mathrm{dec}\circ\mathrm{EC}_f\circ\mathcal F_r=\mathrm{dec}\circ\mathcal F_r$ .

The further hypotheses.

$h_{\text{depth}}$ . All six gadgets have the same number of time steps as the preparation gadget.
$h_C$ . $C$ is an ideal circuit on $N$ qubits. It is well-formed starting and ending with no live qubits: each step uses disjoint qubits and touches all live qubits; preparations act only on dead qubits and other locations only on live ones. Every location's classical condition is constantly true.
$f$ . An arbitrary Pauli fault arrangement on location ids of $C'$ . It places a conjugation by $P$ on the first wire and $Q$ on the other wire at each location where it gives $(P,Q)$ , after the ideal action, or before it for measurements.

The circuit $C'=\mathrm{ft}(P,C)$ . It acts on $N(n+A)$ qubits, and qubit $q$ of $C$ owns the block $\{(q,j): j<n+A\}$ .

Each step $s$ of $C$ becomes $D+D_{\mathrm{EC}}$ steps. Here $D$ is the maximum gadget depth and $D_{\mathrm{EC}}$ is the EC depth.
In the first $D$ steps, every location of step $s$ is replaced in parallel by its gadget on the blocks of its qubits.
In the next $D_{\mathrm{EC}}$ steps, $G_{\mathrm{EC}}$ is run on the block of every qubit touched at step $s$ by a non-measurement location.
Gadget conditions read outcomes through their global ids. The conditions of gate locations of $C$ are conjoined, evaluated on decoded logical outcomes.

ExRec locations. For a location $\ell$ (at step $s$ ) of $C$ , $\mathrm{ExRec}(\ell)$ is the set of locations of $C'$ belonging to:

the gadget instance of $\ell$ ;
the EC instance of step $s-1$ on a qubit of $\ell$ , provided $\ell$ is not a preparation;
the EC instance of step $s$ on a qubit of $\ell$ , provided $\ell$ is not a measurement.

Hypothesis $h_{\text{good}}$ . For every location $\ell$ of $C$ , at most $t$ locations of $C'$ in $\mathrm{ExRec}(\ell)$ are faulty under $f$ .

The output distributions.

$\mu_{C'}$ . The distribution of $C'$ on bit vectors $r'$ of length equal to the number of measurements in $C'$ . It is the real part of the trace of the classical–quantum state obtained by running $C'$ from $|0\cdots0\rangle\langle0\cdots0|$ , with a trivial 1-dimensional environment and the faults of $f$ , at measurement record $r'$ .
$\mathrm{dec}_{\mathrm{ft}}(r')$ . For each measurement location of $C$ , in record order, this applies $\mathrm{md}$ to the outcomes of $C'$ at that location's measurement-gadget measurements. Missing outcomes are read as $0$ .
$\mu_C$ . The ideal distribution of $C$ : the same construction with no errors and trivial environment.

Statement. For every $r$ (a bit vector indexed by the measurements of $C$ ):

\sum_{r'\,:\,\mathrm{dec}_{\mathrm{ft}}(r')=r}\mu_{C'}(r')=\mu_C(r).

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