Quantum Error Correction

Motivation

Quantum error correction protects quantum information from noise by storing it in a code and undoing the damage with a recovery operation. The textbook theory, the Knill–Laflamme conditions, characterizes codes that can be corrected perfectly. Real noise rarely admits perfect correction, and codes that are only approximately correctable can perform better than perfect ones: they can use fewer physical resources for a given target fidelity. Approximate quantum error correction (AQEC) asks for algebraic conditions that tell, from the noise and the code alone, how well a code can be corrected.

Mandayam and Ng (arXiv:1202.5139, Phys. Rev. A 2012) extend an earlier AQEC framework for subspace codes (Ng and Mandayam, arXiv:0909.0931, 2010) to subsystem codes, where information is stored in one tensor factor $A$ of a subspace $\mathcal H_A\otimes\mathcal H_B$ and the factor $B$ is a gauge whose state does not matter. Subsystem codes include noiseless subsystems and the Bacon–Shor family, and they are the natural setting for operator quantum error correction (Kribs, Laflamme and Poulin, arXiv:quant-ph/0412076, 2005).

Setting

The system space is $\mathcal H=\mathcal H_A\otimes\mathcal H_B\oplus\mathcal K$, with $\mathcal H_A$, $\mathcal H_B$ finite dimensional; $P$ is the projector onto $\mathcal H_{AB}=\mathcal H_A\otimes\mathcal H_B$ and $P_A,P_B$ the identities of the factors. The code $\mathcal C$ is the set of all product states $\rho_A\otimes\rho_B$, with $\rho_A,\rho_B$ density operators.

The noise $\mathcal E$ is a completely positive, trace-preserving (CPTP) map with Kraus operators $E_1,\dots,E_N:\mathcal H_{AB}\to\mathcal H$:

$$\mathcal E(\rho)=\sum_iE_i\rho E_i^\dagger,\qquad \sum_iE_i^\dagger E_i=P .$$

Write $\mathcal P_{\mathcal E}$ for the support of $\mathcal E(P)=\sum_iE_iE_i^\dagger$. A recovery is a CP map $\mathcal R:\mathcal B(\mathcal P_{\mathcal E})\to\mathcal B(\mathcal H_{AB})$ that is trace preserving on $\mathcal P_{\mathcal E}$.

The fidelity of states is $F(\rho,\sigma)=\mathrm{tr}\sqrt{\rho^{1/2}\sigma\rho^{1/2}}$. The fidelity loss of the code state $\rho$ under $\mathcal E$ and $\mathcal R$ compares the information in $A$ before and after:

$$\eta_{\mathcal R}\{\rho\}=1-F^2\big(\mathrm{tr}_B\,\rho,\ \mathrm{tr}_B[(\mathcal R\circ\mathcal E)(\rho)]\big).$$

The code is $\epsilon$-correctable on $A$ under $\mathcal E$ when some recovery has $\eta_{\mathcal R}\{\rho\}\le\epsilon$ for every $\rho\in\mathcal C$.

The transpose channel $\mathcal R_P$ is the recovery with Kraus operators

$$R^P_i=P\,E_i^\dagger\,\mathcal E(P)^{-1/2},$$

the inverse square root being taken on the support of $\mathcal E(P)$.

Formalization targets

Goal: Corollary 3

Suppose that, for all $i,j$,

$$PE_i^\dagger\mathcal E(P)^{-1/2}E_jP=P_A\otimes B_{ij}+\Delta_{ij}\qquad(12)$$

with $B_{ij}$ operators on $\mathcal H_B$ and $\Delta_{ij}$ operators on $\mathcal H_{AB}$. Then the transpose channel is a recovery, and for every $\rho\in\mathcal C$

$$\eta_{\mathcal R_P}\{\rho\}\le\Big\|\sum_{ij}\Delta_{ij}^\dagger\Delta_{ij}\Big\|,$$

