Quantum Error Correction

2 missions · 2 completed

Missions

Completed

Captain: Rui Chao

Counterexamples to the Zeng–Pryadko Homological-Distance ConjectureResearch Paper

## 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*](https://arxiv.org/abs/1810.01519), posted in 2018 and subsequently [published in *Physical Review Letters*](https://link.aps.org/doi/10.1103/PhysRevLett.122.230501), 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*](https://prove2.me/missions/Higher-Dimensional%20Quantum%20Hypergraph-Product%20Codes%20with%20Finite%20Rates). 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*](https://link.aps.org/doi/10.1103/PhysRevA.102.062402), published in 2020. In [the corresponding arXiv preprint](https://arxiv.org/abs/2007.12152), 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*](https://prove2.me/theorems/9d65f1ac-c78c-4540-8ac4-38597548a9ff). 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*](https://prove2.me/theorems/4f4006fe-af5b-42ba-a936-bb49e92c92b6). 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](https://dl.acm.org/doi/10.1145/2591796.2591870) introduced homological-product codes and analyzed logical representatives in product constructions; [Audoux and Couvreur](https://www.numdam.org/articles/10.4171/aihpd/71/) developed tensor products of CSS codes through chain-complex methods. More recently, [Akhmechet et al.](https://arxiv.org/abs/2410.11252) discussed the Zeng–Pryadko conjecture in the structured setting of complexes derived from Khovanov homology, while [Berthusen et al.](https://arxiv.org/abs/2508.04794) restated it as Conjecture 5.1 in their study of automorphism gadgets. [Golowich and Guruswami](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.25) 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*](https://link.aps.org/doi/10.1103/PhysRevLett.122.230501), *Physical Review Letters* 122, 230501 (2019); [arXiv:1810.01519 (2018), Eq. (13)](https://arxiv.org/abs/1810.01519). - W. Zeng and L. P. Pryadko, [*Minimal distances for certain quantum product codes and tensor products of chain complexes*](https://link.aps.org/doi/10.1103/PhysRevA.102.062402), *Physical Review A* 102, 062402 (2020); [arXiv:2007.12152, Conjecture 18](https://arxiv.org/abs/2007.12152). - S. Bravyi and M. B. Hastings, [*Homological Product Codes*](https://dl.acm.org/doi/10.1145/2591796.2591870), STOC 2014; [arXiv:1311.0885](https://arxiv.org/abs/1311.0885). - B. Audoux and A. Couvreur, [*On tensor products of CSS codes*](https://www.numdam.org/articles/10.4171/aihpd/71/), *Annales de l'Institut Henri Poincaré D* 6 (2019); [arXiv:1512.07081](https://arxiv.org/abs/1512.07081). - R. Akhmechet et al., [*Khovanov homology and quantum error-correcting codes*](https://arxiv.org/abs/2410.11252), arXiv:2410.11252 (2024). - N. Berthusen et al., [*Automorphism gadgets in homological product codes*](https://arxiv.org/abs/2508.04794), arXiv:2508.04794 (2025). - L. Golowich and V. Guruswami, [*Quantum LDPC Codes of Almost Linear Distance via Iterated Homological Products*](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2025.25), CCC 2025; [full version](https://arxiv.org/abs/2411.03646).

6 thms2 active usersReviewed

Completed

Captain: Rui Chao

Higher-Dimensional Quantum Hypergraph-Product Codes with Finite RatesResearch Paper

## 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)](https://doi.org/10.1103/PhysRevLett.122.230501). Its main distance result is Eq. (13) in the [arXiv version](https://arxiv.org/abs/1810.01519): 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,”](https://doi.org/10.1103/PhysRevLett.122.230501) *Physical Review Letters* 122, 230501 (2019). [arXiv:1810.01519](https://arxiv.org/abs/1810.01519). - Benjamin Audoux and Alain Couvreur, [“On Tensor Products of CSS Codes,”](https://arxiv.org/abs/1512.07081) 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,”](https://doi.org/10.1109/TIT.2013.2292061) *IEEE Transactions on Information Theory* 60 (2014), 1193--1202.

4 thms1 active userReviewed