Quantum Error Correction

Motivation

A quantum memory stores logical qubits in many physical qubits so that errors can be detected and corrected. The overhead of doing so, measured by how many physical qubits are spent per logical qubit at a given error-correcting power, is one of the main costs of fault-tolerant quantum computation. Bivariate-bicycle (BB) codes are currently the leading low-overhead family: the gross code $[[144,12,12]]$ of Bravyi et al. (Nature, 2024) stores 12 logical qubits at distance 12 using 144 data qubits, roughly a tenth of the overhead of a surface code with the same distance, and it is the basis of a published hardware roadmap. The search for higher-rate members of the family is active, and the claims made in it are claims about the exact distance of explicit finite codes. These are finite but very large computations, and they are rarely checked independently.

Timeline.

• 2004 — MacKay, Mitchison and McFadden introduce bicycle codes: CSS codes built from a pair of circulant matrices.
• 2013 — Kovalev and Pryadko generalize the construction to commuting pairs of group-algebra elements (generalized bicycle codes).
• 2024 — Bravyi, Cross, Gambetta, Maslov, Rall and Yoder define BB codes over $\mathbb Z_l\times\mathbb Z_m$ and give the ladder $[[72,12,6]]$, $[[90,8,10]]$, $[[108,8,10]]$, $[[144,12,12]]$, $[[288,12,18]]$, with $[[360,12,\le 24]]$ left with only an upper bound.
• 2026 — An evolutionary search by Cruz-Benito et al. (arXiv:2606.02418) reports $[[288,16,12]]$ as its best indecomposable weight-6 code at distance 12.
• 2026 — Daugherty, Ryan and Ward give two new $[[336,20,12]]$ codes and a new $[[360,24,12]]$ code. They certify the exact distances of the whole ladder, establish $d=24$ for $[[360,12]]$, and show by enumeration that no connected three-term weight-6 BB code with $n\le 360$ and $k\ge 20$ has distance 13 or more.

Setting

Fix positive integers $l,m$ and let $G=\mathbb Z_l\times\mathbb Z_m$. The monomial $x^iy^j$ of the ring $\mathbb F_2[x,y]/(x^l-1,\,y^m-1)$ is identified with $(i,j)\in G$. A polynomial $P$ with coefficients in $\mathbb F_2$ is identified with its support, the finite set of monomials with coefficient $1$. The circulant of $P$ is the $G\times G$ binary matrix with a $1$ in row $g$, column $h$ exactly when $h-g\in P$.

Given two polynomials $A,B$, the BB code $\mathrm{BB}(A,B)$ acts on $n=2lm$ qubits, arranged in two blocks indexed by $G$. Its check matrices are

$$H_X=[\,A\mid B\,],\qquad H_Z=[\,B^{\mathsf T}\mid A^{\mathsf T}\,],$$

where $A$ and $B$ also denote their circulants. Because $G$ is abelian, $H_XH_Z^{\mathsf T}=AB+BA=0$ over $\mathbb F_2$, so this is a CSS code. Its parameters are:

1. the number of logical qubits $k=n-\operatorname{rank}H_X-\operatorname{rank}H_Z$, with ranks over $\mathbb F_2$;
2. the Z-distance $d_Z$, the least Hamming weight of a vector $v\in\mathbb F_2^n$ with $H_Xv=0$ and $v\notin\operatorname{row}(H_Z)$ (a nontrivial Z-logical);
3. the X-distance $d_X$, defined dually: $H_Zv=0$ and $v\notin\operatorname{row}(H_X)$.

The code is $[[n,k,d]]$ when $d_X=d_Z=d$. Each check of a code built from two three-term polynomials touches six qubits (weight 6). The Tanner graph joins each qubit to the X- and Z-checks acting on it, and the code is connected when this graph is connected.

Formalization targets

Goal: the three new codes

$$\mathrm{BB}_{\mathbb Z_2\times\mathbb Z_{84}}\!\left(1+y+xy^{5},\;1+y^{4}+y^{62}\right)=[[336,20,12]],$$ $$\mathrm{BB}_{\mathbb Z_2\times\mathbb Z_{84}}\!\left(1+y+xy^{5},\;1+y^{20}+y^{46}\right)=[[336,20,12]],$$ $$\mathrm{BB}_{\mathbb Z_6\times\mathbb Z_{30}}\!\left(1+y+xy^{2},\;1+y^{8}+x^{2}y^{16}\right)=[[360,24,12]],$$

each with $d_X=d_Z=12$ (Table 9 of the source). Each new code is also a milestone on its own.

Milestones

• Lemma 1 (minimality). In any parity system, no nonempty proper subset of a minimum-weight logical is even on every check.
• Table 3, the certified ladder. $[[72,12,6]]$, $[[90,8,10]]$, $[[108,8,10]]$, $[[144,12,12]]$, $[[288,12,18]]$ and $[[360,12,24]]$, all with $d_X=d_Z$, for the polynomials of Bravyi et al.
• Section 6, the weight-6 envelope. Every connected BB code built from two three-term polynomials with $n\le 360$ and $k\ge 20$ has a nontrivial X- or Z-logical of weight at most 12. In words, none has distance 13 or more.

Significance

The result. The new codes encode 25% and 50% more logical qubits at distance 12 than the best weight-6 code reported by evolutionary search, with figures of merit $kd^2/n$ of 8.57 and 9.60. The ladder distances turn published values, several of them previously supported only by heuristic searches or upper bounds, into exact statements. In particular $d([[360,12]])=24$ settles an upper bound left open by Bravyi et al. The envelope statement is a negative result: within this family and size range, distance 12 is the ceiling at $k\ge 20$.

Formalizing it. In the source, each lower bound on a distance is a DRAT refutation or a replayable proof tree, checked by external programs. Only the pruning lemma (Lemma 1) has a machine-checked proof, in Lean 4. A complete formalization would make the code parameters kernel-checked facts about explicit Mathlib objects, independent of every external checker. Upper bounds on distance and the values of $k$ are finite linear-algebra facts. Lower bounds are exhaustive statements over $\binom{n}{w}$-sized spaces and are the core of the work.

Difficulty

The upper bound $d\le 12$ needs one explicit weight-12 logical together with a proof that it lies outside the opposite row space. The lower bound $d\ge 12$ asks that no nontrivial logical of weight at most 11 exist among roughly $\binom{336}{11}\approx 10^{19}$ candidate supports. Direct enumeration is out of reach. A SAT encoding with a cardinality constraint is several orders of magnitude slower than the source's pruned search, and the resulting proof objects are large: hundreds of megabytes for the larger ladder codes. Kernel-checking such certificates, or finding structure that avoids them, is the central difficulty. Computing $k$ also requires an $\mathbb F_2$-rank of matrices with up to 180 rows and 360 columns, and Mathlib's Matrix.rank is not computable by decide. The envelope statement additionally quantifies over 971 group shapes and every pair of three-term polynomials on each.

Formalization scope

All objects are in the definition file BBCode_Setting. $G$ is ZMod l × ZMod m, and a polynomial is a Finset of monomials, which makes it a set of distinct terms. The circulant has entry 1 at $(g,h)$ iff $h-g\in P$. Qubits are G ⊕ G (left and right blocks). $H_X$ is Matrix.fromCols (circulant A) (circulant B) and $H_Z$ is Matrix.fromCols (circulant B)ᵀ (circulant A)ᵀ, over ZMod 2. The row space is the ZMod 2-span of the rows, and the weight counts nonzero coordinates. NumLogical A B k states $\operatorname{rank}H_X+\operatorname{rank}H_Z+k=n$ additively, avoiding truncated subtraction. HasZDistance A B d requires both a nontrivial Z-logical of weight exactly $d$ and the lower bound for every nontrivial Z-logical, so a code without logicals cannot satisfy it vacuously. IsCode A B n k d bundles $n=2lm$, $k$ and both distances.

The envelope quantifies over all $l,m\ge 1$ with $2lm\le 360$. The source enumerates 961 shapes; the 10 it omits ($lm\le 5$) cannot have $k\ge 20$, so the two ranges are equivalent.

Reusable infrastructure includes computable $\mathbb F_2$ rank certificates (explicit row-echelon or basis witnesses), a verified checker for DRAT or proof-tree certificates, and symmetry lemmas for group translations acting on BB codes. Contributions of any of these, of individual sectors ($d_X$ or $d_Z$ separately), or of upper and lower bounds as separate lemmas are welcome.

Selected references

• S. Bravyi, A. W. Cross, J. M. Gambetta, D. Maslov, P. Rall, T. J. Yoder, High-threshold and low-overhead fault-tolerant quantum memory, Nature 627, 778–782, 2024. https://doi.org/10.1038/s41586-024-07107-7 (arXiv: https://arxiv.org/abs/2308.07915)
• B. W. Daugherty, S. Ryan, G. Ward, New distance-12 bivariate-bicycle codes with 20 and 24 logical qubits: an exhaustive classification and checkable distances to 360 qubits, certificate release v1.0.0, Zenodo, 2026. https://doi.org/10.5281/zenodo.23382175
• D. J. C. MacKay, G. Mitchison, P. L. McFadden, Sparse-graph codes for quantum error correction, IEEE Trans. Inf. Theory 50(10), 2315–2330, 2004. https://arxiv.org/abs/quant-ph/0304161
• A. A. Kovalev, L. P. Pryadko, Quantum Kronecker sum-product low-density parity-check codes with finite rate, Phys. Rev. A 88, 012311, 2013. https://arxiv.org/abs/1212.6703
• J. Cruz-Benito et al., evolutionary search for bivariate-bicycle codes, arXiv:2606.02418, 2026. https://arxiv.org/abs/2606.02418

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

A quantum computer manipulates superpositions of many degrees of freedom, and every gate it applies is imperfect. Before 1996 it was widely argued that this fragility is fatal: the accuracy demanded of each elementary operation appeared to grow with the length of the computation, so that arbitrarily long computations would require arbitrarily perfect hardware. The discovery of quantum error-correcting codes, of fault tolerant syndrome extraction, and of transversally encoded operations changed that picture, but the first fault tolerant schemes still required the error per operation to shrink as the computation grew.

Knill, Laflamme and Zurek, Resilient Quantum Computation: Error Models and Thresholds (arXiv:quant-ph/9702058), together with the independent work of Kitaev and of Aharonov and Ben-Or, removed that requirement: they exhibited a fixed threshold value such that any physical error rate below it permits arbitrarily accurate encoded computation, at an overhead that is only polylogarithmic in the length of the computation. Their paper is also the one that pushes past independent stochastic noise: its thresholds are proved for quasi-independent error models, which accommodate coherent over-rotation and weak residual couplings between neighbouring qubits.

This mission formalizes the quantitative engine of that paper: the concatenation recursion, the error-model bounds it is applied to, the threshold it produces, and the resulting overhead.

Setting

Fix a physical implementation in which each gate, state preparation and idle memory step carries an error location. A noisy network with error locations indexed by a finite set $\mathrm{locs}$ is described through an error expansion; each summand fails at a set of locations, and the model constrains how probable simultaneous failures are.

Write $\mu$ for the underlying probability measure and $F_i$ for the event that location $i$ has failed. Two models from Section I.B of the paper are used here.

• Quasi-independent stochastic model with error probability $p$: for every set $S \subseteq \mathrm{locs}$ of error locations,

$$\mu\Big(\bigcap_{i \in S} F_i\Big) \le p^{|S|}.$$

• Quasi-independent monotonic model with constant $C$ and parameter $p$: the same quantity is bounded by $C\,p^{|S|}$.

The fault tolerant construction of Section I turns physical qubits into encoded qubits: each encoded gate is a transversal operation preceded by fault tolerant recovery networks built from the $7$-qubit Steane code. The analysis of Section II declares an encoded gate failed according to an explicit combinatorial rule, and shows that a failure requires two failures among a set of $f$ minimal pairs of physical error locations. Consequently one level of encoding maps a failure parameter $p$ to $f p^{2}$.

Iterating this reduction is concatenation. Define the level-$h$ failure parameter by

$$E_0 = p, \qquad E_{h+1} = f\,E_h^{2},$$

written $E_h = \texttt{levelError}\,f\,p\,h$ in the Lean development. Let $K$ bound the number of qubits and time steps at the level below that are consumed by one encoded gate, so that one computational gate at level $h$ costs $K^{h}$ physical resources.

Formalization targets

Goal — threshold theorem with polylogarithmic overhead

For $f \ge 1$, $K \ge 2$, $0 \le p < 1/f$, and every gate count $n$ and target failure probability $q$ with $0 < q < n$, there exists a level $h$ with

$$n\,E_h < q \qquad\text{and}\qquad K^{h} \;\le\; K^{2}\Big(\max\Big(1,\ \frac{\log(n/q)}{\log\big(1/(fp)\big)}\Big)\Big)^{\log_2 K}.$$

The first clause is resilience: a computation of $n$ encoded gates can be made to fail with probability below any prescribed $q$. The second is the cost: the overhead per computational gate is polylogarithmic in $n/q$, with exponent $\log_2 K$. The threshold itself is the hypothesis $p < 1/f$; no numerical value is hard-coded, so the statement survives any improvement of the paper's count $f \le 337195$ and of the resulting bounds $3.0 \times 10^{-6}$ and $1.3 \times 10^{-6}$.

Supporting targets

The milestone list covers the closed form $E_h = f^{2^{h}-1} p^{2^{h}}$ of the concatenation recursion and its threshold form $E_h = (fp)^{2^{h}}/f$; convergence $E_h \to 0$ below threshold; the failure bounds $|\mathrm{locs}|\,p$ and $C\,|\mathrm{locs}|\,p$ for a network under the two error models; the criterion $2^{h} > \log(n/q)/\log(1/(fp))$ under which $n (fp)^{2^{h}} < q$; and the overhead estimate $K^{\lceil \log_2 L\rceil} \le K L^{\log_2 K}$.

Significance

The threshold theorem is the reason large-scale quantum computation is regarded as a physically meaningful goal rather than an idealization: it converts an engineering requirement that scales with the problem size into a fixed, size-independent accuracy target, and it fixes the currency — threshold value and overhead exponent — in which every later architecture is compared. The quasi-independent models matter separately: they show the conclusion does not depend on noise being stochastic, which is what rules out the objection that coherent over-rotations invalidate the stochastic analysis.

The paper's own argument is a physics-style derivation: a circuit-level construction, a combinatorial count of failure-inducing pairs of error locations, and a recursion. This mission formalizes the recursion, the probabilistic bounds and the resulting threshold and overhead statements. It does not formalize the circuit-level content — the $7$-qubit code, the cat-state syndrome extraction networks, transversality, or the count $f \le 337195$ itself; these enter the formal statements as the parameters $f$ and $K$. No machine-checked proof of the full threshold theorem, in the sense of a verified fault tolerant circuit construction, is known to the author of this proposal; formalizing the quantitative layer is a prerequisite for one.

Difficulty

The obvious route to "errors vanish under concatenation" is to iterate the bound $p \mapsto f p^{2}$ and observe the doubly exponential decay. That step is the easy half, and the milestone list makes it explicit. What the naive argument silently assumes is exactly what Section II must establish: that the level-$(h+1)$ failure events again obey a quasi-independent bound, with $k$ simultaneous encoded failures bounded by $(f p^{2})^{k}$ rather than merely each single failure bounded by $f p^{2}$. This is why the paper's failure declaration is defined backwards in time and demands disjoint pairs of contributing locations. A formalization that bounds only single-gate failure probabilities cannot close the induction.

The second difficulty is bookkeeping at the edges: the recursion is stated for a failure parameter that is a probability in one model and an operator strength in the other, and the overhead bound involves a real exponent $\log_2 K$ and a ceiling, whose interaction with the degenerate cases $p = 0$ and $n \le q$ has to be handled rather than assumed away.

Formalization scope

All parameters are real numbers: $f, p, q, K, C \in \mathbb{R}$, and the gate count $n$ is a natural number cast to $\mathbb{R}$. levelError is defined by recursion on the level and is total, so it is meaningful for every real $f, p$; the threshold hypothesis appears explicitly as $p < 1/f$ where it is needed.

The two error models are predicates on a measure $\mu$ on a measurable space, a Finset of error locations, and a family of failure events, with values in ENNReal; they quantify over all subsets $S$ of the location set, matching the paper's "at a given $k$ many error locations". The network failure bounds are stated for $\mu\big(\bigcup_{i} F_i\big)$, the probability that some location fails.

The goal is not vacuous: the hypotheses $f \ge 1$, $K \ge 2$, $0 \le p < 1/f$, $0 < q < n$ are simultaneously satisfiable (for instance $f = 1$, $K = 2$, $p = 10^{-6}$, $n = 10^{6}$, $q = 1/2$), and the conclusion asserts a strict inequality together with a quantitative overhead bound, so it cannot be discharged by a degenerate reading. Degenerate inputs are inside the statement rather than excluded: $p = 0$, and the case $\log(n/q)/\log(1/(fp)) \le 1$, are covered by the $\max$ and must be handled.

