Quantum Error Correction

Motivation

A quantum LDPC code is a CSS code whose two check matrices $H_X$ and $H_Z$ have rows and columns of bounded weight, so that every check measures only a few qubits. Such codes are the main candidates for fault-tolerant quantum memories, because their checks are local, but a code is only useful together with a decoder: an efficient procedure that recovers the error, up to stabilizers, from its syndrome. For classical LDPC codes built from expander graphs, Sipser and Spielman showed in 1996 that a simple bit-flipping algorithm corrects a constant fraction of the minimum distance in linear time (Sipser–Spielman 1996). In the quantum setting the obvious analogue fails, and before this work no family of quantum LDPC codes was known to admit an efficient decoder correcting a number of adversarial errors proportional to its minimum distance.

Timeline.

• 1996: Sipser and Spielman, expander codes and their linear-time bit-flipping decoder.
• 2009: Tillich and Zémor introduce the hypergraph product, giving quantum LDPC codes of positive rate and minimum distance of order $\sqrt n$ (arXiv:0903.0566).
• 2015: Leverrier, Tillich and Zémor take the hypergraph product of an expanding biregular graph with itself and prove that a greedy generator-flipping decoder corrects every error of weight up to a constant fraction of the minimum distance (arXiv:1504.00822, FOCS 2015). This mission formalizes that result.

Setting

Let $G = (A \cup B, \mathcal E)$ be a finite bipartite graph, $n_A = |A|$, $n_B = |B|$, with $n_B \le n_A$, and write $a \sim b$ for adjacency. $G$ is $(\Delta_A, \Delta_B)$-biregular if every vertex of $A$ has $\Delta_A$ neighbours and every vertex of $B$ has $\Delta_B$. For $S \subseteq A$ let $\Gamma(S)$ be its neighbourhood. $G$ is $(\gamma_A, \delta_A)$-left-expanding if $|\Gamma(S)| \ge (1 - \delta_A)\Delta_A |S|$ for every $S \subseteq A$ with $|S| \le \gamma_A n_A$; right expansion is the same on the $B$ side, and left-right expanding means both. $\Gamma_u(S)$ denotes the unique neighbours of $S$, adjacent to exactly one vertex of $S$.

Let $H$ be the $n_B \times n_A$ binary biadjacency matrix of $G$. The quantum code $\mathcal Q_G$ has $n = n_A^2 + n_B^2$ qubits, indexed by $A^2 \cup B^2$ (written $\alpha a$ and $b\beta$), and check matrices

$$H_X = (\mathbb 1_{n_A} \otimes H,\ H^T \otimes \mathbb 1_{n_B}), \qquad H_Z = (H \otimes \mathbb 1_{n_A},\ \mathbb 1_{n_B} \otimes H^T),$$

with rows indexed by $A \times B$ and $B \times A$. The row $ba$ of $H_Z$ has support the Z-generator $g_{ba} = \{\alpha a : \alpha \sim b\} \cup \{b\beta : \beta \sim a\}$. An $X$ error is $e \in \mathbb F_2^{A^2 \cup B^2}$, its syndrome is $\sigma_X(e) = H_X e^T$, and $\mathcal C_Z^\perp$ is the space of sums of Z-generators. The weight $w(e_X, e_Z)$ of a quantum error counts the qubits where $e_X$ or $e_Z$ is nonzero.

The decoder. On a syndrome $s$, one iteration picks a vector $e_1$ whose support lies in some generator $g_{ba}$, such that $s_1 = s + \sigma_X(e_1)$ has $|s_1| < |s|$ and the ratio $(|s| - |s_1|)/|e_1|$ is maximal among all such vectors. It iterates on the current syndrome, fails if it gets stuck at a nonzero syndrome, and otherwise outputs the sum $e_O$ of the flipped vectors. The $Z$ decoder is the same with $H_X$ and $H_Z$ exchanged.

Formalization targets

Goal: Theorem 2

Assume $G$ is $(\Delta_A, \Delta_B)$-biregular and $(\gamma_A, \delta_A, \gamma_B, \delta_B)$-left-right expanding with

$$\delta_A < \tfrac16, \qquad \delta_B < \tfrac16,$$

and let $(e_X, e_Z)$ be a quantum error with

$$w(e_X, e_Z) < w_0 = \frac{1}{3(1 + \Delta_B)} \min(\gamma_A n_A, \gamma_B n_B).$$

Then on every run, the $X$ decoder on input $\sigma_X(e_X)$ never outputs a failure and its output satisfies $e_O + e_X \in \mathcal C_Z^\perp$. The $Z$ decoder on $\sigma_Z(e_Z)$ behaves symmetrically, with $e_O + e_Z \in \mathcal C_X^\perp$.

Milestones

In the paper's order of proof:

• Lemma 3, $|\Gamma_u(S_A)| \ge (1 - 2\delta_A)\Delta_A |S_A|$;
• Proposition 4, distance at least $\gamma_A n_A$ for the classical code;
• the distance half of eq. (3), $d_Q \ge \min(d, d^T)$, already posed on the platform;
• Corollary 5, $d_Q \ge \min(\gamma_A n_A, \gamma_B n_B)$;
• the column-weight bound $|\sigma_X(e)| \le \Delta_B |e|$;
• Lemma 7, existence of a critical generator;
• the displays (19), (22), (23), (24) of Appendix B;
• Lemma 8, a step of ratio at least $1/3$ inside a critical generator;
• Lemma 10, the $X$ half of the goal.

Significance

The result. Theorem 2 gives the first family of quantum LDPC codes with an efficient decoder that corrects a number of adversarial errors proportional to the minimum distance. Here that number is of order $\sqrt n$. The same analysis yields a robustness property: low-weight errors have syndromes of proportional weight (Corollary 9 of the paper). Later work on quantum expander codes builds on this analysis, for example on their decoding under random noise (arXiv:1711.08351) and on fault tolerance with constant overhead (arXiv:1808.03821).

Formalizing it. The result is proved on paper. As far as is known, it has no machine-checked proof. The mission produces a formal statement of the decoder and its correctness, and it also produces reusable pieces:

• unique-neighbour expansion;
• the distance of expander codes;
• the distance of hypergraph product codes, tied to an open item of the Tillich–Zémor mission;
• a generic formalization of greedy syndrome-weight decoding.

Difficulty

The obvious quantum analogue of Sipser–Spielman flips single qubits that lower the syndrome weight. It fails because of degeneracy: an error and its sum with a generator have the same syndrome. A small error can therefore look locally like a large one, and no single qubit need be worth flipping. The paper's decoder instead flips arbitrary patterns inside one generator. The difficulty is to show that some pattern always lowers the syndrome weight by a constant fraction of its size. The proof needs a combinatorial structure, the critical generator, whose existence uses unique-neighbour expansion on both sides of the graph, and a case analysis on its six parts. A second difficulty is that the decoder minimizes the syndrome weight, not the error weight, so the intermediate error can grow. Bounding that growth is what limits the guarantee to $w_0$ rather than the distance.

Formalization scope

• The graph is a relation adj : A → B → Prop on finite types, and $H$ = bipMatrix adj : Matrix B A (ZMod 2).
• The published TillichZemor.HGP.Setting is reused. The paper's $H_X$ is TillichZemor.HGP.hz H H and its $H_Z$ is hx H H; the X/Z names are swapped relative to the 2009 paper, and this is checked against eq. (5) in a sanity file.
• Qubits are (A × A) ⊕ (B × B), weights are hammingNorm, and $\mathcal C_Z^\perp$ is CodingTheory.dualCode of ker H_Z.
• Expansion constants are real and cardinalities are compared in $\mathbb R$. Distance statements are per-vector, so no $\infty$-valued minimum distance is cast to a real number.
• The decoder is defined once (Candidate, Step, Reach, DecodesCorrectly), generic in the syndrome and generator matrices. Its ratio is computed in $\mathbb Q$.
• Reach contains every state reachable under any tie-breaking. Correctness requires, at every reachable state, a further step while the syndrome is nonzero, and $e_O + e$ in the row space of the generator matrix once it is zero. Termination is automatic, because each step lowers a natural number.

Additions and omissions.

