Quantum Error Correction

Motivation

The AdS/CFT correspondence relates a theory of quantum gravity in anti-de Sitter space (the bulk) to a quantum field theory without gravity on its boundary (the CFT). A central question is how a local field operator $\phi(x)$ deep in the bulk is represented by boundary operators. Almheiri, Dong and Harlow (JHEP 04 (2015) 163) pointed out a puzzle.

• The bulk operator can be reconstructed on several different boundary regions. For example, it can be reconstructed on $A\cup B$, on $B\cup C$ or on $A\cup C$, but not on any single one of them.
• These reconstructions cannot all be the same CFT operator: an operator commuting with all local operators on a time slice must be trivial.

Their resolution is that the bulk effective theory is a quantum error-correcting code. Bulk operators are logical operators acting on a code subspace of the CFT Hilbert space. Different boundary representations agree only on that subspace, as one logical operator of an erasure-correcting code can be implemented on different subsets of qubits.

The mathematical backbone of that resolution is a finite-dimensional criterion for when a logical operator can be implemented on a given subsystem. This mission formalizes it (Appendix B of the paper), with the examples and corollaries of Section 3.

Timeline.

• 1996–1997: Schumacher and Nielsen characterize correctability by vanishing correlations with a reference system, condition (3.14) (arXiv:quant-ph/9604022). Grassl, Beth and Pellizzari give the matrix-element form (3.19) (arXiv:quant-ph/9610042).
• 1999: Cleve, Gottesman and Lo introduce the three-qutrit code as a quantum secret-sharing scheme (arXiv:quant-ph/9901025).
• 2006: Ryu and Takayanagi propose the holographic entanglement-entropy formula (arXiv:hep-th/0603001).
• 2007: Bény, Kempf and Kribs develop operator-algebra quantum error correction (arXiv:quant-ph/0608071, arXiv:0705.1574), of which the theorem here is a special case.
• 2014–2015: Almheiri, Dong and Harlow recast bulk reconstruction as quantum error correction; Pastawski, Yoshida, Harlow and Preskill build holographic tensor-network codes (arXiv:1503.06237).
• 2016: Dong, Harlow and Wall establish reconstruction in the entanglement wedge (arXiv:1601.05416). Harlow derives the Ryu–Takayanagi formula from operator-algebra error correction (arXiv:1607.03901).

Setting

The physical Hilbert space is a tensor product $\mathcal H = \mathcal H_E\otimes\mathcal H_{\bar E}$ of finite-dimensional spaces. $E$ is the part that may be erased (lost), and $\bar E$ is the part that remains. A code subspace is a subspace $\mathcal H_{\mathcal C}\subseteq\mathcal H$.

An operator $O$ acts within the code subspace if both $O$ and $O^\dagger$ map $\mathcal H_{\mathcal C}$ into itself. Such an operator has a representation on $\bar E$ if there is an operator $O_{\bar E}$ acting only on $\bar E$, that is of the form $\mathbb 1_E\otimes Y$, with

$$O_{\bar E}|\tilde\psi\rangle = O|\tilde\psi\rangle,\qquad O_{\bar E}^\dagger|\tilde\psi\rangle = O^\dagger|\tilde\psi\rangle\qquad\text{for all }|\tilde\psi\rangle\in\mathcal H_{\mathcal C}.$$

Representations on $E$ are defined in the same way, with operators $X\otimes\mathbb 1_{\bar E}$.

The three-qutrit code (Section 3.1) encodes one qutrit into three via

$$|\tilde\imath\rangle = \tfrac{1}{\sqrt3}\textstyle\sum_{a\in\mathbb Z_3}|a,\ a+i,\ a+2i\rangle,$$

that is, $|\tilde 0\rangle = (|000\rangle+|111\rangle+|222\rangle)/\sqrt3$ and so on (Eq. (3.3)).

Formalization targets

Goal: the basic theorem of operator-algebra quantum error correction (Section 3.5, proof in Appendix B)

For an operator $O$ acting within $\mathcal H_{\mathcal C}$,

$$O\ \text{has a representation on }\bar E\iff \langle\tilde\psi'|\,[O,\,X_E\otimes\mathbb 1_{\bar E}]\,|\tilde\psi\rangle = 0\ \ \text{for all } X_E \text{ on } E \text{ and all } |\tilde\psi\rangle,|\tilde\psi'\rangle\in\mathcal H_{\mathcal C}.$$