A complete development needs only Mathlib's real analysis (Real.log, Real.logb, Real.rpow, Nat.ceil) and the measure-theoretic union bound; nothing quantum is required by the formal statements. Contributions strengthening the milestone list towards the circuit level — a formal model of error locations in a network, of the induced next-level error model, or of stabilizer-code recovery — are welcome as further targets.

Selected references

• E. Knill, R. Laflamme, W. H. Zurek, Resilient Quantum Computation: Error Models and Thresholds, arXiv:quant-ph/9702058 (1997), https://arxiv.org/abs/quant-ph/9702058
• A. M. Steane, Error Correcting Codes in Quantum Theory, Physical Review Letters 77, 793 (1996), https://doi.org/10.1103/PhysRevLett.77.793
• P. W. Shor, Fault-tolerant quantum computation, Proceedings of the 37th Symposium on Foundations of Computer Science (1996), https://arxiv.org/abs/quant-ph/9605011
• D. Aharonov, M. Ben-Or, Fault-Tolerant Quantum Computation With Constant Error, arXiv:quant-ph/9611025 (1996), https://arxiv.org/abs/quant-ph/9611025
• A. Yu. Kitaev, Quantum computations: algorithms and error correction, Russian Mathematical Surveys 52, 1191 (1997), https://doi.org/10.1070/RM1997v052n06ABEH002155

Motivation

Quantum computations are performed on physical devices whose elementary operations are never exact: every gate, every idle qubit, every time step is subject to decoherence, damping and systematic inaccuracy. Without protection these errors accumulate and destroy the computation. In 1997 Dorit Aharonov and Michael Ben-Or proved that this can be overcome: as long as the error rate — the probability, per location per time step, that a fault occurs — is below a fixed positive threshold, an arbitrary quantum circuit can be simulated reliably with only polylogarithmic overhead (arXiv:quant-ph/9906129). This threshold theorem is the reason large-scale quantum computing is regarded as physically possible in principle, and the number it produces is the target every hardware programme is measured against.

The engine of the proof is not quantum mechanical but combinatorial. A circuit is encoded, then the encoded circuit is encoded again, $r$ times over. The locations of the resulting circuit are organised into a tree of nested rectangles, and the computation survives precisely when the set of faulty locations is sparse in a recursive sense. The mission formalizes that engine: the recursive sparseness calculus of §7.4–7.6 and §8.2 of the paper, which converts a constant error rate below the threshold into a doubly exponentially small failure probability.

Setting

Fix two natural numbers: $A$, the number of locations in a rectangle, and $k$, the number of faulty sub-rectangles a rectangle tolerates (in the paper $k=\lfloor d/l\rfloor$, where $d$ is the number of errors the code corrects and $l$ is the spread of a fault). A $0$-rectangle is a single location of the circuit, and an $(r+1)$-rectangle consists of $A$ many $r$-rectangles. A fault pattern of an $r$-rectangle records, for each of its $A^{r}$ locations, whether a fault occurred there.

Following Definition 18 of the paper, a fault pattern is $(r,k)$-sparse by recursion on $r$: at level $0$ it is sparse when the location carries no fault; at level $r+1$ it is sparse when at most $k$ of the $A$ constituent $r$-rectangles carry a pattern that is not $(r,k)$-sparse. Under independent probabilistic noise of rate $\eta$ each location is faulty with probability $\eta$, independently; write $P(r)$ for the probability that the pattern of an $r$-rectangle is $(r,k)$-sparse, and $1-P(r)$ for the probability that it is not.

Two thresholds appear. The threshold condition for probabilistic noise (Definition 19) is

$$\binom{A}{k+1}\,\eta^{k+1} < \eta ,$$

and the threshold condition for general noise (Definition 21) is

$$e\binom{A}{k+1}(2\eta)^{k+1} < 2\eta .$$

The corresponding thresholds are $\eta_c=\binom{A}{k+1}^{-1/k}$ and $\eta_c'=\tfrac12\bigl(e\binom{A}{k+1}\bigr)^{-1/k}$: every positive $\eta$ below them satisfies the respective condition.

Target

The goal is the quantitative core of Theorem 10. Below the threshold there are constants $C,c>0$ such that for every circuit size $v\ge 1$ and every accuracy $0<\varepsilon<1$ some recursion depth $r$ satisfies both

$$v\cdot\bigl(1-P(r)\bigr) < \varepsilon \qquad\text{and}\qquad A^{r} \le C\Bigl(1+\log\frac{v}{\varepsilon}\Bigr)^{c}.$$