• The hypothesis $\Delta_A \ge 1$ is added throughout. With $\Delta_A = 0$ the expansion conditions are vacuous, $H = 0$, and every error is invisible.
• In Lemma 8 the vector $e_1$ is required to be nonzero. With $e_1 = 0$ the printed inequality reads $0 \ge 0$.
• Lemma 8 is posed in its first assertion only. The critical generator is taken with respect to a minimum-weight representative of the coset, as in Appendix B.
• The clauses "runs in time linear in the code length" and "letting $\Delta_A$, $\Delta_B$ be fixed and allowing $n_A, n_B$ to grow" are not formalized. The goal holds for every finite graph meeting the hypotheses.

Trivializing formalizations ruled out. The goal names the paper's own decoder, not "there exists a decoder", which a brute-force coset decoder would satisfy. It quantifies over every run, not a single favourable one. It asserts both never-failing and correctness, not partial correctness alone. It uses $H_X$ = hz H H, not the swapped matrix.

Welcome contributions. Proofs of the counting milestones (Lemma 3, Proposition 4, the column-weight bound, (19), (22)–(24)) are independent of one another. The distance bound of Tillich–Zémor, open on the platform, is the deepest dependency. Unique-neighbour expansion and the hypergraph-product distance bound are useful beyond this mission.

Selected references

• A. Leverrier, J.-P. Tillich, G. Zémor, Quantum expander codes, FOCS 2015; arXiv:1504.00822v1 (2015). https://arxiv.org/abs/1504.00822
• J.-P. Tillich, G. Zémor, Quantum LDPC codes with positive rate and minimum distance proportional to the square root of the blocklength, IEEE Trans. Inf. Theory 60(2), 2014; arXiv:0903.0566. https://arxiv.org/abs/0903.0566
• M. Sipser, D. A. Spielman, Expander codes, IEEE Trans. Inf. Theory 42(6), 1996. https://doi.org/10.1109/18.556667
• O. Fawzi, A. Grospellier, A. Leverrier, Efficient decoding of random errors for quantum expander codes, STOC 2018; arXiv:1711.08351. https://arxiv.org/abs/1711.08351
• O. Fawzi, A. Grospellier, A. Leverrier, Constant overhead quantum fault-tolerance with quantum expander codes, FOCS 2018; arXiv:1808.03821. https://arxiv.org/abs/1808.03821

Motivation

Quantum error correction needs families of codes that protect a growing number of logical qubits while using checks that touch few physical qubits. In a quantum Tanner code, the local constraints come from two smaller binary codes. The distance analysis requires those local codes to satisfy a geometric condition called robustness: a low-weight word in a certain sum code must occupy only a controlled number of complete rows and columns. The deterministic distance theorem in Leverrier and Zémor's Quantum Tanner codes assumes this condition; their Theorem 9 supplies it for randomly chosen component codes. Establishing that random codes satisfy the assumption makes the later existence result meaningful rather than conditional on a property with no known examples.

The appendix follows the approach of Panteleev and Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, with a separate treatment of puncturing. The historical relation here is limited: this mission formalizes Leverrier and Zémor's Theorem 9 and its own numbered supporting results, with their hypotheses and constants.

Setting

Fix two coordinate sets $A$ and $B$, each of cardinality $\Delta$. A binary linear code $C_A\subseteq\mathbb F_2^A$ is a vector subspace; similarly $C_B\subseteq\mathbb F_2^B$. Regard a word on $A\times B$ as a matrix $x=(x_{ab})$. The column code contains matrices whose column at every $b\in B$ belongs to $C_A$. The row code contains matrices whose row at every $a\in A$ belongs to $C_B$. Their intersection is the tensor code $C_A\otimes C_B$; their sum is the dual tensor code $C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B$. The Hamming weight $|x|$ counts its nonzero entries. These conventions are those of §3.5 of the source paper.

Write $d_A,d_B$ for the actual minimum distances of the two component codes. The dual tensor code is $w$-robust if every codeword $x$ with $|x|\le w$ vanishes outside the union of some set of at most $|x|/d_B$ rows and some set of at most $|x|/d_A$ columns. Thus a low-weight word cannot be spread thinly across many rows and columns. For retained coordinate sets $A'\subseteq A$ and $B'\subseteq B$, the punctured codes $C_{A'}$ and $C_{B'}$ are the images under restriction. Robustness has $p$-resistance to puncturing when the corresponding dual tensor code remains $w$-robust for every pair $A',B'$ of equal size obtained by removing at most $p$ coordinates from each side. These are Definitions 5 and 8 on pp. 15–16 of the paper.

A uniform generator matrix with $r$ rows and $\Delta$ columns is sampled uniformly from all binary matrices of that shape. Its row span is $C_A$. Independently, a uniform parity-check matrix with $s$ rows and $\Delta$ columns defines $C_B$ as its kernel. Probability is the fraction of matrices, or matrix pairs, satisfying an event. In the asymptotic statement, $\Delta$ tends through natural numbers to infinity.

Formalization targets

Random robustness and resistance

For $0<\rho_A,\rho_B<1$, $0<\varepsilon<1/2$, and $1/2+\varepsilon<\gamma<1$, sample $C_A$ and $C_B$ from the matrix models above, using $\lfloor\rho_A\Delta\rfloor$ generator rows and $\lceil(1-\rho_B)\Delta\rceil$ parity-check rows. The goal, Theorem 9, is

$$\Pr\!\left[C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B\text{ is }\Delta^{3/2-\varepsilon}\text{-robust with }\Delta^\gamma\text{-resistance}\right]\longrightarrow 1.$$

The milestones are the paper's numbered appendix statements: Lemma 31 converts concentration on few rows and columns into Definition 5's sharper weight-based bounds; Lemmas 24–29 address ranks and probabilities for random kernels and punctured kernels; Theorem 30 gives the quantitative high-probability alternative used before the final limit. The goal fixes the exponents and quantifies over the whole uniform matrix experiment.

Significance

Theorem 9 certifies that the robustness hypothesis needed by the paper's distance construction occurs with asymptotic probability one. It covers all allowed puncturings at once, which matters because a later distance argument deletes coordinates selected by the codeword under study. A statement about one fixed puncturing would not provide that guarantee. The result is proved in the 2022 paper; this mission poses its statements for machine-checked proofs and does not claim that those proofs already exist.

Formalizing the result produces reusable finite probability statements for random linear codes, a parity-check treatment of puncturing, and rank bounds for sparse binary matrices. Those ingredients are independent of the group complex used in the paper's other mission. They can support later formalizations of random coding arguments where a union over many coordinate restrictions is necessary.

Difficulty

The evident first check is that one fixed low-weight matrix probably does not belong to a random dual tensor code. That alone does not establish robustness: the statement ranges over all such matrices and, for resistance, over every pair of large retained coordinate sets. The paper's intermediate results control this whole collection using rank information about sparse matrices and the exact probability that independent vectors lie in a random kernel. A further issue is that puncturing a parity-check code does not simply delete columns from its defining matrix; the discarded columns contribute a random subspace. The quantitative event in Theorem 30 and the simultaneous limit in Theorem 9 both have to survive these ranges.

Formalization scope

Lean uses ZMod 2 for $\mathbb F_2$, Fin \Delta for each coordinate set, and functions on $A\times B$ for matrices. Rows are indexed by $A$ and belong to $C_B$; columns are indexed by $B$ and belong to $C_A$. The published TillichZemor.HGP.Setting supplies the parity-check kernel and the extended-natural minimum distance, whose value is infinity for the zero code. CodingTheory is a published prerequisite. Local definitions give the row and column codes, their sum, puncturing, robustness, uniform finite probability, generator row span, and binary entropy in bits.

The printed matrix sizes $\rho_A\Delta$ and $(1-\rho_B)\Delta$ need integer values. The chosen floor and ceiling keep their respective dimensions within the bounds used in the appendix. Every logarithm in the formalized appendix bounds means $\log_2$, including occurrences printed simply as $\log$. Theorem 30 includes an explicit sufficiently-large-$\Delta$ threshold, as its proof's asymptotic count requires, and carries the appendix's preceding entropy condition $\delta<h^{-1}(1-\rho)$ as $\delta<1/2$ and $h_2(\delta)<1-\rho$. Lemmas 25, 26, and 29 use the preceding condition $d>2\alpha\Delta$; the symbol beside $\Delta$ in the scan is ambiguous, and the argument on p. 29 determines this reading. These choices are recorded for audit in MODERATION_NOTES.md.

The probability space is all matrices of each stated size, with the two matrices in Theorem 9 sampled independently. There is no conditioning on a favorable code or an assumed version of Theorem 30 in the goal. The mission does not formalize the later quantum Tanner code construction or the cited Gilbert–Varshamov result as an additional item. Contributions proving the goal, the numbered milestones, or reusable rank and finite-probability facts are within scope.

