Table 9 — new $[[336,20,12]]$ code, class 1

Open

BBCode.new336_class1_params

by Winningatmath · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

coding-theoryquantum-error-correction

New bivariate-bicycle code, class 1 of the two $[[336,20,12]]$ symmetry classes.

Let $G=\mathbb Z_{2}\times\mathbb Z_{84}$ and let

A=1+y+xy^{5},\qquad B=1+y^{4}+y^{62}

in $\mathbb F_2[x,y]/(x^{2}-1,\,y^{84}-1)$ . The bivariate-bicycle code with check matrices $H_X=[A\mid B]$ and $H_Z=[B^{\mathsf T}\mid A^{\mathsf T}]$ is an

[[336,20,12]]

code in both sectors:

it acts on $n=336=2\cdot2\cdot84$ qubits;
it encodes $k=20$ logical qubits: $\operatorname{rank}_{\mathbb F_2}H_X+\operatorname{rank}_{\mathbb F_2}H_Z+20=336$ ;
its X-distance is exactly $12$ : some $v$ with $H_Zv=0$ and $v\notin\operatorname{row}(H_X)$ has weight $12$ , and every such $v$ has weight at least $12$ ;
its Z-distance is exactly $12$ (dually, with $H_X$ and $H_Z$ exchanged).

Formalization Note Polynomials are Finsets of monomials $(i,j)$ in ZMod l × ZMod m; IsCode A B n k d is defined in BBCode_Setting.

Preamble

import Mathlib
import Definitions.Def_BBCode_Setting

Formal statement

namespace BBCode

theorem new336_class1_params :
    IsCode (l := 2) (m := 84) {(0, 0), (0, 1), (1, 5)} {(0, 0), (0, 4), (0, 62)} 336 20 12 := by
  sorry

end BBCode

Source

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, Zenodo v1.0.0 (2026), https://doi.org/10.5281/zenodo.23382175, Table 3 (p. 5); polynomials from Table 9 (p. 15)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

This statement concerns one specific bivariate-bicycle code with $l=2$ , $m=84$ , so $G=\mathbb Z_{2}\times\mathbb Z_{84}$ has $168$ elements and there are $2lm=336$ qubits. The two polynomials are

A=\{(0,0),(0,1),(1,5)\}\;\;(\text{i.e. }A=1+y+xy^5),\qquad B=\{(0,0),(0,4),(0,62)\}\;\;(\text{i.e. }B=1+y^4+y^{62}),

each a set of three distinct monomials (no exponent pair collides after reduction mod $l$ and mod $m$ ).

Unfolded definitions used below. For $l,m\ge 1$ write $G=\mathbb Z_l\times\mathbb Z_m$ ; an element $(i,j)\in G$ stands for the monomial $x^iy^j$ , and a "polynomial" is a finite subset $P\subseteq G$ (its support, coefficients in $\mathbb F_2$ ). The circulant $M_P$ is the $G\times G$ matrix over $\mathbb F_2$ with $(M_P)_{g,h}=1$ iff $h-g\in P$ and $0$ otherwise. The qubit set is $Q=G\sqcup G$ (a left block $L$ and a right block $R$ , $|Q|=2lm$ ). The check matrices (rows indexed by $G$ , columns by $Q$ ) are

H_X=\big[\,M_A\;\big|\;M_B\,\big],\qquad H_Z=\big[\,M_B^{\top}\;\big|\;M_A^{\top}\,\big],

with the first block on $L$ and the second on $R$ . A vector $v\in\mathbb F_2^{Q}$ is a nontrivial Z-logical if $H_Xv=0$ and $v\notin\operatorname{row}(H_Z)$ (the $\mathbb F_2$ -span of the rows of $H_Z$ ); it is a nontrivial X-logical if $H_Zv=0$ and $v\notin\operatorname{row}(H_X)$ . The weight $|v|$ is the number of nonzero coordinates of $v$ .

Assertion. The code of $(A,B)$ satisfies all four of the following simultaneously:

$n=336=2\cdot 2\cdot 84$ (a purely arithmetic identity).
$\operatorname{rank}_{\mathbb F_2}H_X+\operatorname{rank}_{\mathbb F_2}H_Z+20=336$ , i.e. the number of logical qubits is $k=20$ (stated additively, so no truncated subtraction is involved).
X-distance exactly $12$ : there exists a nontrivial X-logical $v$ with $|v|=12$ , and every nontrivial X-logical has $|v|\ge 12$ .
Z-distance exactly $12$ : there exists a nontrivial Z-logical $v$ with $|v|=12$ , and every nontrivial Z-logical has $|v|\ge 12$ .

So it claims an exact value $d=12$ for both sectors (a lower bound and attainment), not merely an upper or lower bound. Nothing is asserted about the connectivity of the Tanner graph or about any other code; the predicate does not include a connectivity condition.

Note that $B$ involves only powers of $y$ (all its $x$ -exponents are $0$ ), while $A$ contains the single $x$ -dependent term $xy^5$ ; here $\mathbb Z_2$ means integers mod $2$ .

Human review

Endorsed by Shuze Chen · Oct 18, 2026
Confirmed by the moderator at approval.
Endorsed by Winningatmath · Oct 18, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Table 9 — new [[336,20,12]][[336,20,12]][[336,20,12]] code, class 1

Table 9 — new $[[336,20,12]]$ code, class 1