Existence of a strict-gap CSS instance

Proved

ZengPryadkoConjecture18Counterexample.strictGapDataExists

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

codingtheorycounterexamplehomologicalalgebraquantumerrorcorrectiontensorproducts

There exist natural numbers $n,r_X,r_Z$ , surjective binary CSS check maps $H_X:\mathbb F_2^n\to\mathbb F_2^{r_X}$ and $H_Z:\mathbb F_2^n\to\mathbb F_2^{r_Z}$ , and a paired logical $X/Z$ vector pair satisfying all conditions of the mission definition, such that the associated three-term complexes $A,B$ obey

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

This is an unconditional existence assertion: completing it requires an actual CSS instance, rather than assuming the strict gap. The quantum Golay $[[23,1,7]]$ code and the three-level concatenated Steane code are candidate realizations.

Preamble

import Definitions.Def_ZengPryadkoConjecture18Counterexample

open ZengPryadko2019

Formal statement

namespace ZengPryadkoConjecture18Counterexample

theorem strictGapDataExists :
    ∃ (n rX rZ : ℕ) (D : CSSSwapProductData n rX rZ),
      (↑(rZ + n + rX) : WithTop ℕ) <
        chainDistanceAt (leftComplex D) 1 *
          chainDistanceAt (rightComplex D) 1 := by sorry

end ZengPryadkoConjecture18Counterexample

Source

Rui Chao, counterexample construction (unpublished note, 2026); candidate instances include the binary quantum Golay [[23,1,7]] code and the three-level concatenated Steane [[343,1,27]] code

Read-back

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

There exist natural numbers $n,r_X,r_Z$ , binary linear maps

X:\mathbb F_2^n\to\mathbb F_2^{r_X}, \qquad Z:\mathbb F_2^n\to\mathbb F_2^{r_Z},

and vectors $x_{\mathrm{log}},z_{\mathrm{log}}\in\mathbb F_2^n$ , such that $X$ and $Z$ are surjective, $X Z^{\mathsf T}=0$ , $Z X^{\mathsf T}=0$ , $Zx_{\mathrm{log}}=0$ , $Xz_{\mathrm{log}}=0$ , and $\sum_{i=0}^{n-1}x_{\mathrm{log},i}z_{\mathrm{log},i}=1$ in $\mathbb F_2=\mathbb Z/2\mathbb Z$ . Here the transposes are taken with respect to the standard finite coordinate bases. Define

d_L=\inf\left\{\operatorname{wt}(v)\ \middle|\ v\in\mathbb F_2^n,\ Xv=0,\ v\notin\operatorname{im}(Z^{\mathsf T})\right\}

and

d_R=\inf\left\{\operatorname{wt}(v)\ \middle|\ v\in\mathbb F_2^n,\ Zv=0,\ v\notin\operatorname{im}(X^{\mathsf T})\right\},

where $\operatorname{wt}(v)$ is the Hamming weight and both infima are taken in $\mathbb N\cup\{\top\}$ , with the infimum of an empty set equal to $\top$ . Equivalently, $d_L$ is the degree- $1$ homological distance of the three-term complex with dimensions $r_X,n,r_Z$ in degrees $0,1,2$ , boundaries $X$ and $Z^{\mathsf T}$ , and zero-dimensional groups above degree $2$ ; $d_R$ is the corresponding distance for the complex with dimensions $r_Z,n,r_X$ and boundaries $Z$ and $X^{\mathsf T}$ . These data satisfy the strict inequality

r_Z+n+r_X<d_Ld_R

in $\mathbb N\cup\{\top\}$ , where $r_Z+n+r_X$ is first added in $\mathbb N$ and then embedded into $\mathbb N\cup\{\top\}$ . The quantified parameters initially range over all natural numbers, including zero; the condition $x_{\mathrm{log}}\cdot z_{\mathrm{log}}=1$ rules out $n=0$ , while $r_X=0$ or $r_Z=0$ is not explicitly excluded.

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