Selected references

• Anthony Leverrier and Gilles Zémor, Quantum Tanner codes, arXiv:2202.13641v3, 2022. Preprint.
• Pavel Panteleev and Gleb Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, arXiv:2111.03654, 2021. Preprint.

Why quantum Tanner codes matter

An error-correcting code protects information by adding redundancy. A quantum code must also account for two kinds of errors, commonly called $X$ and $Z$ errors. Quantum low-density parity-check codes use checks that each touch only a bounded number of qubits, while each qubit participates in only a bounded number of checks. Such locality matters when the number of qubits grows. For years it was difficult to make both the number of encoded qubits and the minimum distance proportional to the block length while retaining bounded-weight checks. Leverrier and Zémor's quantum Tanner construction gives a route through local codes placed on an expanding square complex; its main distance theorem is the target of this mission Leverrier and Zémor, 2022.

The construction combines two earlier ingredients. Left-right Cayley complexes provide the squares and expansion properties used by the code Dinur, Evra, Livne, Lubotzky, and Mozes, 2021. Robustness of a dual tensor code, including after puncturing coordinates, controls local words Panteleev and Kalachev, 2021. The paper states the local reduction property as Theorem 1 and derives the rate and distance bounds as Theorem 17. This mission formalizes that implication under the paper's stated component-code and expansion conditions; the separate random-code result that supplies robust examples belongs to the second mission of this series.

The square complex and its codes

Let $G$ be a finite group and let $A,B\subseteq G$ be inverse-closed sets, each of size $\Delta$. The total no-conjugacy condition says $ag\ne gb$ for every $a\in A$, $b\in B$, and $g\in G$. Vertices are two copies of the group, $V=G\times\{0,1\}$. A square associated with $v=(g,i)$ and $(a,b)\in A\times B$ has vertices $v$, $(ag,1-i)$, $(gb,1-i)$, and $(agb,i)$. The set of squares is $Q$, and a binary word on $Q$ has length $n=|Q|$. At a vertex $v$, the incident squares are indexed by $A\times B$; this indexing makes the local view $x_v$ of a word $x\in\mathbb F_2^Q$ an $A\times B$ matrix Leverrier and Zémor, §§3.2 and 4.1.

A binary linear code $C_A$ has coordinates indexed by $A$, and $C_B$ has coordinates indexed by $B$. Their tensor code $C_A\otimes C_B$ consists of matrices whose columns lie in $C_A$ and whose rows lie in $C_B$. The dual tensor code $C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B$ is the sum of the column and row codes. In Definition 5, it is $w$-robust when every member of weight at most $w$ is supported on a union of few rows and columns, with the bounds determined by the two component minimum distances. Definition 8 requires this property after deleting up to $p$ coordinates from each side. These are conditions on all relevant codewords and all permitted puncturings, including the unpunctured pair Leverrier and Zémor, pp. 15–16.

The two Tanner codes are $\mathcal C_0=T(\mathcal G^\square_0,(C_A\otimes C_B)^\perp)$ and $\mathcal C_1=T(\mathcal G^\square_1,(C_A^\perp\otimes C_B^\perp)^\perp)$. Here $\mathcal G^\square_i$ is the square-adjacency graph on the vertices in copy $i$. Together they define the quantum CSS code $\mathcal Q=(\mathcal C_0,\mathcal C_1)$. Its dimension counts encoded qubits. Its distance is the smaller of the minimum weights in $\mathcal C_0\setminus\mathcal C_1^\perp$ and $\mathcal C_1\setminus\mathcal C_0^\perp$ Leverrier and Zémor, pp. 14, 18.

Formalization targets

The goal is Theorem 17. Fix $0<\rho<1/2$, $0<\varepsilon<1/2$, $1/2+\varepsilon<\gamma<1$, and $\delta>0$. For sufficiently large $\Delta$, take a left-right Cayley complex satisfying total no-conjugacy and the paper's Ramanujan conditions. Require $0<\dim C_A\le\rho\Delta$, $\dim C_B=\Delta-\dim C_A$, minimum distance at least $\delta\Delta$ for $C_A,C_B$ and both duals, and $\Delta^{3/2-\varepsilon/2}$ robustness with $\Delta^\gamma$ resistance to puncturing for both relevant dual tensor codes. The target is

$$k\ge (1-2\rho)^2 n,\qquad d\ge \frac{\delta n}{4\Delta^{3/2+\varepsilon}}.$$

The milestones mirror the paper's route to this result. Lemma 4 bounds the nontrivial eigenvalues of the union and square graphs. Propositions 6 and 7 turn dual-tensor robustness into a decomposition and a $3/2$ closeness bound. Theorem 1 supplies a weight-reducing local codeword for every sufficiently light nonzero Tanner-code word. Display (5) supplies the dimension lower bound. Theorem 17 combines the two distance directions with that rate estimate Leverrier and Zémor, pp. 12, 15–16, 18–23.

What the result supplies

The lower bound on $k$ ensures a positive fraction of qubits can carry logical information when $\rho<1/2$. The lower bound on $d$ rules out small undetectable logical errors. For a fixed allowable degree $\Delta$, both bounds scale linearly with $n$. The paper also shows that random component codes can satisfy the robustness assumptions; that probabilistic result is a separate formalization target Leverrier and Zémor, Theorems 9 and 17.

A checked development would make explicit how the square indexing, duals, punctured codes, and CSS quotient fit together. The source proves the mathematical result; the statements here remain open Lean theorems. Reusable contributions include the tensor-code interface, spectral bounds for the graph construction, and lemmas connecting local views to the global Tanner codes. A proof of the existence of infinite Ramanujan complex families is outside this mission's stated target.

Where the proof is difficult

A light global codeword need not have a local view that is itself close to a tensor-code word. Some square-graph vertices have unusually large local weight, and puncturing is needed to isolate coordinates shared with those exceptional vertices. The paper's small-set expansion estimates and robustness conditions control those interactions. Simply averaging local weights does not yield the weight-reducing local codeword asserted by Theorem 1 Leverrier and Zémor, §4.2.

Formalization scope

Words are functions into ZMod 2, codes are submodules, and a matrix is a function on $A\times B$ with $A$ indexing rows. The square coordinates are four-element vertex sets. The construction uses $V=G\times\operatorname{Fin}(2)$ and counts $n$ as the number of squares rather than building $n=\Delta^2|G|/2$ into a definition. The minimum distance of the zero code is infinity, and robustness uses inequalities involving that extended value. Powers of $\Delta$ and the parameters $w,p$ are real; the paper uses integer $w,p$ in Definition 8, while the theorem's power thresholds need real comparisons. The formal robustness predicate includes Definition 5's range $0\le w\le\Delta^2$; the theorem thresholds satisfy it for sufficiently large $\Delta$. These conventions are recorded with each item.

The goal quantifies over every finite complex satisfying inverse closure, total no-conjugacy, and Ramanujan conditions, with a uniform threshold $\Delta_0$ chosen before the group and codes. This pins the complexes in the cited infinite family without formalizing their existence. In particular, the goal contains no auxiliary set or local reduction assumption that could make the distance bound immediate. The published CodingTheory and TillichZemor.HGP.Setting definitions supply dual codes and CSS dimension; the paper-specific setting supplies the square complex, local views, Tanner codes, and robustness. Contributions that keep these conventions and close any milestone theorem are welcome.

Selected references

• A. Leverrier and G. Zémor, Quantum Tanner codes, arXiv preprint, 2022. arXiv:2202.13641v3.
• I. Dinur, S. Evra, R. Livne, A. Lubotzky, and S. Mozes, Locally Testable Codes with constant rate, distance, and locality, arXiv preprint, 2021. arXiv:2111.04808.
• P. Panteleev and G. Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, arXiv preprint, 2021. arXiv:2111.03654.

Motivation

Quantum error correction and quantum communication both ask the same question: after a known noise process $\mathcal A$ has acted on a quantum system, how well can its effect be undone? For a given noise model the best recovery is the solution of a semidefinite program, which gives a number but no structure and no formula. Barnum and Knill showed in 2000 that a single, explicit recovery map, built from $\mathcal A$ and the input state alone, is always close to the best one: its fidelity is at least the square of the optimal fidelity (arXiv:quant-ph/0004088). The map they use is now usually called the Petz recovery map or transpose channel; Petz had introduced it in operator-algebraic work on sufficiency (Petz 1986; Petz 1988). Near-optimality results of this kind underlie approximate quantum error correction and the later theory of recoverability in quantum information.