so $\mathcal C$ is $\epsilon$-correctable on $A$ whenever $\epsilon\ge\|\sum_{ij}\Delta_{ij}^\dagger\Delta_{ij}\|$ (operator norm). The statement holds for every choice of the operators $B_{ij}$; each choice determines $\Delta_{ij}$ and gives a bound.

Theorem 2

Under (12), $\mathcal C$ is $\epsilon$-correctable on $A$ for every $\epsilon\ge\eta_P$, where

$$\eta_P=\max_{|\psi_A,\phi_B\rangle}\langle\phi_B|\sum_{ij}\Big[\langle\psi_A|\Delta^\dagger_{ij}\Delta_{ij}|\psi_A\rangle-\langle\psi_A|\Delta^\dagger_{ij}|\psi_A\rangle\langle\psi_A|\Delta_{ij}|\psi_A\rangle\Big]|\phi_B\rangle$$

is the fidelity loss of the transpose channel. Theorem 2 is sharper than Corollary 3; the corollary trades sharpness for a quantity that is easy to compute.

Milestones

The milestones follow the paper's own steps: the pure-state form (5) of the fidelity; the reduction of the worst case over $\mathcal C$ to pure product states; trace preservation of $\mathcal R_P$ on $\mathcal P_{\mathcal E}$; the trace-preservation identity of $\mathcal R_P\circ\mathcal E$ in terms of $B_{ij},\Delta_{ij}$; the fidelity formula (14) on pure product states; Theorem 2; and the bound of the expression (13) by the operator norm.

Significance

When all $\Delta_{ij}$ vanish, (12) is the paper's perfect-correction condition (Theorem 1), and the transpose channel is a perfect recovery. Corollary 3 quantifies the robustness of that statement: a perturbation of size $\|\sum\Delta^\dagger\Delta\|$ costs at most that much fidelity loss, with an explicit recovery. This turns the search for approximate subsystem codes into a check of a matrix inequality, and it supplies the sufficient half of a characterization whose necessary half (near-optimality of the transpose channel) the paper establishes only in restricted scenarios.

Status: the results are proved in the paper, not formalized. Prove2Me's catalog has no statement of Theorem 2, Corollary 3, or of perfect-correction conditions for subsystem codes. This mission states the subsystem-code model in Lean, with mixed code states and a possibly singular $\mathcal E(P)$, and poses each step of the paper's proof as a target. The reduction to pure states needs the joint concavity of the fidelity, which Mathlib does not have; a proof of it is reusable across quantum information theory.

Difficulty

Two steps resist a direct computation. First, the code contains mixed product states, while the fidelity formula (14) is available only for pure ones; the passage from one to the other is the joint concavity of $F$, a consequence of Uhlmann's theorem, not a linear-algebra identity. Second, $\mathcal E(P)$ need not be invertible: $\mathcal E(P)^{-1/2}$ is a pseudo-inverse, the transpose channel is trace preserving only on $\mathcal P_{\mathcal E}$, and the trace-preservation identity of $\mathcal R_P\circ\mathcal E$ needs that each $E_j$ maps into $\mathcal P_{\mathcal E}$. Arguments that treat $\mathcal E(P)^{-1/2}$ as an inverse are wrong in general.

Formalization scope

• $\mathcal H_{AB}$ is indexed by a × b with $A$ first, matching ⊗ₖ and the published partial trace; $\mathcal H$ is a separate finite type o. The noise's Kraus operators are rectangular matrices Matrix o (a × b) ℂ, so $P$, $P_A$, $P_B$ are identity matrices and $P_A\otimes B_{ij}$ is 1 ⊗ₖ B i j.
• Vectors are a → ℂ, unit when star ψ ⬝ᵥ ψ = 1; $|\psi\rangle\langle\psi|$ is vecMulVec ψ (star ψ).
• Published definitions are reused: the fidelity (WildeQIT.fidelity $=F^2$, rootFidelity $=F$), the partial trace WildeQIT.partialTraceRight, the channel action PeresTerno.krausUpdate, density matrices PeresTerno.IsDensityMatrix, and the support inverse square root and support projector QReversal.NearOpt.invSqrt, supportProj.
• A recovery is any finite Kraus family $R_k$ from o to a × b with $\mathcal P_{\mathcal E}(\sum_kR_k^\dagger R_k)\mathcal P_{\mathcal E}=\mathcal P_{\mathcal E}$. Full support of $\mathcal E(P)$ is not assumed.
• $\epsilon$-correctability is the existence of a recovery with fidelity loss at most $\epsilon$ on every code state; it is equivalent to the paper's $\epsilon\ge\eta_{\mathrm{op}}$ because the minimum defining $\eta_{\mathrm{op}}$ is attained. "$\epsilon\ge\eta_P$" is stated as a bound on the expression (13) at every pair of unit vectors, with no supremum.
• The norm in (15) is the operator norm, Mathlib's Matrix.Norms.L2Operator; neither the entrywise sup norm nor the Frobenius norm.