Milestones (in source order)

1. Section 3.1 (after Eq. (3.3)): for every encoded three-qutrit state, the reduced density matrix of each single qutrit is $\tfrac13\mathbb 1$.
2. Eqs. (3.4)–(3.6): the permutation $U_{12}$ of Eq. (3.6) is unitary, and $(U_{12}\otimes I_3)|\tilde\imath\rangle = |i\rangle\otimes\tfrac1{\sqrt3}(|00\rangle+|11\rangle+|22\rangle)$.
3. Eqs. (3.9)–(3.10): for every single-qutrit operator $O$, the operator $O_{12} = U_{12}^\dagger (O\otimes\mathbb 1) U_{12}$, with $O$ acting on the first qutrit, satisfies $O_{12}|\tilde\imath\rangle = \sum_j O_{ji}|\tilde\jmath\rangle$.
4. Section 3.2, Eqs. (3.19) ⟺ (3.21): the projection of every $X_E$ onto the code subspace is proportional to the identity iff every operator acting within the code subspace has a representation on $\bar E$. The source states, citing the literature, that (3.19) is equivalent to correctability of the erasure of $E$; that equivalence is not formalized.
5. Section 3.5, two-qubit example: on the code spanned by $(|00\rangle+|11\rangle)/\sqrt2$ and $(|01\rangle+|10\rangle)/\sqrt2$, the logical $X$ is realized by the bit flip of either qubit. No operator on the first qubit alone reproduces the logical $Z$ on the code, and every logical operator realizable on the first qubit acts on the code as $a\mathbb 1 + b\bar X$: the code corrects only the subalgebra generated by $\mathbb 1$ and $\bar X$.
6. Section 3.5, algebraic no-cloning: if $O_1$ has a representation on $\bar E$ and $O_2$ has a representation on $E$, then $O_1$ and $O_2$ commute on the code subspace. Consequently, the elements of any family of logical operators that is represented both on $E$ and on $\bar E$ commute pairwise on the code subspace, so a non-abelian algebra cannot be represented on both.

Significance

The result. The goal theorem characterizes, by a checkable commutation condition, which logical operators survive the loss of $E$; milestone 4 is its specialization to full erasure correction. Milestone 6 explains why a non-commuting algebra of bulk operators cannot be represented on two complementary boundary regions at once, so reconstructions of $\phi(x)$ on different regions are distinct operators that agree only on the code subspace. The three-qutrit code models this: every logical operator is realized on any two qutrits, and no single qutrit carries information.

Formalizing it. All statements are proved in the source, or cited there from standard references, and are finite-dimensional. This mission produces machine-checked versions and a reusable vocabulary of code subspaces, logical operators and subsystem representations. That vocabulary is the starting point for formalizing the later results it underlies, in particular the subsystem and operator-algebra theorems of Harlow's derivation of the Ryu–Takayanagi formula (arXiv:1607.03901).

Status honesty. The mathematics is unconditional finite-dimensional linear algebra. The application to AdS/CFT rests on the conjectured duality and on bulk effective field theory, and is context only; none of it enters the hypotheses. The appendix proof is the authors' own, and the theorem is a special case of the results of Bény, Kempf and Kribs. The equivalence of (3.19) with correctability of the erasure (the existence of a recovery unitary, Eqs. (3.14)–(3.18)) is cited in the source from Schumacher–Nielsen and Grassl–Beth–Pellizzari, and is not part of this mission. No machine-checked proof of any of these statements is known. Neither Mathlib nor Physlib (including its quantum-information library) formalizes code subspaces, erasure correction or operator-algebra quantum error correction.

Difficulty

The forward direction of the goal is a direct computation. The converse is an existence statement: an operator $O_{\bar E}=\mathbb 1_E\otimes Y$ has to be produced from a hypothesis that constrains only the matrix elements of $O$ between code states. That hypothesis says nothing about how $O$ acts off the code subspace, and $O$ generally acts nontrivially on $E$. So no candidate for $Y$ can be read off from $O$ itself.