Timeline.

• 1986–1988, D. Petz: the map $\rho^{1/2}\mathcal A^\dagger(\mathcal A(\rho)^{-1/2}\,\cdot\,\mathcal A(\rho)^{-1/2})\rho^{1/2}$ characterizes when a channel can be reversed exactly on a family of states.
• 2002, Barnum and Knill (J. Math. Phys. 43, 2097; doi:10.1063/1.1459754): in the published version, the reversal operation achieves at least the square of the optimal entanglement fidelity for a single input state.
• arXiv v2 of the same paper (the source of this mission): the published Eq. (34) had dropped the ensemble weights; with that corrected, the bound holds for the average entanglement fidelity of any ensemble of commuting density matrices (Acknowledgments, p. 14).

Setting

A finite-dimensional quantum system is described by complex $n\times n$ matrices; $X^\dagger$ is the conjugate transpose, and a density matrix is a positive semidefinite matrix of trace one. A completely positive map $\mathcal A$ is given by a finite decomposition $\mathcal A\sim\{A_i\}_i$ of matrices and acts by

$$\mathcal A(X)=\sum_iA_iXA_i^\dagger .$$

It is trace-preserving if $\sum_iA_i^\dagger A_i=I$ and trace-nonincreasing if $\sum_iA_i^\dagger A_i\le I$ in the Loewner order. The composite $\mathcal R\mathcal A$ has decomposition $\{R_kA_i\}_{(k,i)}$.

For a state $\rho$ the paper defines the reversal operation

$$\mathcal R_{\mathcal A,\rho}\sim\{\rho^{1/2}A_i^\dagger\,\mathcal A(\rho)^{-1/2}\}_i,$$

under the standing assumption that $\mathcal A(\rho)$ has full support. Here $X^{-1/2}$ is the generalized inverse square root: invert the square roots of the non-zero eigenvalues and keep the zero eigenvalues.

Fidelities are measured by the entanglement fidelity $F_e(\rho,\mathcal K)=\sum_k|\operatorname{tr}K_k\rho|^2$ of a map $\mathcal K\sim\{K_k\}_k$ and, for an ensemble $E=\{p_l,\rho_l\}_l$ (weights $p_l\ge0$ summing to one, density matrices $\rho_l$), by the average entanglement fidelity

$$\bar F_e(E,\mathcal K)=\sum_lp_lF_e(\rho_l,\mathcal K).$$

When $\rho=\sum_ip_i|i\rangle\langle i|$ in an orthonormal eigenbasis, the classical fidelity is $F_{\mathrm{cl}}(\rho,\mathcal K)=\sum_ip_i\langle i|\mathcal K(|i\rangle\langle i|)|i\rangle$, the average entanglement fidelity of the ensemble of eigenstates.

Formalization targets

Goal: Theorem 3 (p. 7)

Let $\mathcal A$ be trace-preserving, $E=\{p_l,\rho_l\}_l$ an ensemble of pairwise commuting density matrices, $\rho=\sum_lp_l\rho_l$, and assume $\mathcal A(\rho)$ has full support. Then for every trace-preserving completely positive $\mathcal R$,

$$\bar F_e(E,\mathcal R_{\mathcal A,\rho}\mathcal A)\;\ge\;\bar F_e(E,\mathcal R\mathcal A)^2 .$$

Milestones

The milestones follow the paper's proof:

1. Lemma 1 (p. 7): $\mathcal R_{\mathcal A,\rho}$ depends only on the map $\mathcal A$, not on its decomposition.
2. (14)–(15) (p. 7): after replacing $R_k$ by $P_CR_k$ ($P_C$ the support projector of $\rho$), which leaves $\bar F_e$ unchanged and makes $\mathcal R$ trace-nonincreasing, each $R_k=\rho^{1/2}B_k^\dagger\mathcal A(\rho)^{-1/2}$, and $\mathcal B(\rho)\le\mathcal A(\rho)$.
3. (28)–(32) (p. 9): $\sum_lp_l\sum_i|\operatorname{tr}\rho_lR^l_iB^l_i|^2\le\sum_lp_l\sum_{i,j}\operatorname{tr}R^l_iB^l_j\rho_lB_j^{l\dagger}R_i^{l\dagger}$.
4. (33)–(34) (p. 9): that sum equals $\operatorname{tr}\mathcal R(\mathcal B(\rho))\le\operatorname{tr}\mathcal R(\mathcal A(\rho))\le1$.

Two companions are also posed: Proposition 2, $\mathcal R_{\mathcal A,\rho}(\mathcal A(\rho))=\rho$, and Corollary 4, $F_{\mathrm{cl}}(\rho,\mathcal R\mathcal A)\le\sqrt{F_{\mathrm{cl}}(\rho,\mathcal R_{\mathcal A,\rho}\mathcal A)}$ and $F_e(\rho,\mathcal R\mathcal A)\le\sqrt{F_e(\rho,\mathcal R_{\mathcal A,\rho}\mathcal A)}$.

Significance

The result. Theorem 3 says that the error $1-\bar F_e$ of the reversal operation is at most twice the optimal error, since $(1-\eta)^2\ge1-2\eta$. It gives a closed-form recovery whose performance is within a factor two in error of the semidefinite optimum, for every noise process and every commuting ensemble. Taking the ensemble of eigenstates of $\rho$ (Corollary 4) gives the same guarantee for classical information sent through a quantum channel; the companion mission (II of this series) applies the construction to state discrimination, where the reversal operation is the pretty good measurement.

Formalizing it. The result is proved on paper; none of it has a machine-checked proof that we know of. The mission asks for the full argument: the decomposition independence of the reversal map, the reduction to the support of $\rho$, the singular-value change of decomposition (17)–(18), the chain (19)–(26) of Cauchy–Schwarz inequalities, and the normalization (27)–(34). It also fixes in Lean the arXiv v2 statement (commuting ensembles), which is stronger than the published one.

Difficulty

The obvious approach is to compare $\mathcal R_{\mathcal A,\rho}$ with an optimal $\mathcal R$ term by term. That fails: the fidelity of $\mathcal R\mathcal A$ is a sum of squared traces mixing the decompositions of $\mathcal R$ and $\mathcal A$, and no termwise inequality relates it to the fidelity of $\mathcal R_{\mathcal A,\rho}\mathcal A$. The paper first rewrites every recovery in the shape of the reversal map, then chooses, for each ensemble member separately, new decompositions of $\mathcal A$ and $\mathcal B$ that diagonalize a coefficient matrix; making that choice legitimate needs the unitary freedom of Kraus decompositions, which Mathlib does not have. The commutation $[\rho,\rho_l]=0$ is used to move fractional powers of $\rho$ and $\rho_l$ past each other inside traces; without commutation the authors do not know whether the theorem holds (p. 10).

Formalization scope

