Table 9 — new $[[360,24,12]]$ code

Open

BBCode.new360_params

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

coding-theoryquantum-error-correction

New bivariate-bicycle code with 24 logical qubits.

Let $G=\mathbb Z_{6}\times\mathbb Z_{30}$ and let

A=1+y+xy^{2},\qquad B=1+y^{8}+x^{2}y^{16}

in $\mathbb F_2[x,y]/(x^{6}-1,\,y^{30}-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

[[360,24,12]]

code in both sectors:

it acts on $n=360=2\cdot6\cdot30$ qubits;
it encodes $k=24$ logical qubits: $\operatorname{rank}_{\mathbb F_2}H_X+\operatorname{rank}_{\mathbb F_2}H_Z+24=360$ ;
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 new360_params :
    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 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=6$ , $m=30$ , so $G=\mathbb Z_{6}\times\mathbb Z_{30}$ has $180$ elements and there are $2lm=360$ qubits. The two polynomials are

A=\{(0,0),(0,1),(1,2)\}\;\;(\text{i.e. }A=1+y+xy^2),\qquad B=\{(0,0),(0,8),(2,16)\}\;\;(\text{i.e. }B=1+y^8+x^2y^{16}),

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=360=2\cdot 6\cdot 30$ (a purely arithmetic identity).
$\operatorname{rank}_{\mathbb F_2}H_X+\operatorname{rank}_{\mathbb F_2}H_Z+24=360$ , i.e. the number of logical qubits is $k=24$ (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.

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 [[360,24,12]][[360,24,12]][[360,24,12]] code

Table 9 — new $[[360,24,12]]$ code