The first inequality says that, over all $v$ rectangles of the simulated circuit, the probability that any of them carries a non-sparse fault pattern is below $\varepsilon$; the second says that the overhead per simulated location, $A^{r}$, is polylogarithmic in $v/\varepsilon$ — the cost claimed in Theorem 10.

The milestones build up to it: the two threshold conditions hold below the respective thresholds, the exponent gap $\delta$ of equation 7.5 exists, the base case $P(0)=1-\eta$, the union-bound recursion $1-P(r+1)\le\binom{A}{k+1}(1-P(r))^{k+1}$, Lemma 10 itself ($P(r)\ge 1-\eta^{(1+\delta)^r}$), and the analogous recursion 8.8–8.10 governing the bad part in the general-noise analysis.

Significance

Lemma 10 is where a constant error rate becomes a vanishing one. Each level of concatenation only has to improve reliability slightly, because the improvement compounds doubly exponentially in the number of levels; this is exactly why constant-rate noise can be tolerated while Shor's earlier scheme needed a polylogarithmically small rate. The same recursion, with $2\eta$ in place of $\eta$ and an extra factor of $e$, controls the trace norm of the bad part of the fault-path expansion in the general-noise model (§8.2), which is how the result is extended from probabilistic errors to decoherence, damping and systematic inaccuracy.

Formalizing this part of the paper yields a reusable, model-independent statement: nothing in the milestones mentions density matrices, so the sparseness calculus can later be plugged into a formal model of noisy quantum circuits, or reused for classical concatenated fault tolerance. What this mission does not do is formalize the circuit-level statement of Theorem 10 — that requires a full Lean model of quantum circuits with mixed states, fault-tolerant procedures, and the code constructions of §3–§6, and is deliberately out of scope here.

Difficulty

The obvious approach — bound the failure probability by a union bound over all fault sets of size $k+1$ and iterate — is exactly right, but the iteration is where the work is. The recursion $q_{r+1}\le\binom{A}{k+1}q_r^{k+1}$ only produces the doubly exponential decay $\eta^{(1+\delta)^r}$ once the threshold condition is converted into the strict exponent gap $\delta$ of equation 7.5, and the induction has to keep $q_r\le\eta$ alive to reuse that gap at every level. In the general-noise recursion there is a second trap: the factor $(1+b_r)^{A-k-1}$ exceeds $1$, so the recursion is not contracting termwise, and one needs $2\eta A\le 1$ to bound it by $e$.

On the probabilistic side, the statements are about a genuine product distribution on an exponentially large sample space, not a recursively defined real number: the union-bound step must be carried out over the actual set of fault patterns, where independence across the $A$ sub-rectangles is what makes the product bound valid.

Formalization scope

Fault patterns are a type defined by recursion on the level: $\mathrm{FaultPattern}(A,0)$ is the booleans and $\mathrm{FaultPattern}(A,r+1)$ is the functions from the $A$ sub-rectangles to $\mathrm{FaultPattern}(A,r)$; every level is a finite type with decidable equality. Sparseness is a decidable predicate following Definition 18 verbatim. The noise distribution is given by the weight of a pattern, the product over all locations of $\eta$ (faulty) or $1-\eta$ (clean), and the sparseness probability is the sum of these weights over the sparse patterns — an honest finite product measure, so no hypothesis $0\le\eta\le1$ is built into the definitions and each statement carries the range hypotheses it needs.

Two conventions are worth flagging. First, the thresholds are formalized as $\binom{A}{k+1}^{-1/k}$ and $\tfrac12(e\binom{A}{k+1})^{-1/k}$; the paper prints the exponent as $-k$ in equations 7.4 and 8.6, which is inconsistent with its own threshold conditions 7.3 and 8.5, and $-1/k$ is the exponent for which the paper's claim "any $\eta<\eta_c$ satisfies the threshold condition" is true. Second, Lemma 10 is stated with $\ge$ rather than the paper's strict $>$, because at $r=0$ the two sides are equal.

Nothing here is vacuous: all hypotheses are satisfiable — for instance $A=7$, $k=1$, $\eta=10^{-3}$ satisfies every hypothesis of the goal — and the goal quantifies over all circuit sizes and all accuracies, so it cannot be discharged by a degenerate choice. A complete development needs only real analysis, finite sums and binomial counting from Mathlib. Contributions that generalise the branching factor to a per-rectangle bound $A_i\le A$, or that connect the calculus to a formal model of noisy circuits, are welcome.