• Matrices are Matrix n n ℂ over a finite type n with decidable equality; Loewner order, square roots and functional calculus come from Mathlib (open scoped MatrixOrder). The map $X\mapsto\sum_iA_iXA_i^\dagger$ is the published PeresTerno.krausUpdate, referenced, not redefined.
• Maps are unbundled Kraus families over arbitrary finite index types. The recovery $\mathcal R$ in Theorem 3 ranges over every finite family with $\sum_kR_k^\dagger R_k=I$.
• $X^{-1/2}$ is cfc (fun x => (Real.sqrt x)⁻¹) X, the generalized inverse; Mathlib's junk matrix inverse is not used. The support projector is the functional calculus of the indicator of $x\ne0$.
• $F_e$ is defined by the formula (8), which the paper derives from its purification definition. $F_{\mathrm{cl}}$ takes an orthonormal eigenbasis and weights as data, with $\rho=\sum_ip_i|i\rangle\langle i|$ as a hypothesis.
• Standing hypotheses, all from the paper: $\mathcal A$ trace-preserving (§II's noise model); $\mathcal A(\rho)$ positive definite (full support, p. 7); the ensemble is a probability vector of pairwise commuting density matrices with $\rho=\sum_lp_l\rho_l$.
• In (34) the page prints $\operatorname{tr}\mathcal R(\mathcal A(\rho))=1$; after the replacement $R_k\mapsto P_CR_k$ the map is only trace-nonincreasing, so the milestone states $\le1$.
• Trivializing encodings are ruled out: the reversal family is the literal formula (12) for the given $\mathcal A$ and the ensemble's own $\rho$, and the fidelity of a composite map is (8) applied to the composite decomposition $\{R_kA_i\}$, never the right-hand side of the proof's chain.
• Infrastructure a complete development needs, reusable beyond this mission: the unitary freedom of Kraus decompositions, the singular value decomposition of a complex square matrix, the trace Cauchy–Schwarz inequality for Hilbert–Schmidt products, and functional-calculus identities such as $\rho^{1/2}\rho^{-1/2}=P_C$. Contributions of any of these as separate theorems are welcome. The pure-state, measurement form $P_{\mathrm{opt}}^2\le P_{\mathrm{PGM}}\le P_{\mathrm{opt}}$ is already posed on the platform as QAlgorithms.Arunachalam.barnumKnill and is not repeated here.

Selected references

• H. Barnum, E. Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, arXiv:quant-ph/0004088v2. https://arxiv.org/abs/quant-ph/0004088
• H. Barnum, E. Knill, same title, J. Math. Phys. 43, 2097 (2002). https://doi.org/10.1063/1.1459754
• D. Petz, Sufficient subalgebras and the relative entropy of states of a von Neumann algebra, Commun. Math. Phys. 105, 123–131 (1986). https://doi.org/10.1007/BF01212345
• D. Petz, Sufficiency of channels over von Neumann algebras, Quart. J. Math. 39, 97–108 (1988). https://doi.org/10.1093/qmath/39.1.97
• B. Schumacher, Sending entanglement through noisy quantum channels, Phys. Rev. A 54, 2614 (1996). https://doi.org/10.1103/PhysRevA.54.2614
• R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press (1985), §7.3. https://doi.org/10.1017/CBO9780511810817

Motivation

Quantum computers need error correction, and the codes that are cheapest to run in hardware are quantum low-density parity-check (LDPC) codes: every check involves a bounded number of qubits, and every qubit takes part in a bounded number of checks. For a long time the only well-understood quantum LDPC codes were surface codes such as Kitaev's toric code, whose minimum distance grows like the square root of the length but which encode a fixed number of qubits, so their rate tends to zero. Tillich and Zémor (arXiv:0903.0566; IEEE Transactions on Information Theory, 2014; preliminary version ISIT 2009) gave the first general construction of quantum LDPC codes with positive rate and minimum distance proportional to $\sqrt N$, from any classical LDPC code. Their hypergraph product became the standard building block of the field.

Timeline.

• 1996: Calderbank–Shor and Steane introduce CSS codes, quantum codes built from two classical binary codes (quant-ph/9512032, quant-ph/9601029).
• 1997: Kitaev's toric code: LDPC, distance $\Theta(\sqrt N)$, dimension 2 (quant-ph/9707021).
• 2009: Tillich and Zémor: the hypergraph product, with positive rate and distance $\Theta(\sqrt N)$ (this mission).
• 2020–2021: distance beyond $\sqrt N$ for quantum LDPC codes: $\sqrt N\log N$ by Evra, Kaufman and Zémor (arXiv:2004.07935); $N^{3/5}$ up to polylogarithmic factors by Hastings, Haah and O'Donnell (arXiv:2009.03921).
• 2022: Panteleev and Kalachev construct asymptotically good quantum LDPC codes, using lifted products that generalize the hypergraph product (arXiv:2111.03654).

Setting

All codes are binary linear codes, subspaces of $\mathbb F_2^{\iota}$ for a finite coordinate set $\iota$. The Hamming weight $|x|$ of $x$ is its number of nonzero coordinates. The minimum distance $d(\mathcal C)$ of a code is the least weight of a nonzero codeword, with the convention $d(\{0\})=\infty$.

A Tanner graph $\mathcal G=\mathcal T(V,C,E)$ is the bipartite graph of a parity-check matrix $H\in\mathbb F_2^{C\times V}$: the variable nodes $V$ index the columns, the check nodes $C$ index the rows, and $c\sim v$ iff $H_{cv}=1$. Its code is $\mathcal C=\ker H$. The transpose Tanner graph $\mathcal G^T$ is that of $H^T$, and its code $\mathcal C^T=\ker H^T$ is the transpose code. It depends on the matrix $H$, not only on $\mathcal C$.

A CSS code is a pair $(\mathcal C_X,\mathcal C_Z)$ of codes of the same length $N$ with $\mathcal C_Z^\perp\subseteq\mathcal C_X$. Its quantum dimension and quantum minimum distance are

$$k_Q=\dim(\mathcal C_X/\mathcal C_Z^\perp),\qquad d_Q=\min(d_X,d_Z),\quad d_X=\min\{|x|:x\in\mathcal C_X\setminus\mathcal C_Z^\perp\},$$

with $d_Z$ defined symmetrically and $\min\emptyset=\infty$.

Given $H_1\in\mathbb F_2^{C_1\times V_1}$ and $H_2\in\mathbb F_2^{C_2\times V_2}$ with Tanner graphs $\mathcal G_1,\mathcal G_2$, the code $\mathcal Q(\mathcal G_1\times\mathcal G_2)$ has qubits $(V_1\times V_2)\sqcup(C_1\times C_2)$ and check matrices

$$H_X=\big(H_1\otimes I_{V_2}\ \big|\ I_{C_1}\otimes H_2^T\big),\qquad H_Z=\big(I_{V_1}\otimes H_2\ \big|\ H_1^T\otimes I_{C_2}\big),$$

with $\mathcal C_X=\ker H_X$ and $\mathcal C_Z=\ker H_Z$. Write $k_i=\dim\mathcal C_i$, $k_i^T=\dim\mathcal C_i^T$, $d_i=d(\mathcal C_i)$ and $d_i^T=d(\mathcal C_i^T)$.

Formalization targets

Goal: Theorem 1 (p. 3)

Let $H$ be a full-rank $(n-k)\times n$ parity-check matrix of an $[n,k,d]$ code. The code $\mathcal Q(\mathcal G\times\mathcal G)$ built from two copies of its Tanner graph is a CSS code with

$$N=n^2+(n-k)^2,\qquad k_Q=k^2,\qquad d_Q=d,$$

and each row of $H_X$ and $H_Z$ has weight $i+j$, with $i$ a row weight and $j$ a column weight of $H$.

General results

• Proposition 14 (dimension): $k_Q=k_1k_2+k_1^Tk_2^T$ for any two Tanner graphs.
• Theorem 15 (distance): $d_Q\ge m:=\min(d_1,d_2,d_1^T,d_2^T)$, with $d_Q=m$ whenever $d_i=m$ and $d_{3-i}\ne\infty$, or $d_i^T=m$ and $d_{3-i}^T\ne\infty$, for some $i\in\{1,2\}$.

The milestones follow the paper. They are Proposition 4 (validity), eq. (4), Fact 12 and Propositions 9, 10, 13 (product codes and transposes), which lead to Proposition 14. Then come eq. (17), the weight claim and Lemma 16 (lower bound), and the two claims of p. 17 and Lemma 17 (upper bound), which lead to Theorem 15. The degree count of p. 11 gives the row weights.

Significance

The result. The construction needs no orthogonality between the input codes: any two parity-check matrices give a valid CSS code. Its parameters are read off the classical inputs. A family of classical LDPC codes with fixed rate and linear distance therefore gives quantum LDPC codes with fixed rate and distance $\Theta(\sqrt N)$, and sparse inputs give sparse stabilizers. The toric code is the special case where both inputs are cycle graphs. The hypergraph product is also the base case of the later homological and lifted-product constructions, and the source of the standard decoding and fault-tolerance results for these codes.

Formalizing it. The theorem is proved in the paper; what is missing is a machine-checked proof. The platform holds the toric code's distance and dimension (ToricCode.toric_distance, ToricCode.toric_homologyRank), but over its own chain complex, not over a general construction. This mission produces a reusable layer: Tanner graphs as binary matrices, CSS dimension and distance with the $\infty$ convention, product codes, and the parameters of the hypergraph product for arbitrary finite index sets.

Difficulty

The dimension count is linear algebra once the codes $\ker H_X^T$ and $\ker H_Z^T$ have been identified with product codes. The obstacle is the distance. Lower bounds on the minimum weights of $\mathcal C_X$ and $\mathcal C_Z$ themselves are useless: $\mathcal C_Z^\perp\subseteq\mathcal C_X$ contains the rows of $H_Z$, which have constant weight, so the minimum weight of $\mathcal C_X$ is bounded by a constant. Any bound of order $\min(d_1,d_2,d_1^T,d_2^T)$ must use the definition of $d_X$ over $\mathcal C_X\setminus\mathcal C_Z^\perp$ and show that every low-weight codeword of $\mathcal C_X$ is degenerate, i.e. lies in $\mathcal C_Z^\perp$. The upper bound needs an explicit codeword of $\mathcal C_X$ outside $\mathcal C_Z^\perp$, and showing that it is not in $\mathcal C_Z^\perp$ requires an argument of its own.

Formalization scope

Lean represents a Tanner graph by its matrix H : Matrix C V (ZMod 2) over arbitrary finite index types. The code is ker H, the transpose code is ker Hᵀ, and the dual code is CodingTheory.dualCode from the published definition CodingTheory. Hamming weight is Mathlib's hammingNorm. Minimum distances live in ℕ∞, where the empty infimum is ⊤, the paper's $\infty$. $k_Q$ is the dimension of the quotient of $\mathcal C_X$ by $\mathcal C_Z^\perp\cap\mathcal C_X$. In $H_X$ and $H_Z$ the qubits are ordered $(V_1\times V_2)\sqcup(C_1\times C_2)$, as on p. 18. A product code is a set of $\iota_1\times\iota_2$ matrices whose columns (fixed second coordinate) lie in the first code. The general results are stated without nonemptiness assumptions; they hold for empty index sets.

Theorem 1 has two disclosed differences from the page:

• It adds the hypothesis $k\le n$, which is implicit in "$[n,k,d]$". Without it the matrix has no rows and the dimension claim fails.
• It drops the word "LDPC", a property of families of codes. Its finite content is the row-weight clause, which is kept.

"There is a construction" is formalized as the paper's construction, the hypergraph product of $H$ with itself.

Several encodings would trivialize the statements and are excluded: an $\mathbb N$-valued minimum distance that is $0$ on the zero code; $d_X$ taken over $\mathcal C_X\setminus\{0\}$ instead of $\mathcal C_X\setminus\mathcal C_Z^\perp$; $k_Q$ computed by truncated natural subtraction; an existential "there is a code with these parameters"; and the transpose code replaced by the dual code.

A complete development needs ranks and kernels of Kronecker products over $\mathbb F_2$, dimensions of product codes (Proposition 9, not in Mathlib), and the restriction of Tanner graphs to induced subgraphs. The product-code and CSS layers are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative arguments for Proposition 14 via the Künneth formula.

Selected references

• J.-P. Tillich and G. Zémor, Quantum LDPC codes with positive rate and minimum distance proportional to the square root of the blocklength, IEEE Transactions on Information Theory 60(2), 2014; preprint arXiv:0903.0566v2. https://arxiv.org/abs/0903.0566 , https://doi.org/10.1109/TIT.2013.2292061
• A. R. Calderbank and P. W. Shor, Good quantum error-correcting codes exist, Physical Review A 54, 1996. https://arxiv.org/abs/quant-ph/9512032
• A. M. Steane, Multiple particle interference and quantum error correction, Proceedings of the Royal Society A 452, 1996. https://arxiv.org/abs/quant-ph/9601029
• A. Yu. Kitaev, Fault-tolerant quantum computation by anyons, Annals of Physics 303, 2003. https://arxiv.org/abs/quant-ph/9707021
• F. J. MacWilliams and N. J. A. Sloane, The Theory of Error-Correcting Codes, North-Holland, 1977, Ch. 18 §2 (product codes).
• S. Evra, T. Kaufman and G. Zémor, Decodable quantum LDPC codes beyond the √n distance barrier using high-dimensional expanders, FOCS 2020. https://arxiv.org/abs/2004.07935
• M. B. Hastings, J. Haah and R. O'Donnell, Fiber bundle codes: breaking the N^{1/2} polylog(N) barrier for quantum LDPC codes, STOC 2021. https://arxiv.org/abs/2009.03921
• P. Panteleev and G. Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, STOC 2022. https://arxiv.org/abs/2111.03654
• N. P. Breuckmann and J. N. Eberhardt, Quantum low-density parity-check codes, PRX Quantum 2, 2021. https://arxiv.org/abs/2103.06309

Motivation

In the AdS/CFT correspondence a quantum theory of gravity in an asymptotically anti-de Sitter spacetime is equivalent to a conformal field theory on its boundary. A central question is how local bulk physics is encoded in the boundary theory, and in particular which bulk region is described by a given boundary subregion $R$. Harlow's TASI 2017 lectures (arXiv:1802.01040) review the answer that emerged from quantum error correction: the boundary Hilbert space is a code, bulk effective field theory lives in a code subspace, and the boundary subregion $R$ can reconstruct every bulk operator in its entanglement wedge. The lectures state as their main technical target the theorem that this entanglement wedge reconstruction, the quantum Ryu–Takayanagi (RT) formula with a central area operator, and the JLMS formula (equality of boundary and bulk relative entropies) are mathematically equivalent. All of these statements are finite-dimensional linear algebra, which makes them formalizable now.

Timeline. Almheiri, Dong and Harlow proposed the quantum-error-correction interpretation of AdS/CFT in 2014 (arXiv:1411.7041). Jafferis, Lewkowycz, Maldacena and Suh derived the JLMS relation in 2015 (arXiv:1512.06431), and Dong, Harlow and Wall established the implications between JLMS and reconstruction for factors in 2016 (arXiv:1601.05416). Harlow proved the general three-way equivalence for arbitrary finite-dimensional von Neumann algebras in 2016 (arXiv:1607.03901, Comm. Math. Phys. 2017). The TASI lectures (2017, published 2018) present this theorem as Theorem 5.2.

Setting

All Hilbert spaces are finite-dimensional. The boundary space factorizes as $\mathcal H=\mathcal H_R\otimes\mathcal H_{\overline R}$. A code subspace $\mathcal H_{code}\subseteq\mathcal H$ is described by an isometry $V$ whose columns $|\tilde i\rangle$ are an orthonormal basis of $\mathcal H_{code}$. An operator $O_R$ on $\mathcal H_R$ represents a logical operator $\tilde O$ if $O_R|\tilde\psi\rangle=\tilde O|\tilde\psi\rangle$ and $O_R^\dagger|\tilde\psi\rangle=\tilde O^\dagger|\tilde\psi\rangle$ for every code state.

A von Neumann algebra $M$ on $\mathcal H_{code}$ is a set of operators closed under sums, products and adjoints and containing all multiples of the identity; $M'$ is its commutant and $Z_M=M\cap M'$ its center. Every such $M$ is block diagonal, $\mathcal H_{code}=\bigoplus_\alpha\mathcal H_{r_\alpha}\otimes\mathcal H_{\overline r_\alpha}$ with $M=\bigoplus_\alpha\mathcal L(\mathcal H_{r_\alpha})\otimes I_{\overline r_\alpha}$. For a state $\tilde\rho$ with diagonal blocks $p_\alpha\tilde\rho_{r_\alpha\overline r_\alpha}$, the algebraic entropy is $S(\tilde\rho,M)=-\sum_\alpha p_\alpha\log p_\alpha+\sum_\alpha p_\alpha S(\tilde\rho_{r_\alpha})$, and the algebraic relative entropy $S(\tilde\rho|\tilde\sigma,M)$ is defined analogously (eqs. (5.16), (5.18)).

Formalization targets

Goal: Theorem 5.2 (entanglement wedge reconstruction theorem)

For $\mathcal H_{code}\subseteq\mathcal H_R\otimes\mathcal H_{\overline R}$ and a von Neumann algebra $M$ on $\mathcal H_{code}$, the following are equivalent:

$$\text{(1) every } \tilde O\in M \text{ is represented on } R \text{ and every } \tilde O'\in M' \text{ on } \overline R;$$ $$\text{(2) } \exists\,\mathcal L_R\in Z_M:\ S(\tilde\rho_R)=\mathrm{Tr}(\tilde\rho\mathcal L_R)+S(\tilde\rho,M),\ \ S(\tilde\rho_{\overline R})=\mathrm{Tr}(\tilde\rho\mathcal L_R)+S(\tilde\rho,M')\ \ \forall\tilde\rho;$$ $$\text{(3) } S(\tilde\rho_R|\tilde\sigma_R)=S(\tilde\rho|\tilde\sigma,M),\ \ S(\tilde\rho_{\overline R}|\tilde\sigma_{\overline R})=S(\tilde\rho|\tilde\sigma,M')\ \ \forall\tilde\rho,\tilde\sigma.$$

Milestones

• Theorem 4.1: four equivalent characterizations of a correctable erasure of $\overline R$ (operator reconstruction on $R$; $PX_{\overline R}P=\lambda P$; decoupling of a reference system from $\overline R$; the explicit encoding $|\tilde i\rangle=U_R(|i\rangle_{R_1}|\chi\rangle_{R_2\overline R})$).
• Eq. (4.25): the quantum Singleton bound $m\ge\frac{n+k}{2}$ for codes whose accessibility depends only on the number of qudits.
• Theorem 5.1: every von Neumann algebra on a finite-dimensional Hilbert space is a block-diagonal direct sum of factors, with the matching descriptions of $M'$ and $Z_M$.

Significance

Theorem 5.2 turns three separately motivated features of holography into a single mathematical statement. Since the RT formula is independently derived from the gravitational path integral, the theorem implies subregion duality in the entanglement wedge; it also shows that a non-trivial area operator requires an algebra with non-trivial center. Theorem 4.1 is the subsystem-code special case, and Theorem 5.1 is the structure result that gives the algebraic entropies their meaning.

The results are proved in the literature (Harlow 2017 for Theorem 5.2; Theorems 4.1 and 5.1 are standard), but the lectures state Theorem 5.2 without proof, and none of these statements has a machine-checked proof that this mission is aware of. The mission produces formal statements and, eventually, formal proofs of the finite-dimensional structure theory of operator-algebra quantum error correction.

Difficulty

The three conditions live at different levels: (1) is a statement about operators, (2) about von Neumann entropies of single states, and (3) about relative entropies of pairs of states. Passing between them requires control of the full block structure of $M$ relative to the bipartition $R\overline R$, not only of a single factor, and the classical term $\sum_\alpha p_\alpha\log(p_\alpha/q_\alpha)$ of (5.18) couples different blocks, so the general case does not reduce to the factor case treated earlier in the literature. Relative entropies can be infinite (when supports are not nested), so the equalities in (3) are equalities of extended reals and every argument must remain valid at $+\infty$.

Formalization scope

Hilbert spaces are coordinate spaces $\mathbb C^{\iota}$ for finite index types, operators are complex matrices, tensor products are Kronecker products, and $\mathcal H_{code}$ is the image of an isometry $V$ (an operator $O_R$ acts on code states as $O_R\otimes I_{\overline R}$ applied to $V$). States are density matrices (positive semidefinite, trace one). Von Neumann entropy and relative entropy are defined from eigen-decompositions; relative entropy takes values in the extended reals. A von Neumann algebra is a $*$-subalgebra of matrices; the algebraic entropies are computed in a block decomposition $U$ of $M$, which every statement takes as an arbitrary decomposition realizing $M$ (the value does not depend on the choice). The RT identity is stated as an equality of complex numbers. Theorem 4.1 assumes a nonzero code subspace; the Singleton bound assumes $d\ge2$ and $k\ge1$; both conditions are implicit in the lectures and are needed for the statements to be true.

A trivializing reading is excluded: the hypotheses of every statement are satisfiable, and the goal is a full equivalence of three non-trivial conditions rather than any single implication.

Useful reusable infrastructure: partial traces and their interaction with Kronecker products, entropies of block-diagonal states, relative entropy (Klein's inequality and its equality case), and the structure theory of finite-dimensional $*$-algebras of matrices. Contributions of proofs of the individual implications (1)⇒(2), (2)⇒(3), (3)⇒(1) as sketches are welcome.

Selected references

• D. Harlow, TASI Lectures on the Emergence of Bulk Physics in AdS/CFT, PoS(TASI2017)002, 2018. https://arxiv.org/abs/1802.01040
• D. Harlow, The Ryu–Takayanagi Formula from Quantum Error Correction, Comm. Math. Phys. 354 (2017) 865–912. https://arxiv.org/abs/1607.03901
• A. Almheiri, X. Dong, D. Harlow, Bulk Locality and Quantum Error Correction in AdS/CFT, JHEP 04 (2015) 163. https://arxiv.org/abs/1411.7041
• D. Jafferis, A. Lewkowycz, J. Maldacena, S. J. Suh, Relative entropy equals bulk relative entropy, JHEP 06 (2016) 004. https://arxiv.org/abs/1512.06431
• X. Dong, D. Harlow, A. C. Wall, Reconstruction of Bulk Operators within the Entanglement Wedge in Gauge-Gravity Duality, Phys. Rev. Lett. 117 (2016) 021601. https://arxiv.org/abs/1601.05416

Motivation

A quantum computer cannot perform gate operations perfectly, so a small constant error per operation is unavoidable. A priori this could mean that a noisy quantum computer can apply only a bounded number of gates before the computation is destroyed by noise, which would rule out long quantum computations in practice. The threshold theorem (or quantum fault-tolerance theorem) says that this does not happen: if the error rate of the physical components is below a constant threshold, quantum error correction can suppress the logical error rate to arbitrarily low levels at a modest cost in size. It is the quantum analogue of von Neumann's threshold theorem for classical computation with unreliable components (von Neumann 1956).

Timeline.

• 1956: von Neumann shows that reliable classical computation is possible with components that fail with a small constant probability.
• 1996: Shor gives the first fault-tolerant quantum computation scheme, proving a weaker version of the threshold theorem (Shor 1996).
• 1997-1999: the threshold theorem is proved independently, for various error models, by Aharonov and Ben-Or (arXiv:quant-ph/9906129); Knill, Laflamme and Zurek (arXiv:quant-ph/9702058); and Kitaev (arXiv:quant-ph/9707021).
• 2000: Nielsen and Chuang give the general framework stated below in their textbook.

Setting

A register of qubits is labelled by a finite set $Q$, and its states are density matrices indexed by bit strings $x:Q\to\{0,1\}$. A location applies one elementary operation to an ordered tuple of distinct qubits. The elementary operations are the gates $H$, $T=\mathrm{diag}(1,e^{i\pi/4})$ and $\mathrm{CNOT}$, the preparation of a qubit in $|0\rangle$, and a single-qubit wait. A layer is a set of locations whose supports partition the register, so idle qubits carry explicit waits. A circuit $C$ is a sequence of layers started in $|0\cdots0\rangle$, and its size $|C|$ is its total number of locations. Measuring every qubit at the end gives the outcome distribution $P_{\mathrm{ideal}}(C)$.

The hardware follows an independent stochastic noise model with fault rate at most $p$: each location, independently, is faulty with some probability $q\le p$, and a faulty location applies an arbitrary, adversarially chosen quantum channel to its own qubits instead of its ideal operation. Running a physical circuit $C'$ on such hardware gives the outcome distribution $P_{\mathrm{noisy}}(C')$. A physical circuit simulating $n$ logical qubits acts on $n$ blocks of $b$ qubits; at the end each block's measured bits are decoded to one logical bit by a fixed map $\mathrm{dec}:\{0,1\}^b\to\{0,1\}$.

Formalization targets

Goal: threshold theorem

The source states the theorem as follows: a quantum circuit on $n$ qubits containing $p(n)$ gates may be simulated with probability of error at most $\varepsilon$ using $O(\log^{c}(p(n)/\varepsilon)\,p(n))$ gates, for some constant $c$, on hardware whose components fail with probability at most $p$, provided $p$ is below some constant threshold $p_{\mathrm{th}}$, and given reasonable assumptions about the noise in the underlying hardware. Formally: there are $p_{\mathrm{th}}>0$ and $c\in\mathbb N$ such that for each $0\le p<p_{\mathrm{th}}$ there is $A$ such that for all $n$, $D$ and $0<\varepsilon<1$ there are $b$ and $\mathrm{dec}$ such that every depth-$D$ circuit $C$ on $n$ qubits has a simulation $C'$ with

$$|C'|\le A\Big(\log\tfrac{|C|}{\varepsilon}+1\Big)^{c}|C|,\qquad d_{\mathrm{TV}}\big(\mathrm{dec}_*P_{\mathrm{noisy}}(C'),P_{\mathrm{ideal}}(C)\big)\le\varepsilon$$