Milestone 4 has the same character in both directions. One direction must produce a representation on $\bar E$ for every operator acting within the code subspace, starting from the scalar condition (3.19), which concerns operators on $E$ alone. The other direction is a non-existence claim about operators on $E$, to be derived from a property quantified over all logical operators.

The explicit-code milestones are finite but involve the irrational normalization $1/\sqrt3$ and a $27$-dimensional space.

Formalization scope

• Representation. Vectors on $\mathcal H_E\otimes\mathcal H_{\bar E}$ are functions on $e\times\bar e$ for finite types $e,\bar e$, with $E$ first. Operators are complex matrices, tensor products are Mathlib's Kronecker product ⊗ₖ, $O^\dagger$ is the conjugate transpose, and $\langle w|u\rangle$ is star w ⬝ᵥ u.
• Code subspace. The code subspace is an arbitrary complex subspace (Submodule ℂ). It is described without a basis: "$\langle\tilde\imath|\cdots|\tilde\jmath\rangle = 0$ for all $i,j$" is stated for all pairs of code vectors, which is equivalent by sesquilinearity.
• Proportionality. Eq. (3.19), $\langle\tilde\imath|X_E|\tilde\jmath\rangle = \delta_{ij}C(X)$, is stated basis-free as $\langle w|X_E v\rangle = c\,\langle w|v\rangle$ for one constant $c$ and all code vectors $v,w$.
• Three-qutrit vectors. These are indexed by $((q_1,q_2),q_3)$. $U_{12}$ is the permutation matrix of the table in Eq. (3.6), and the single-qutrit reduced states are partial traces over the other two qutrits.
• Not trivial. The goal quantifies over every code subspace and every operator acting within it. The zero subspace makes both sides true and is harmless. The examples are fixed concrete codes.
• Not formalized. Cited but not proved in the source: (3.14) with the recovery unitary (3.16)–(3.18), and the bound (3.25). Heuristic: the count (3.22) and the Page-theorem argument after it. Definitions only: quantum secret sharing (Section 3.3), (3.23) and (3.24). Immediate or by symmetry: (3.20), recovery from qutrits 2,3 or 1,3, and the $*$-subalgebra remark after the theorem. Out of scope: Sections 4–5 (the AdS/CFT model, backreaction).
• Infrastructure. A complete development needs lemmas on Kronecker products acting on vectors ((A ⊗ₖ B) *ᵥ v), conjugate transposes of Kronecker products, orthogonal projection onto a Submodule, and partial traces. These are reusable; stand-alone contributions are welcome.

Selected references

• A. Almheiri, X. Dong, D. Harlow, Bulk locality and quantum error correction in AdS/CFT, JHEP 04 (2015) 163. arXiv:1411.7041
• C. Bény, A. Kempf, D. W. Kribs, Generalization of quantum error correction via the Heisenberg picture, Phys. Rev. Lett. 98, 100502 (2007). arXiv:quant-ph/0608071
• C. Bény, A. Kempf, D. W. Kribs, Quantum error correction of observables, Phys. Rev. A 76, 042303 (2007). arXiv:0705.1574
• B. Schumacher, M. A. Nielsen, Quantum data processing and error correction, Phys. Rev. A 54, 2629 (1996). arXiv:quant-ph/9604022
• M. Grassl, T. Beth, T. Pellizzari, Codes for the quantum erasure channel, Phys. Rev. A 56, 33 (1997). arXiv:quant-ph/9610042
• R. Cleve, D. Gottesman, H.-K. Lo, How to share a quantum secret, Phys. Rev. Lett. 83, 648 (1999). arXiv:quant-ph/9901025
• S. Ryu, T. Takayanagi, Holographic derivation of entanglement entropy from AdS/CFT, Phys. Rev. Lett. 96, 181602 (2006). arXiv:hep-th/0603001
• F. Pastawski, B. Yoshida, D. Harlow, J. Preskill, Holographic quantum error-correcting codes: toy models for the bulk/boundary correspondence, JHEP 06 (2015) 149. arXiv:1503.06237
• X. Dong, D. Harlow, A. C. Wall, Reconstruction of bulk operators within the entanglement wedge in gauge-gravity duality, Phys. Rev. Lett. 117, 021601 (2016). arXiv:1601.05416
• D. Harlow, The Ryu–Takayanagi formula from quantum error correction, Commun. Math. Phys. 354, 865 (2017). arXiv:1607.03901