Selected references

• Dorit Aharonov and Michael Ben-Or, Fault-Tolerant Quantum Computation With Constant Error Rate, arXiv:quant-ph/9906129 (1999); preliminary version in Proc. 29th ACM STOC (1997). https://arxiv.org/abs/quant-ph/9906129
• Peter W. Shor, Fault-tolerant quantum computation, Proc. 37th FOCS (1996). https://arxiv.org/abs/quant-ph/9605011
• Dorit Aharonov, Alexei Kitaev and Noam Nisan, Quantum circuits with mixed states, Proc. 30th ACM STOC (1998). https://arxiv.org/abs/quant-ph/9806029

Background and main question

The tensor product of chain complexes is a basic construction in homological algebra and in the theory of quantum CSS codes. If $A$ and $B$ are finite based chain complexes over a finite field, their tensor product is graded by total degree,

$$(A\otimes B)_j=\bigoplus_{i=0}^{j} A_i\otimes B_{j-i}.$$

Each complex carries a basis-dependent homological distance: $d_j(A)$ is the least Hamming weight of a degree-$j$ cycle that is not a boundary, with $d_j(A)=\infty$ when the degree-$j$ homology vanishes. A natural candidate for the distance of the tensor product is therefore

$$m_j(A,B)=\min_{0\le i\le j} d_i(A)d_{j-i}(B).$$

Every nonzero pair of homology classes in complementary degrees gives a pure-tensor class of the corresponding product weight, so one always has $d_j(A\otimes B)\le m_j(A,B)$. The substantive question is whether this upper bound is always sharp.

In the preprint Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates, posted in 2018 and subsequently published in Physical Review Letters, Zeng and Pryadko proved that the bound is sharp when one factor is a binary one-complex. Their exact formula is Eq. (13) of the arXiv version and is the capstone theorem of the Prove2Me mission Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates. The present formalization is a direct sequel: it retains the same definitions and degree conventions while examining what happens when the one-complex restriction is removed.

Zeng and Pryadko later considered arbitrary finite chain complexes over arbitrary finite fields in Minimal distances for certain quantum product codes and tensor products of chain complexes, published in 2020. In the corresponding arXiv preprint, Conjecture 18 asserts the unrestricted equality

$$d_j(A\otimes B)=m_j(A,B).$$

The conjecture is appealing because it would make tensor-product distance completely compositional: the degreewise distances of the two factors would determine the distance of their product. The obstruction is that a homology class in $A\otimes B$ need not have a minimum-weight representative supported in a single bidegree. A representative spread across several summands of the total complex can be lighter than every pure-tensor representative. The purpose of this formalization is to turn that observation into a concrete, machine-checked counterexample to Conjecture 18 while preserving the valid one-complex theorem as a sharply delimited special case.

The counterexample mechanism

The common foundation is recorded in the Prove2Me entry Based binary chain complexes and homological distance. In particular, the boundary in degree $j$ is a map $\partial_j:A_j\to A_{j-1}$, and

$$d_j(A)=\inf\{\operatorname{wt}(x):x\in\ker\partial_j,\ x\notin\operatorname{im}\partial_{j+1}\}.$$

The one-complex result is separately available as Eq. (13) — Exact distance with a one-complex. The construction below uses exactly the same notion of distance, but both tensor factors are genuine three-term complexes.

Begin with binary CSS check maps

$$H_X:\mathbb F_2^n\longrightarrow\mathbb F_2^{r_X}, \qquad H_Z:\mathbb F_2^n\longrightarrow\mathbb F_2^{r_Z},$$

assumed surjective and satisfying $H_XH_Z^T=H_ZH_X^T=0$. Suppose there are logical vectors $x,z\in\mathbb F_2^n$ such that

$$H_Zx=0,\qquad H_Xz=0,\qquad x\cdot z=1.$$

The check maps determine two dual three-term complexes

$$A:\quad \mathbb F_2^{r_X}\xleftarrow{H_X}\mathbb F_2^n \xleftarrow{H_Z^T}\mathbb F_2^{r_Z}, \qquad B:\quad \mathbb F_2^{r_Z}\xleftarrow{H_Z}\mathbb F_2^n \xleftarrow{H_X^T}\mathbb F_2^{r_X}.$$