for every noise model with fault rate at most $p$. The goal leaves the threshold, the exponent and the constants unspecified; it asserts only the shape of the result.

Milestones

1. Errors accumulate at most linearly: without encoding, $d_{\mathrm{TV}}\le p\,|C|$.
2. Better gates: one level of encoding gives $d_{\mathrm{TV}}\le c\,p^2|C|$ with $|C'|\le A|C|$.
3. Recursion: $e_{k+1}\le c\,e_k^2$ and $e_0\le p$ imply $e_k\le (cp)^{2^k}/c$.
4. Concatenation: for every $k$, $d_{\mathrm{TV}}\le \frac{(cp)^{2^k}}{c}|C|$ with $|C'|\le A d^k|C|$.
5. Overhead: choosing $k$ to make the total error at most $\varepsilon$ costs $d^k=O\big((\log(g/\varepsilon)+1)^{\lceil\log_2 d\rceil}\big)$.

Significance

The theorem shows that noise is not a fundamental obstacle to scalable quantum computation: any efficient ideal quantum algorithm remains efficient on noisy hardware once the physical error rate is below a constant. Current estimates put the threshold for the surface code on the order of $1\%$ (Fowler, Stephens, Groszkowski 2009), and the theorem underlies the resource estimates that guide current hardware development (Campbell, Terhal, Vuillot 2017).

