Three new weight-6 BB codes: two $[[336,20,12]]$ and one $[[360,24,12]]$

Open

BBCode.new_codes

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

coding-theoryquantum-error-correction

The three bivariate-bicycle codes of Table 9 have the stated parameters, with $d_X=d_Z=12$ :

over $\mathbb Z_2\times\mathbb Z_{84}$ , $A=1+y+xy^{5}$ , $B=1+y^{4}+y^{62}$ : $[[336,20,12]]$ ;
over $\mathbb Z_2\times\mathbb Z_{84}$ , $A=1+y+xy^{5}$ , $B=1+y^{20}+y^{46}$ : $[[336,20,12]]$ ;
over $\mathbb Z_6\times\mathbb Z_{30}$ , $A=1+y+xy^{2}$ , $B=1+y^{8}+x^{2}y^{16}$ : $[[360,24,12]]$ .

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

k=n-\operatorname{rank}H_X-\operatorname{rank}H_Z,

and each distance is the minimum weight of a nontrivial logical in that sector. These codes encode 25% and 50% more logical qubits than the best distance-12 weight-6 code previously reported.

Formalization Note IsCode is defined in BBCode_Setting.

Preamble

import Mathlib
import Definitions.Def_BBCode_Setting

Formal statement

namespace BBCode

theorem new_codes :
    IsCode (l := 2) (m := 84) {(0, 0), (0, 1), (1, 5)} {(0, 0), (0, 4), (0, 62)} 336 20 12 ∧
    IsCode (l := 2) (m := 84) {(0, 0), (0, 1), (1, 5)} {(0, 0), (0, 20), (0, 46)} 336 20 12 ∧
    IsCode (l := 6) (m := 30) {(0, 0), (0, 1), (1, 2)} {(0, 0), (0, 8), (2, 16)} 360 24 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 9 (p. 15) and Table 3 (p. 5)

Read-back

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

This is the conjunction of three code-parameter claims, identical to the three separate statements for the codes below. In each case $G=\mathbb Z_l\times\mathbb Z_m$ and $(i,j)$ stands for $x^iy^j$ .

$l=2$ , $m=84$ , $A=\{(0,0),(0,1),(1,5)\}=1+y+xy^5$ , $B=\{(0,0),(0,4),(0,62)\}=1+y^4+y^{62}$ : parameters $(n,k,d)=(336,20,12)$ .
$l=2$ , $m=84$ , the same $A$ , $B=\{(0,0),(0,20),(0,46)\}=1+y^{20}+y^{46}$ : parameters $(336,20,12)$ .
$l=6$ , $m=30$ , $A=\{(0,0),(0,1),(1,2)\}=1+y+xy^2$ , $B=\{(0,0),(0,8),(2,16)\}=1+y^8+x^2y^{16}$ : parameters $(360,24,12)$ .

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$ .

For each code, "parameters $(n,k,d)$ " means all of: (a) $n=2lm$ (arithmetic: $336=2\cdot2\cdot84$ , $360=2\cdot6\cdot30$ ); (b) $\operatorname{rank}_{\mathbb F_2}H_X+\operatorname{rank}_{\mathbb F_2}H_Z+k=2lm$ ; (c) some nontrivial X-logical has weight exactly $d$ and every nontrivial X-logical has weight $\ge d$ ; (d) the same for Z-logicals. Thus each claims exact distance $d=12$ in both sectors. In codes 1 and 2, $B$ involves only powers of $y$ . No connectivity of the Tanner graph is asserted for any of the three codes.

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

Three new weight-6 BB codes: two [[336,20,12]][[336,20,12]][[336,20,12]] and one [[360,24,12]][[360,24,12]][[360,24,12]]

Three new weight-6 BB codes: two $[[336,20,12]]$ and one $[[360,24,12]]$