The statements carry no smallness hypothesis on $\Delta_{ij}$, quantify over all code states including mixed ones rather than over pure states only, and admit only recoveries that are trace preserving on $\mathcal P_{\mathcal E}$; each of these restrictions would make the goal weaker or trivial.

Needed infrastructure: the continuous functional calculus identities for $X^{-1/2}XX^{-1/2}$ and for range inclusions of $\sum_iE_iE_i^\dagger$, Kronecker-product algebra, and joint concavity (or Uhlmann's theorem) for the fidelity. Proofs of any milestone, and general fidelity lemmas usable beyond this mission, are welcome.

Selected references

• P. Mandayam and H. K. Ng, Towards a unified framework for approximate quantum error correction, Phys. Rev. A 86, 012335 (2012). arXiv:1202.5139 (version v2 is the one formalized).
• H. K. Ng and P. Mandayam, Simple approach to approximate quantum error correction based on the transpose channel, Phys. Rev. A 81, 062342 (2010). arXiv:0909.0931
• D. Kribs, R. Laflamme and D. Poulin, Unified and generalized approach to quantum error correction, Phys. Rev. Lett. 94, 180501 (2005). arXiv:quant-ph/0412076
• E. Knill and R. Laflamme, Theory of quantum error-correcting codes, Phys. Rev. A 55, 900 (1997). arXiv:quant-ph/9604034
• H. Barnum and E. Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, J. Math. Phys. 43, 2097 (2002). arXiv:quant-ph/0004088

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 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

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

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 that runs long computations must protect its data with a quantum error-correcting code and must compute on the encoded data without letting errors spread. The simplest gates with that property are transversal gates: a code is laid out in several code blocks, and a transversal gate couples each physical subsystem of one block only to the corresponding subsystem of the other blocks, so a single fault never becomes several faults inside one block (Gottesman 1997; Aliferis, Gottesman, Preskill 2006). Every known code has some encoded gate that is not transversal, and fault-tolerant schemes pay for the missing gates with expensive constructions such as magic-state distillation. Whether some code has a universal transversal gate set was a long-standing question.

Timeline.

• 2007: Zeng, Cross and Chuang show that transversal gates are not universal for stabilizer codes on qubits (arXiv:0706.1382).
• 2008: Chen, Chung, Cross, Zeng and Chuang extend this to stabilizer codes on qudits (arXiv:0801.2360).
• 2008–2009: Eastin and Knill prove the statement for every code that detects an arbitrary error on any single subsystem, stabilizer or not (arXiv:0811.4262; Phys. Rev. Lett. 102, 110502, 2009). This is the result of the present mission, now called the Eastin–Knill theorem.

Setting

A composite quantum system $\mathcal Q$ consists of finitely many physical subsystems $j$, subsystem $j$ having dimension $d_j$. Operators on $\mathcal Q$ are complex matrices on $\mathbb C^{d_1}\otimes\cdots\otimes\mathbb C^{d_n}$. A product operator is $\bigotimes_j U_j$ with $U_j$ acting on subsystem $j$, and $\mathcal T$ is the group of unitary product operators ($U_j \in \mathcal U(d_j)$).

A quantum code is a subspace of the state space, represented by the orthogonal projector $P$ onto it; its dimension $\operatorname{rank} P$ is the dimension of the encoded system, and the code is nontrivial when this dimension is at least $2$. An error $E$ is detectable when $PEP \propto P$. The code is local-error-detecting when every error on any single subsystem is detectable: $P\,(I\otimes E\otimes I)\,P \propto P$ for every operator $E$ acting on one subsystem.

A unitary $U$ is logical when it preserves the code space,

$$(I-P)\,U\,P = 0 \qquad \text{(Eq. (1))},$$

and $\mathcal G$ denotes the logical unitary product operators. An encoded unitary is a unitary operator $W$ of the code space ($PWP = W$, $W^\dagger W = WW^\dagger = P$). A set $S$ of unitaries is universal when every encoded unitary is approximated to arbitrary accuracy by the actions $PUP$, $U \in S$, on the code space.

For a code made of blocks $b$, each with subsystems at the same positions $j$ and a block code $P_b$, the joint code is $P = \bigotimes_b P_b$. The transversal part $j$ collects subsystem $j$ of every block, and a transversal unitary is a product of unitaries, one on each transversal part.

Formalization targets

Goal: Corollary 1

For block codes $P_b$, each local-error-detecting, with $\operatorname{rank}\bigotimes_b P_b \ge 2$, the set $\mathcal G$ of transversal logical unitaries is not universal:

$$\{\,W : PWP = W,\ W^\dagger W = WW^\dagger = P\,\}\ \not\subseteq\ \overline{\{\,PUP : U \in \mathcal G\,\}}.$$

Theorem 1 (milestone)

The same conclusion for product operators on the physical subsystems of a single local-error-detecting code with $\operatorname{rank} P \ge 2$.

Milestones on the way

In attack order: Lemma 1 (logical unitaries form a group); Lemma 2 (logical unitaries in a closed group of unitaries form a closed subgroup); $\mathcal T$ is a compact group; the derivative step $(I-P)DP = 0$; elements of the Lie algebra of $\mathcal T$ are sums of local Hermitian operators; $DP \propto P$ for a logical sum of local Hermitians; the identity component $\mathcal C$ of $\mathcal G$ acts on the code space as a scalar; $\mathcal G$ has finitely many actions on the code space up to phase; Theorem 1; and the detectability of an error on a single transversal part.

Significance

The result. The theorem rules out the simplest route to fault tolerance for every code that detects single-subsystem errors, which includes every code of distance at least $2$. It explains why every fault-tolerant architecture needs a non-transversal ingredient (state injection and distillation, code switching, gauge fixing, measurements with feed-forward), and it is the starting point for later refinements: approximate and covariant versions for continuous symmetries (Faist et al. 2020), and restrictions on the level of the Clifford hierarchy reachable transversally (Bravyi–König 2013).

Formalizing it. The result is proved; no machine-checked proof of it is known to exist. The mission produces a checked statement of the theorem for arbitrary finite-dimensional subsystems and arbitrary (non-stabilizer) codes, together with a reusable layer: tensor-product operators on index-typed subsystems, codes as projectors, logical operators, local error detection, encoded universality and block codes. Related platform items are QAlgorithms_Defs_QECC (qubit stabilizer codes, detectability for submodule codes) and QAlgorithms.GottesmanIntro.knillLaflamme (the error-correction criterion), which use a different model of codes and are not imported here.

Difficulty

The paper's argument runs through Lie theory: $\mathcal G$ is a closed subgroup of the compact group $\mathcal T$, so it is a compact Lie group with finitely many connected components; its identity component is generated by exponentials of its Lie algebra, and local error detection forces that Lie algebra to act on the code space by scalars. None of this is about the code alone; the difficulty is the passage from a closed matrix group to its Lie algebra and back (exponential coordinates, connectedness of the identity component, finiteness of the component group of a compact Lie group). Mathlib has the matrix exponential and compactness of the unitary group but not Cartan's closed-subgroup theorem or the Lie algebra of a closed matrix group.

A frequent first idea, that $\mathcal G$ itself is a finite group, is false: every global phase $e^{i\theta}I$ is a logical product unitary, so $\mathcal G$ always contains a circle. Only the action of $\mathcal G$ on the code space is finite, and only up to phase; a statement that ignores the phase is false.

Formalization scope

Subsystem $j$ is a finite index type $\alpha_j$ (so $d_j = |\alpha_j|$), and the system has basis $\prod_j \alpha_j$; operators are Matrix over ℂ, unitaries are Matrix.unitaryGroup. A code is its projector (Hermitian, idempotent) and its dimension is Matrix.rank; "nontrivial" is $2 \le \operatorname{rank} P$. Closure is in the standard topology on complex matrices, which is the topology of any norm. Exponentials are NormedSpace.exp with the factor $i$ of the physics convention (footnote 1).

Disclosed restatements:

1. "Lie group/Lie subgroup" (Lemma 2, $\mathcal T$) is stated as closed or compact subgroup; Cartan's theorem is not in Mathlib.
2. "$D$ in the Lie algebra" is stated through the one-parameter group $t\mapsto e^{itD}$.
3. The real coefficients $\alpha_j$ in $D = \sum_j \alpha_j H_j$ are absorbed into the Hermitian $H_j$.
4. The page's "the constant of proportionality must be one" is a slip (global phases lie in $\mathcal C$); the identity-component and finite-actions milestones state $CP \propto P$ and $GP = c\,FP$.
5. Corollary 1's code blocks are a tensor product of block codes $P_b$ with common positions $j$ and possibly different codes and dimensions; a single block is Theorem 1.

Universality is defined only through approximation of encoded unitaries, local error detection quantifies over every matrix on one subsystem, and $\mathcal G$ is the full intersection of $\mathcal T$ with the logical unitaries, so no hypothesis trivializes the conclusion; at rank $1$ the conclusion is false, which is why the rank hypothesis is $\ge 2$ and not $P \ne 0$.

A complete development needs the Lie algebra of a closed subgroup of Matrix.unitaryGroup, connectedness of the identity component via exponentials, and finiteness of the component group of a compact matrix group. These parts are reusable far beyond this mission, and contributions of them, as well as alternative proofs of Theorem 1 that avoid Lie theory, are welcome.

Selected references

• B. Eastin, E. Knill, Restrictions on Transversal Encoded Quantum Gate Sets, Phys. Rev. Lett. 102, 110502 (2009). https://arxiv.org/abs/0811.4262
• B. Zeng, A. Cross, I. L. Chuang, Transversality versus Universality for Additive Quantum Codes, IEEE Trans. Inf. Theory 57 (2011). https://arxiv.org/abs/0706.1382
• X. Chen, H. Chung, A. W. Cross, B. Zeng, I. L. Chuang, Subsystem stabilizer codes cannot have a universal set of transversal gates for even one encoded qudit, Phys. Rev. A 78, 012353 (2008). https://arxiv.org/abs/0801.2360
• D. Gottesman, Stabilizer Codes and Quantum Error Correction, PhD thesis, Caltech (1997). https://arxiv.org/abs/quant-ph/9705052
• S. Bravyi, R. König, Classification of topologically protected gates for local stabilizer codes, Phys. Rev. Lett. 110, 170503 (2013). https://arxiv.org/abs/1206.1609
• P. Faist et al., Continuous symmetries and approximate quantum error correction, Phys. Rev. X 10, 041018 (2020). https://arxiv.org/abs/1902.07714

Why decoding good quantum LDPC codes matters

Quantum computers must correct errors faster than they accumulate, and quantum low-density parity-check (LDPC) codes are the leading candidates for doing so with little overhead: every check involves a bounded number of qubits, so syndromes can be measured by local circuits. In 2021–2022 the first asymptotically good quantum LDPC codes appeared, with dimension and minimum distance both linear in the code length $n$: the expander lifted product codes of Panteleev and Kalachev (arXiv:2111.03654) and the quantum Tanner codes of Leverrier and Zémor (arXiv:2202.13641). A code is only useful if errors can be corrected efficiently. Leverrier and Zémor (arXiv:2208.05537) give two decoders for quantum Tanner codes that correct every error of weight up to a constant fraction of $n$: a sequential one running in linear time, and a parallel decoder running in a logarithmic number of rounds of local updates. This mission is about the parallel decoder.

Timeline:

• 2021, Panteleev–Kalachev: asymptotically good quantum LDPC codes and locally testable classical codes (arXiv:2111.03654).
• 2022, Leverrier–Zémor: quantum Tanner codes, a simpler construction on left-right Cayley complexes (arXiv:2202.13641).
• 2022, Gu–Pattison–Tang, Leverrier–Zémor and Dinur–Hsieh–Lin–Vidick: efficient decoders for linear-distance quantum LDPC codes (arXiv:2206.06557, arXiv:2206.07571, arXiv:2206.07750).
• 2022, Leverrier–Zémor, Decoding quantum Tanner codes: sequential and parallel decoders up to a constant fraction of $n$, with a revised parallel analysis in v3 (arXiv:2208.05537v3).

The code and the decoder

Let $G$ be a finite group and $A=A^{-1}$, $B=B^{-1}\subseteq G$ with $|A|=|B|=\Delta$. The quadripartite left-right Cayley complex has four copies of $G$ as vertices, $V_{ij}=G\times\{ij\}$, and one square $\{(g,00),(ag,01),(gb,10),(agb,11)\}$ for every $(g,a,b)\in G\times A\times B$. The set of squares $Q$ has $n=|G|\Delta^2$ elements, and every vertex $v$ sees its $Q$-neighbourhood $Q(v)$ as an $A\times B$ array: columns are indexed by $b$, rows by $a$. The left Cayley graph $\mathrm{Cay}(G,A)$ and the right Cayley graph $\mathrm{Cay}(G,B)$ are assumed to be non-bipartite Ramanujan graphs: every adjacency eigenvalue other than $\pm\Delta$ has absolute value at most $2\sqrt{\Delta-1}$.

Two local codes $C_A\subseteq\mathbb F_2^A$, $C_B\subseteq\mathbb F_2^B$ with $\dim C_A+\dim C_B=\Delta$ are fixed. Write $V_0=V_{00}\cup V_{11}$ and $V_1=V_{01}\cup V_{10}$. The code $\mathcal C_1\subseteq\mathbb F_2^Q$ consists of the vectors whose view on every $Q(v)$, $v\in V_1$, lies in the dual tensor code $C_A\otimes\mathbb F_2^B+\mathbb F_2^A\otimes C_B$: every local view is a sum of a word whose columns are in $C_A$ and a word whose rows are in $C_B$. $\mathcal C_0$ is defined in the same way on $V_0$ with $C_A^\perp$, $C_B^\perp$. The local codes and their duals have distance at least $\delta\Delta$. Both dual tensor codes are $\kappa$-product-expanding: every codeword $x$ splits as $x=c+r$ with $|x|\ge\kappa\Delta(\|c\|+\|r\|)$, where $\|c\|$ counts non-zero columns and $\|r\|$ non-zero rows.

A $\sigma_x$-type error $e\in\mathbb F_2^Q$ is decoded in three phases. In the preprocessing phase every $v\in V_1$ chooses a minimum-weight local error $\varepsilon_v$ with the local syndrome of $e$; the mismatch is $Z=\sum_{v\in V_1}\varepsilon_v$. The mismatch decomposition writes $Z=\hat C_0+\hat R_0+\hat C_1+\hat R_1$, with $\hat C_j$ a sum of $C_A$-columns and $\hat R_i$ a sum of $C_B$-rows. Postprocessing outputs $\hat e=\sum_{v\in V_{10}}\varepsilon_v+\hat C_0+\hat R_1$. The parallel decoder (Algorithm 3) runs rounds of four substeps, one for each of $V_{00},V_{01},V_{10},V_{11}$. In a substep, every vertex $v$ of the current class simultaneously looks for a non-zero local dual tensor codeword $x_v$ on $Q(v)$ with $|\hat Z|-|\hat Z+x_v|\ge|x_v|/2$, picks one of maximum weight, splits it as $c_v+r_v$ with $\|c_v\|+\|r_v\|$ minimal, and updates $\hat C_j$, $\hat R_i$ and $\hat Z$.

Formalization targets

Goal: Theorem 20 (= Theorem 3)

Fix $\varepsilon\in(0,1/6)$ and $\delta,\kappa>0$. For all $\Delta$ large enough, every error with

$$|e|<\frac1{2^{12}}\min\Big(\frac{\varepsilon^3}{16},\frac\kappa4\Big)\delta^2\kappa^2\frac n\Delta$$

is corrected by every run of the parallel decoder. With $\theta=\frac14\big(\frac14-\frac32\varepsilon\big)$, each round satisfies $|\hat Z_{k+1}|\le(1-\theta)|\hat Z_k|$, so $\hat Z_k=0$ once $(1-\theta)^k\cdot4|e|<1$, and then $e+\hat e$ lies in the span $\mathcal C_0^\perp$ of the $\sigma_x$-generators.

Milestones

• Lemma 4 (expander mixing) and Lemma 5: $\lambda(\mathcal G^\square_0),\lambda(\mathcal G^\square_1)\le4\Delta$.
• Lemmas 7, 10, 11, 8 and Theorem 9: the minimum distance, $d_{\min}\ge\delta^2\kappa^2n/(1024\Delta)$.
• Lemmas 14, 15, 16 and Theorem 12: if a minimum decomposition of a non-zero mismatch has few active vertices, some local codeword lowers $|Z|$ by $(1-\varepsilon)|x_v|$.
• Lemma 17: $|Z|\le4|e|$ and $\|Z\|\le4|e|/(\kappa\Delta)$.
• Lemma 19: below $2^{-16}\varepsilon^3\kappa^2\delta^2n/\Delta$, sequential decoding with parameter $1/2$ never stalls, and switching to $\varepsilon$ still converges.
• Lemma 18: if the $\varepsilon$-sequential decoder converges, one parallel round removes at least $\theta|Z|$.

Significance

The theorem shows that asymptotically good quantum LDPC codes can be decoded against adversarial errors of linear weight by $O(\log n)$ rounds of local computation, each vertex acting only on its own $Q$-neighbourhood. This matters for fault tolerance, where decoding latency is a bottleneck. The milestones carry independent value. Theorem 9 is a linear minimum distance bound for quantum Tanner codes in the quadripartite setting. Theorem 12 is the local-to-global "weight reduction" principle on which both decoders rest. Lemmas 4–5 are spectral facts about Cayley graphs and square complexes that are reusable for any expander-based code.

The paper's results are proved, not open; none has been machine-checked. The sequential decoder's correctness (Theorem 13) is posed separately on the platform as an open goal in the mission Decoding quantum Tanner codes (Leverrier, Zemor), which shares this mission's published definitions; this mission does not restate it. Formalizing the present chain would give a complete, checked proof that a parallel decoder exists for good quantum LDPC codes, and would expose the constants. Two printed constants are corrected here (see the scope section), and sharper constants or simpler arguments are welcome.

Difficulty

The obvious argument is to bound the mismatch and its norm, apply Theorem 12 repeatedly, and let all vertices of a class flip at once. That argument fails because parallel flips are not sequential flips. A vertex's best local move against the mismatch at its turn need not be the move a converging sequential run would make, and a round could stall even though a sequential run never does. Lemma 18 resolves this with a virtual sequential run, a partition of its increments into "good" and "bad" ones (Claim 1), and the maximum-weight rule at every vertex. Without that rule the lemma is false. Theorem 12 itself is a counting contradiction. It uses robustness, the expander mixing lemma twice, and two notions of "exceptional" vertices, and it needs $\Delta$ large. Theorem 9 needs the coset-minimization of Lemma 7 before the same counting can start.

Formalization scope

The development builds on the published layers QAlgorithms_Defs_TensorCode and QAlgorithms_Defs_TannerDecoder. These define the complex, $\varphi_v$, $\mathcal C_0$, $\mathcal C_1$, the $\sigma_x$ span, minimum local corrections, the mismatch, Algorithm 2 and the output $\hat e$. The conventions are:

• A vertex $(g,ij)$ is (g, (i, j)) : G × (Bool × Bool), squares are G × A × B, and weights are hammingNorm cast to ℝ.
• One new definitions file holds Algorithm 3 (admissible move, parallel choice, substep, round, run), decompositions and their norm, active, exceptional and ordinary vertices, the clustering sets $T$, stalled and converging sequential decoders, $\mathcal C_1^\perp$, and the square graphs $\mathcal G^\square_k$.
• "$\Delta$ large enough" is $\exists\Delta_0\,\forall\Delta\ge\Delta_0$, with $\Delta_0$ depending only on the constants fixed before it.
• Only $\sigma_x$-type errors are treated; the $\sigma_z$ case is symmetric.
• Non-bipartiteness of the Cayley graphs (the standing choice of p. 10) is assumed wherever spectral bounds are used.
• Theorem 12 assumes $Z\ne0$ and asks for a non-zero $x_v$.

Corrected constants. Theorem 9 is stated with $1024$ instead of the printed $256$, because Lemma 8 and the proof's $|x|\ge\frac{\kappa\Delta}2\|x\|$ give $1024$. The goal's error bound uses $\min(\varepsilon^3/16,\kappa/4)$ instead of $\min(\varepsilon^3/16,\kappa)$, which is what the corrected distance supports. Both corrected statements are weaker than the printed ones.

No trivialization. Every vertex must flip a maximum-weight admissible move whenever one exists, and runs range over all such choices. "Logarithmic time" is the per-round contraction factor, not mere eventual termination. Validity is membership of $e+\hat e$ in the $\sigma_x$-generator span, with $\hat e$ the paper's postprocessing output. A formalization that lets vertices idle, drops the maximum-weight rule, or proves only eventual termination does not prove this theorem.

Needed and reusable infrastructure:

• spectral graph theory for regular multigraphs (expander mixing, eigenvalues of commuting Cayley adjacencies);
• product expansion and local minimality of decompositions;
• the combinatorics of the left-right complex (shared rows and columns).

Contributions proving the graph lemmas or Lemma 18, whose proof is pure counting, are especially welcome.

Selected references

• A. Leverrier, G. Zémor, Decoding quantum Tanner codes, IEEE Transactions on Information Theory; arXiv:2208.05537v3, 2022. https://arxiv.org/abs/2208.05537
• A. Leverrier, G. Zémor, Quantum Tanner codes, FOCS 2022; arXiv:2202.13641. https://arxiv.org/abs/2202.13641
• P. Panteleev, G. Kalachev, Asymptotically good quantum and locally testable classical LDPC codes, STOC 2022; arXiv:2111.03654. https://arxiv.org/abs/2111.03654
• S. Gu, C. A. Pattison, E. Tang, An efficient decoder for a linear distance quantum LDPC code, STOC 2023; arXiv:2206.06557. https://arxiv.org/abs/2206.06557
• A. Leverrier, G. Zémor, Efficient decoding up to a constant fraction of the code length for asymptotically good quantum codes, SODA 2023; arXiv:2206.07571. https://arxiv.org/abs/2206.07571
• I. Dinur, M.-H. Hsieh, T.-C. Lin, T. Vidick, Good quantum LDPC codes with linear time decoders, arXiv:2206.07750, 2022. https://arxiv.org/abs/2206.07750
• G. Kalachev, P. Panteleev, Two-sided robustly testable codes, arXiv:2206.09973, 2022. https://arxiv.org/abs/2206.09973