Their degree-two tensor space has three bidegree summands, corresponding to $(2,0)$, $(1,1)$, and $(0,2)$. Under the natural matrix identifications, consider the element whose three blocks are

$$(I_{r_Z},I_n,I_{r_X}).$$

The CSS orthogonality relations make this element a cycle. Its pairing with the chosen logical vectors certifies that it is not a boundary. Its Hamming weight is exactly $r_Z+n+r_X$, whereas the componentwise candidate in degree two reduces to

$$m_2(A,B)=d_1(A)d_1(B).$$

Consequently, any CSS datum satisfying

$$r_Z+n+r_X<d_1(A)d_1(B)$$

produces the strict inequality $d_2(A\otimes B)<m_2(A,B)$. For orientation, a binary quantum Golay CSS presentation with parameters $[[23,1,7]]$ has $r_X=r_Z=11$, giving the numerical comparison $45<49$. The formal proof must supply an explicit CSS instance and verify its algebraic and distance properties, rather than relying on the parameter notation alone.

Formalization objectives

The first milestone proves the general certificate: for every CSS datum satisfying the hypotheses above, the element $(I_{r_Z},I_n,I_{r_X})$ is a nontrivial degree-two cycle of weight $r_Z+n+r_X$, and the componentwise minimum is $d_1(A)d_1(B)$.

The second milestone constructs and verifies one explicit CSS datum for which $r_Z+n+r_X<d_1(A)d_1(B)$. This is the step that turns the general mechanism into an actual counterexample.

The capstone packages the construction as the direct existential statement

$$\exists\,A,B\qquad d_2(A\otimes B)<\min_{0\le i\le 2}d_i(A)d_{2-i}(B).$$

Thus the final theorem is not conditional on the existence of suitable code data: it exhibits finite based binary chain complexes for which the equality proposed in Conjecture 18 fails.

Relation to prior work

The counterexample concerns only the unrestricted passage from a one-complex factor to two arbitrary bounded complexes. It does not conflict with Zeng and Pryadko's Eq. (13), whose one-complex hypothesis rules out the three-bidegree interaction used here.

The broader literature also indicates why additional structure matters. Bravyi and Hastings introduced homological-product codes and analyzed logical representatives in product constructions; Audoux and Couvreur developed tensor products of CSS codes through chain-complex methods. More recently, Akhmechet et al. discussed the Zeng–Pryadko conjecture in the structured setting of complexes derived from Khovanov homology, while Berthusen et al. restated it as Conjecture 5.1 in their study of automorphism gadgets. Golowich and Guruswami obtained strong distance guarantees for iterated homological products under expansion and local-testability hypotheses. These results are compatible with the proposed counterexample: they concern special families or impose hypotheses that are absent from Conjecture 18.

Besides settling the unrestricted statement, the formalization isolates a reusable obstruction. It shows precisely how a low-weight class assembled across several bidegrees can evade a formula based only on the degreewise distances of the factors. This distinction should help guide corrected formulations in which an exact product formula, or a useful lower bound, is recovered from additional geometric, expansion, or local-testability assumptions.

The main formal issues are mathematically substantive rather than presentational: the proof must respect the endpoint conventions for the boundary maps, distinguish a cycle from a non-boundary, compare finite weights with $\infty$-valued distances, and verify a concrete strict-gap instance. Making each of these points explicit is especially important here, because an indexing shift or a merely conditional existence statement would no longer constitute a refutation of the conjecture as stated.

References

• W. Zeng and L. P. Pryadko, Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates, Physical Review Letters 122, 230501 (2019); arXiv:1810.01519 (2018), Eq. (13).
• W. Zeng and L. P. Pryadko, Minimal distances for certain quantum product codes and tensor products of chain complexes, Physical Review A 102, 062402 (2020); arXiv:2007.12152, Conjecture 18.
• S. Bravyi and M. B. Hastings, Homological Product Codes, STOC 2014; arXiv:1311.0885.
• B. Audoux and A. Couvreur, On tensor products of CSS codes, Annales de l'Institut Henri Poincaré D 6 (2019); arXiv:1512.07081.
• R. Akhmechet et al., Khovanov homology and quantum error-correcting codes, arXiv:2410.11252 (2024).
• N. Berthusen et al., Automorphism gadgets in homological product codes, arXiv:2508.04794 (2025).
• L. Golowich and V. Guruswami, Quantum LDPC Codes of Almost Linear Distance via Iterated Homological Products, CCC 2025; full version.

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.