The theorem has been proved on paper in several forms. A machine-checked proof requires an explicit model of noisy circuits, the construction of fault-tolerant gadgets for a universal gate set, and the probabilistic bookkeeping that is usually left informal. This mission provides the model and an attack path that follows the standard proof strategy.

Difficulty

Encoding a gate in an error-correcting code makes it larger, and therefore exposes it to more faults. The whole difficulty is to show that errors are corrected faster than they are created: every encoded gadget, including error correction itself and the non-Clifford $T$ gate, must be designed so that a single fault cannot cause a logical failure, and this must hold uniformly at every level of concatenation. Simply repeating each operation and taking a majority vote does not work for quantum states, which cannot be copied, and measuring a qubit directly destroys the encoded information.

Formalization scope

All statements use one definition file. Qubits of the physical register are labelled by Fin n × Fin b; states are complex matrices indexed by Q → Fin 2; channels are lists of Kraus operators; noise is the independent stochastic model above, with per-location fault probabilities in $[0,p]$ and arbitrary fault channels. No mid-circuit measurement is available, but qubits can be re-prepared in $|0\rangle$ at any time. Sizes count every location, idle steps included. The block size and the decoder may depend on $n$, the depth, $\varepsilon$ and $p$, but never on the circuit being simulated; this rules out a decoder that simply writes down the answer, and the size bound rules out classical brute-force simulation inside the physical circuit.

