Counterexample to Zeng–Pryadko Conjecture 18

Proved

ZengPryadkoConjecture18Counterexample.refutation

by Rui Chao · Sep 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

codingtheorycounterexamplehomologicalalgebraquantumerrorcorrectiontensorproducts

There exist two finite-length based binary chain complexes $A$ and $B$ for which the homological distance of their full tensor product in degree two is strictly smaller than the minimum of the products of complementary factor distances:

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

Thus the universal equality proposed as Conjecture 18 by Zeng and Pryadko fails already for finite based chain complexes over $\mathbb F_2$ in total degree two. The theorem does not concern the one-complex special case covered by their Eq. (13).

Preamble

import Definitions.Def_ZengPryadkoConjecture18Counterexample

open ZengPryadko2019

Formal statement

namespace ZengPryadkoConjecture18Counterexample

theorem refutation :
    ∃ (A B : BasedBinaryChainComplex),
      tensorProductDistanceAt A B 2 <
        componentDistanceMinimum A B 2 := by sorry

end ZengPryadkoConjecture18Counterexample

Source

W. Zeng and L. P. Pryadko, Minimal distances for certain quantum product codes and tensor products of chain complexes, Phys. Rev. A 102, 062402 (2020), Conjecture 18, https://arxiv.org/abs/2007.12152v3; counterexample construction supplied by Rui Chao (2026)

Read-back

What the Lean code literally says, in plain math · gpt-5.6-sol

There exist two based binary chain complexes $A$ and $B$ over $\mathbb F_2=\mathbb Z/2\mathbb Z$ with the following property. Each $C\in\{A,B\}$ consists of a dimension function $n_C:\mathbb N\to\mathbb N$ , linear maps

\partial^C_j:\mathbb F_2^{\operatorname{Fin}(n_C(j))}\longrightarrow \mathbb F_2^{I^C_j}, \qquad I^C_0=\varnothing,\quad I^C_{j+1}=\operatorname{Fin}(n_C(j)),

satisfying $\partial^C_j\circ\partial^C_{j+1}=0$ for every $j$ , and a natural-number bound $\ell_C$ such that $n_C(i)=0$ whenever $\ell_C<i$ . No positivity or nontriviality condition is imposed on these dimensions, and the bound need not be minimal. For $j\in\mathbb N$ , let

T_j(A,B)=\coprod_{\substack{p,q\in\mathbb N\\p+q=j}} \operatorname{Fin}(n_A(p))\times\operatorname{Fin}(n_B(q))

be the coordinate set in tensor-product degree $j$ , and write a word on this set as $x_{p,q}(a,b)$ . The tensor boundary $D_0$ is the zero map to the word space on the empty coordinate set, while for $j\ge 1$ , $p+q=j-1$ , $a\in\operatorname{Fin}(n_A(p))$ , and $b\in\operatorname{Fin}(n_B(q))$ ,

(D_jx)_{p,q}(a,b)= \left(\partial^A_{p+1}\bigl(a'\mapsto x_{p+1,q}(a',b)\bigr)\right)_a+ \left(\partial^B_{q+1}\bigl(b'\mapsto x_{p,q+1}(a,b')\bigr)\right)_b.

All distances below take values in $\mathbb N\cup\{\infty\}$ . Define

d_C(i)=\inf\left\{ \operatorname{wt}(y): y\in\mathbb F_2^{\operatorname{Fin}(n_C(i))},\ \partial^C_i y=0,\ y\notin\operatorname{im}(\partial^C_{i+1}) \right\},

and

d_{A\otimes B}(2)=\inf\left\{ \operatorname{wt}(x): x\in\mathbb F_2^{T_2(A,B)},\ D_2x=0,\ x\notin\operatorname{im}(D_3) \right\},

where $\operatorname{wt}$ is the number of nonzero coordinates; either infimum is $\infty$ if its defining set is empty. Then the asserted property is the strict inequality

d_{A\otimes B}(2) < \inf_{i\in\{0,1,2\}} \bigl(d_A(i)\,d_B(2-i)\bigr) = \min\!\left\{ d_A(0)d_B(2),\ d_A(1)d_B(1),\ d_A(2)d_B(0) \right\},

with the products and strict order taken in $\mathbb N\cup\{\infty\}$ .

Human review

Endorsed by Shuze Chen · Sep 11, 2026
Endorsed by Rui Chao · Sep 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph