Table 3 — gross code $[[144,12,12]]$

Open

BBCode.gross_params

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

coding-theoryquantum-error-correction

The gross code of Bravyi et al.

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

A=x^{3}+y+y^{2},\qquad B=y^{3}+x+x^{2}

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

[[144,12,12]]

code in both sectors:

it acts on $n=144=2\cdot12\cdot6$ qubits;
it encodes $k=12$ logical qubits: $\operatorname{rank}_{\mathbb F_2}H_X+\operatorname{rank}_{\mathbb F_2}H_Z+12=144$ ;
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 gross_params :
    IsCode (l := 12) (m := 6) {(3, 0), (0, 1), (0, 2)} {(0, 3), (1, 0), (2, 0)} 144 12 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 Bravyi et al., Nature 627, 778 (2024), Table 3, https://doi.org/10.1038/s41586-024-07107-7

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=12$ , $m=6$ , so $G=\mathbb Z_{12}\times\mathbb Z_{6}$ has $72$ elements and there are $2lm=144$ qubits. The two polynomials are

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

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=144=2\cdot 12\cdot 6$ (a purely arithmetic identity).
$\operatorname{rank}_{\mathbb F_2}H_X+\operatorname{rank}_{\mathbb F_2}H_Z+12=144$ , i.e. the number of logical qubits is $k=12$ (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 3 — gross code [[144,12,12]][[144,12,12]][[144,12,12]]

Table 3 — gross code $[[144,12,12]]$