A complete development needs: trace-distance and contractivity facts for channels, a quantum error-correcting code with fault-tolerant gadgets for $H$, $T$, $\mathrm{CNOT}$, preparation and error correction, a fault-counting argument for one level of encoding, and its iteration under concatenation. The channel and trace-distance infrastructure is reusable beyond this mission.

Selected references

• J. von Neumann, Probabilistic Logics and the Synthesis of Reliable Organisms From Unreliable Components, Automata Studies, Princeton University Press, 1956. https://doi.org/10.1515/9781400882618-003
• P. W. Shor, Fault-tolerant quantum computation, Proc. 37th FOCS, 1996. https://doi.org/10.1109/SFCS.1996.548464
• D. Aharonov and M. Ben-Or, Fault-Tolerant Quantum Computation with Constant Error Rate, SIAM J. Comput. 38(4), 2008. https://arxiv.org/abs/quant-ph/9906129
• E. Knill, Resilient Quantum Computation, Science 279, 1998. https://arxiv.org/abs/quant-ph/9702058
• A. Yu. Kitaev, Fault-tolerant quantum computation by anyons, Annals of Physics 303, 2003. https://arxiv.org/abs/quant-ph/9707021
• M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, 10th anniversary ed., Cambridge University Press, 2010.
• Wikipedia, Threshold theorem. https://en.wikipedia.org/w/index.php?title=Threshold_theorem&oldid=1360742213

Motivation

This mission develops Chapter 3 of An Introduction to Quantum Error Correction and Fault-Tolerant Quantum Computation by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

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.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• Theorem 5: Stabilizer codes: an Abelian S of order 2^a without -1 gives an [[n, n-a, d]] code.
• Lemma 1: Every error syndrome of a stabilizer is realized by a Pauli error.

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

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

Motivation

This mission develops Chapter 4 of Stabilizer Codes and Quantum Error Correction by Daniel Gottesman. The chapter's selected results describe the mathematical guarantees below.

Setting and conventions

The linked theorem statements and shared definitions specify the register types, oracle access, normalization, and resource conventions. Their source locators and independent readbacks accompany each target.

Chapter goal

Let a stabilizer on $n=m+k$ qubits ($m=n-k$ generators) be given in the standard form (4.3) of §4.1,

$$\left(\begin{array}{ccc|ccc} I & A_1 & A_2 & B & C_1 & C_2\\ 0 & 0 & 0 & D & I & E\end{array}\right),$$

with $r$ rows in the first block, and assume its rows commute: $H_xH_z^{\mathsf T}+H_zH_x^{\mathsf T}=0$. For a binary row $(a\,|\,b)$ write $P(a|b)=\bigotimes_q \sigma_z^{b_q}\sigma_x^{a_q}$ (the real form, sign $+1$). Let $M_i=P(\text{row } i)$ be the generators and let $\bar X_1,\dots,\bar X_k$ be the logical $\sigma_x$ operators in the standard form of p.40: $\bar X_i=P(0\,u_2\,e_i\,|\,v_1\,0\,0)$ with $u_2$ the $i$-th row of $E^{\mathsf T}$ and $v_1$ the $i$-th row of $E^{\mathsf T}C_1^{\mathsf T}+C_2^{\mathsf T}$.

Let $U_{\mathrm{enc}}$ be the encoding network of §4.2 (with the author's errata): first, for each $i$, the controlled-NOTs that apply $\bar X_i$ without its final $\sigma_x$, controlled on qubit $n-k+i$; then, for $i=1,\dots,r$ in turn, the Hadamard $R$ on qubit $i$, a $\sigma_z$ on qubit $i$ if $B_{ii}=1$, and $M_i$ without its qubit-$i$ factor, controlled on qubit $i$ (controlled-$\sigma_z^{b}\sigma_x^{a}$ gates). Then for every $c=c_1\dots c_k\in\{0,1\}^k$,

$$U_{\mathrm{enc}}\,|0\dots0\rangle|c_1\dots c_k\rangle=\frac{(I+M_1)\cdots(I+M_{n-k})\,\bar X_1^{c_1}\cdots\bar X_k^{c_k}|0\dots0\rangle}{\big\|(I+M_1)\cdots(I+M_{n-k})\,\bar X_1^{c_1}\cdots\bar X_k^{c_k}|0\dots0\rangle\big\|},$$

and in particular the vector on the right-hand side is nonzero.

This is the correctness of Gottesman's general encoding circuit for stabilizer codes: the network prepares exactly the encoded basis states, with no leftover global phase.

Formalization Note The errata are built in: the Hadamard on qubit $i$ comes just before that qubit's control operations, controlled-$Y$ gates are controlled-$\sigma_z\sigma_x$ gates in the real form, and every generator has sign $+1$. The page writes encoded states unnormalized; the unitary network yields the normalized vector. Since the real form $\sigma_z\sigma_x=i\sigma_y$, a generator with an odd number of $(1|1)$ positions is $i$ times a Hermitian Pauli operator; the identity is the one the page's network computes in this convention.

Significance

These are known mathematical results. Their Lean statements have been checked and reviewed against the cited source; formal proofs remain open for contributors.

Supporting targets

• §4.1: Every stabilizer code can be put into the standard form (4.3).
• §4.2: The standard-form encoding network maps |c⟩ to the encoded basis state (4.8).

Formalization scope

Prove the existing statements under their stated hypotheses and definitions. Any correction to a printed source claim remains explicit in its target description. All listed target proofs are currently sorry; no proof is claimed. The mission goal is the designated chapter capstone; the remaining targets are separate milestones. Parts a, b, c and d are merged into their original chapter.

Selected references

• Daniel Gottesman, Stabilizer Codes and Quantum Error Correction, 1997 thesis, downloaded arXiv v1 PDF; PDF title page now prints 2024. https://arxiv.org/pdf/quant-ph/9705052v1.