Motivation

Quantum low-density parity-check codes encode quantum information using sparse parity constraints. A standard way to construct them is to translate binary chain complexes into Calderbank--Shor--Steane codes and to combine complexes by tensor product. Homology identifies the logical operators of the resulting code, while the smallest Hamming weight of a nontrivial homology class controls one of its distances. Determining how this distance behaves under a tensor product is therefore a basic structural question, not merely a parameter calculation.

Weilei Zeng and Leonid P. Pryadko studied products in which one factor is an arbitrary finite binary chain complex and the other is the one-complex induced by a binary matrix. Their paper was published as “Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,” Physical Review Letters 122, 230501 (2019). Its main distance result is Eq. (13) in the arXiv version: for this particular tensor factor, the usual product upper bound is always exact. The result extends the familiar two-complex setting of quantum hypergraph-product codes to the local structure occurring in complexes of any dimension.

Setting

A based binary chain complex consists of finite-dimensional vector spaces $A_i$ over $\mathbb F_2$, each equipped with a specified coordinate basis, and linear boundary maps

$$\cdots\longrightarrow A_{i+1}\xrightarrow{\partial_{i+1}}A_i \xrightarrow{\partial_i}A_{i-1}\longrightarrow\cdots$$

such that $\partial_i\partial_{i+1}=0$. Its degree-$i$ homology is $H_i(\mathcal A)=\ker\partial_i/\operatorname{im}\partial_{i+1}$. The homological distance is measured in the chosen basis:

$$d_i(\mathcal A)= \min\{\operatorname{wt}(x):x\in\ker\partial_i\setminus \operatorname{im}\partial_{i+1}\}.$$

Following the paper, the minimum of an empty set is $\infty$. Thus $d_i(\mathcal A)=\infty$ when $H_i(\mathcal A)$ is trivial.

The endpoint convention is also the one stated explicitly after Eq. (1). For an $m$-complex, $\partial_0:A_0\to\{0\}$ is the zero $0\times n_0$ matrix and $\partial_{m+1}:\{0\}\to A_m$ is the zero $n_m\times0$ matrix. Consequently

$$d_0(\mathcal A)=\min\{\operatorname{wt}(x): x\in A_0\setminus\operatorname{im}\partial_1\}$$

and

$$d_m(\mathcal A)=\min\{\operatorname{wt}(x): 0\ne x\in\ker\partial_m\}.$$

For an $r\times c$ binary matrix $P$, the one-complex $\mathcal K(P)$ has $\mathbb F_2^c$ in degree one, $\mathbb F_2^r$ in degree zero, and boundary $P$. Its two distances are

$$d_1(\mathcal K(P))= \min\{\operatorname{wt}(x):Px=0,\ x\ne0\}$$

and

$$d_0(\mathcal K(P))= \min\{\operatorname{wt}(y):y\notin\operatorname{im}P\}.$$

In particular, $d_0=1$ unless $P$ has full row rank, in which case $d_0=\infty$. The degree-$j$ chain group of $\mathcal A\times\mathcal K(P)$ is

$$(A_j\otimes\mathbb F_2^r)\oplus (A_{j-1}\otimes\mathbb F_2^c),$$

with the standard tensor-product boundary. Over $\mathbb F_2$ the usual sign in that boundary has no effect.

Formalization targets

Tensor-product upper bound for arbitrary complexes

The first milestone is Eq. (11) for two arbitrary finite-length based binary chain complexes:

$$d_j(\mathcal A\times\mathcal B)\le \min_i d_i(\mathcal A)d_{j-i}(\mathcal B).$$

Rank-sensitive lower bound

Let $u=\operatorname{rank}P$ and $\delta=d_1(\mathcal K(P))$. The second milestone is Theorem 1, including both of its cases:

$$u<r\Longrightarrow d_j(\mathcal A\times\mathcal K(P))\ge \min\!\left(d_j(\mathcal A),d_{j-1}(\mathcal A)\delta\right),$$

and

$$u=r\Longrightarrow d_j(\mathcal A\times\mathcal K(P))\ge d_{j-1}(\mathcal A)\delta.$$

Exact distance with a one-complex

The goal is Eq. (13):

$$d_j(\mathcal A\times\mathcal K(P))= \min\!\left( d_{j-1}(\mathcal A)d_1(\mathcal K(P)), d_j(\mathcal A)d_0(\mathcal K(P)) \right).$$

No full-rank hypothesis is imposed on $P$.

Significance

The equality determines the product distance exactly from four component distances. General tensor-product arguments immediately provide the upper bound, but an exact formula requires ruling out lower-weight homology classes that mix the two direct-sum blocks. Once established, the formula can be applied repeatedly to tensor products of one-complexes, which is the step used in the paper to obtain higher-dimensional quantum hypergraph-product code families and to compute their distances.

For formalization, the mission contributes reusable definitions of finite based binary chain data, homological distance valued in $\mathbb N\cup\{\infty\}$, the one-complex of a binary matrix, and the relevant tensor-product boundary maps. Mathlib contains Hamming weight and general homological-algebra infrastructure, while QECLean contains a closely related based length-three homological-code interface. Neither the selected Mathlib environment nor the inspected QECLean development currently supplies this rank-sensitive exact distance theorem.

Difficulty

The central issue is that Hamming weight depends on the chosen bases and is not preserved by arbitrary homological isomorphisms. A Künneth isomorphism describes the product homology and readily produces low-weight representatives, which is enough for the upper bound, but it does not by itself exclude a still lighter representative obtained by cancellation between the two tensor blocks. The lower bound must also remain valid at the endpoints of the complex and in singular cases where one or more homology groups vanish and the relevant distance is $\infty$.

The theorem cannot be reduced to a dimension calculation. It must reason about supports and Hamming weights of based representatives while respecting the quotient by boundaries, and it must cover both $\operatorname{rank}P<r$ and $\operatorname{rank}P=r$.

Formalization scope

The Lean development works over ZMod 2. A finite basis in degree $i$ is represented by Fin (dimension i), and a chain group is the function space from that coordinate type to ZMod 2. BasedBinaryChainComplex stores the dimension and boundary in every nonnegative degree, the chain condition, and a finite length above which all dimensions are zero. Thus the first milestone quantifies over genuinely arbitrary finite lengths for both $\mathcal A$ and $\mathcal B$, rather than over a local window or a one-complex specialization. If the stored length is $m$, the zero-dimensional source in degree $m+1$ makes $\partial_{m+1}:\{0\}\to A_m$ the unique zero map, just as the zero-dimensional target below degree zero makes $\partial_0:A_0\to\{0\}$ the unique zero map. Hence both singular endpoint cases in Eqs. (1) and (4) are represented directly.

Distances use WithTop ℕ. Their definitions are actual minima of Hamming weights of nontrivial representatives, with ⊤ produced by the empty-set case; infinite distance is not an extra hypothesis or a separately hard-coded branch. Coordinate types may be empty, which covers missing endpoint blocks. The binary matrix $P$ is represented as a linear map between two finite based function spaces. Its row and column coordinate types need not be nonempty, and no injectivity or surjectivity assumption is added.

The degree-$j$ product group is indexed by the disjoint union of all coordinate products $A_i\times B_{j-i}$ for $0\le i\le j$. Consequently its Hamming norm is the sum of the weights of all tensor-degree blocks. The product boundary is the standard signed tensor boundary; its sign disappears over $\mathbb F_2$. A formal proof verifies that every pair of consecutive product boundaries composes to zero; the cancellation of the two mixed terms uses characteristic two. Thus the product distance is taken from an actual chain complex, rather than from unrelated adjacent linear maps. A basis-free tensor product or an abstract homology group alone is insufficient for the target, because either would discard the weight data on which the statement depends. The mission does not formalize the asymptotic code-family construction later in the paper, the transposed cohomological distance, or the CSS-code parameter translation. Those are natural downstream missions; they should reuse rather than alter the present based-chain definitions.

Selected references

• Weilei Zeng and Leonid P. Pryadko, “Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,” Physical Review Letters 122, 230501 (2019). arXiv:1810.01519.
• Benjamin Audoux and Alain Couvreur, “On Tensor Products of CSS Codes,” arXiv:1512.07081 (2015), especially Proposition 1.13 and Corollary 2.14 as cited by Zeng--Pryadko.
• Jean-Pierre Tillich and Gilles 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 (2014), 1193--1202.