Bivariate-bicycle codes: circulants, $H_X=[A\mid B]$ , $H_Z=[B^{\mathsf T}\mid A^{\mathsf T}]$ , logicals and distances

Definition

BBCode_Setting

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

coding-theoryquantum-error-correction

Setting for bivariate-bicycle (BB) quantum codes.

Fix $l,m\ge1$ and $G=\mathbb Z_l\times\mathbb Z_m$ . The monomial $x^iy^j$ of $\mathbb F_2[x,y]/(x^l-1,y^m-1)$ is $(i,j)\in G$ , and a polynomial is the finite set of its monomials. The circulant of $P$ is the $G\times G$ binary matrix with entry $1$ at $(g,h)$ iff $h-g\in P$ . For polynomials $A,B$ the code acts on $n=2lm$ qubits $G\sqcup G$ with

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

over $\mathbb F_2$ .

A nontrivial Z-logical is $v\in\mathbb F_2^n$ with $H_Xv=0$ and $v\notin\operatorname{row}(H_Z)$ ; a nontrivial X-logical is $v$ with $H_Zv=0$ and $v\notin\operatorname{row}(H_X)$ .
The weight $|v|$ is the number of nonzero coordinates.
The Z-distance (resp. X-distance) is exactly $d$ when some nontrivial Z-logical (X-logical) has weight $d$ and all have weight $\ge d$ .
The code encodes $k$ logical qubits when $\operatorname{rank}H_X+\operatorname{rank}H_Z+k=n$ .
IsCode A B n k d means $n=2lm$ , $k$ logical qubits, and $d_X=d_Z=d$ .
The Tanner graph joins each qubit to the X- and Z-checks with a $1$ in its column; the code is connected when this graph is connected.

These definitions are shared by every statement of the mission.

Formalization Note $k$ is stated additively to avoid truncated natural subtraction; each distance predicate includes the existence of a logical of weight exactly $d$ , so it cannot hold vacuously.

Definition code

import Mathlib

/-!
Bivariate-bicycle (BB) quantum codes, following §2 of Daugherty–Ryan–Ward,
"New distance-12 bivariate-bicycle codes with 20 and 24 logical qubits"
(Zenodo 10.5281/zenodo.23382175, v1.0.0, 2026-10-14), and Bravyi et al.,
Nature 627, 778 (2024).
-/

namespace BBCode

open Matrix

/-- The group `ℤ_l × ℤ_m`. The monomial `x^i y^j` of `𝔽₂[x,y]/(x^l - 1, y^m - 1)` is the
element `(i, j)`. -/
abbrev Grp (l m : ℕ) := ZMod l × ZMod m

/-- A polynomial of `𝔽₂[x,y]/(x^l - 1, y^m - 1)`, given by its support: the finite set of
monomials `(i, j)` whose coefficient is `1`. -/
abbrev Poly (l m : ℕ) := Finset (Grp l m)

/-- The `lm × lm` circulant of a polynomial `P`: row `g` has a `1` in column `g + t`
for each monomial `t ∈ P`, and `0` elsewhere. -/
def circulant {l m : ℕ} (P : Poly l m) : Matrix (Grp l m) (Grp l m) (ZMod 2) :=
  fun g h => if h - g ∈ P then 1 else 0

/-- The physical qubits: two blocks of `lm` qubits, `n = 2lm` in total. -/
abbrev Qubit (l m : ℕ) := Grp l m ⊕ Grp l m

/-- The X-check matrix `H_X = [A | B]`. -/
def HX {l m : ℕ} (A B : Poly l m) : Matrix (Grp l m) (Qubit l m) (ZMod 2) :=
  Matrix.fromCols (circulant A) (circulant B)

/-- The Z-check matrix `H_Z = [Bᵀ | Aᵀ]`. -/
def HZ {l m : ℕ} (A B : Poly l m) : Matrix (Grp l m) (Qubit l m) (ZMod 2) :=
  Matrix.fromCols (circulant B)ᵀ (circulant A)ᵀ

/-- The row space of a binary matrix: the `𝔽₂`-span of its rows. -/
def rowSpace {r c : Type} (H : Matrix r c (ZMod 2)) : Submodule (ZMod 2) (c → ZMod 2) :=
  Submodule.span (ZMod 2) (Set.range H)

/-- The Hamming weight of a binary vector: the number of nonzero coordinates. -/
def weight {ι : Type} [Fintype ι] (v : ι → ZMod 2) : ℕ :=
  (Finset.univ.filter fun i => v i ≠ 0).card

/-- A nontrivial Z-logical operator: `H_X v = 0` and `v ∉ row(H_Z)`. -/
def IsZLogical {l m : ℕ} [NeZero l] [NeZero m] (A B : Poly l m) (v : Qubit l m → ZMod 2) :
    Prop :=
  HX A B *ᵥ v = 0 ∧ v ∉ rowSpace (HZ A B)

/-- A nontrivial X-logical operator: `H_Z v = 0` and `v ∉ row(H_X)`. -/
def IsXLogical {l m : ℕ} [NeZero l] [NeZero m] (A B : Poly l m) (v : Qubit l m → ZMod 2) :
    Prop :=
  HZ A B *ᵥ v = 0 ∧ v ∉ rowSpace (HX A B)

/-- The Z-distance is exactly `d`: some nontrivial Z-logical has weight `d`, and every
nontrivial Z-logical has weight at least `d`. -/
def HasZDistance {l m : ℕ} [NeZero l] [NeZero m] (A B : Poly l m) (d : ℕ) : Prop :=
  (∃ v, IsZLogical A B v ∧ weight v = d) ∧ ∀ v, IsZLogical A B v → d ≤ weight v

/-- The X-distance is exactly `d`. -/
def HasXDistance {l m : ℕ} [NeZero l] [NeZero m] (A B : Poly l m) (d : ℕ) : Prop :=
  (∃ v, IsXLogical A B v ∧ weight v = d) ∧ ∀ v, IsXLogical A B v → d ≤ weight v

/-- The code encodes `k` logical qubits: `k = n - rank H_X - rank H_Z` with `n = 2lm`
(stated additively to avoid truncated subtraction). -/
def NumLogical {l m : ℕ} [NeZero l] [NeZero m] (A B : Poly l m) (k : ℕ) : Prop :=
  (HX A B).rank + (HZ A B).rank + k = 2 * (l * m)

/-- The BB code of `(A, B)` is an `[[n, k, d]]` code with `d_X = d_Z = d`. -/
def IsCode {l m : ℕ} [NeZero l] [NeZero m] (A B : Poly l m) (n k d : ℕ) : Prop :=
  n = 2 * (l * m) ∧ NumLogical A B k ∧ HasXDistance A B d ∧ HasZDistance A B d

/-- The Tanner graph: qubits are joined to the X- and Z-checks that act on them. -/
def tannerGraph {l m : ℕ} (A B : Poly l m) :
    SimpleGraph (Qubit l m ⊕ (Grp l m ⊕ Grp l m)) :=
  SimpleGraph.fromRel fun u w =>
    match u, w with
    | Sum.inl q, Sum.inr (Sum.inl c) => HX A B c q = 1
    | Sum.inl q, Sum.inr (Sum.inr c) => HZ A B c q = 1
    | _, _ => False

/-- A BB code is connected (indecomposable) when its Tanner graph is connected. -/
def IsConnected {l m : ℕ} (A B : Poly l m) : Prop :=
  (tannerGraph A B).Connected

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, §2 'Setting and engines' (p. 2); conventions as in 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 item is a file of definitions only; it asserts nothing by itself. Everything is parametrised by natural numbers $l,m$ .

Group. $G_{l,m}=\mathbb Z_l\times\mathbb Z_m$ (integers mod $l$ times integers mod $m$ ). Edge case: if $l=0$ (resp. $m=0$ ), the factor $\mathbb Z_0$ is the full integers $\mathbb Z$ , so $G$ is infinite. The definitions below that need finiteness (logical operators, distances, logical count, IsCode) explicitly require $l\ne 0$ and $m\ne 0$ ; the circulant, the check matrices, the Tanner graph and its connectivity do not, and are also defined (on infinite index sets) when $l=0$ or $m=0$ .
Polynomials. A polynomial $P$ is a finite subset of $G$ , interpreted as the support of an element of $\mathbb F_2[x,y]/(x^l-1,y^m-1)$ , with $(i,j)\leftrightarrow x^iy^j$ . Because it is a set, every monomial has coefficient $0$ or $1$ and listed duplicates would silently merge.
Circulant. $M_P$ is the $G\times G$ matrix over $\mathbb F_2$ with

(M_P)_{g,h}=\begin{cases}1 & h-g\in P\\ 0&\text{otherwise,}\end{cases}

so row $g$ has ones exactly at columns $g+t$ , $t\in P$ . Its transpose has $(M_P^{\top})_{g,h}=1$ iff $g-h\in P$ .

Qubits. $Q=G\sqcup G$ : a left block $L$ and a right block $R$ , each a copy of $G$ (so $2lm$ qubits when $l,m\ge1$ ).
Check matrices. Rows indexed by $G$ , columns by $Q$ :

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

the first block acting on $L$ , the second on $R$ .

Row space. $\operatorname{row}(H)$ is the $\mathbb F_2$ -linear span of the rows of $H$ .
Weight. $|v|$ = number of coordinates where $v\ne0$ (Hamming weight).
Nontrivial Z-logical (needs $l,m\ne0$ ): $v\in\mathbb F_2^{Q}$ with $H_Xv=0$ and $v\notin\operatorname{row}(H_Z)$ . Nontrivial X-logical: $H_Zv=0$ and $v\notin\operatorname{row}(H_X)$ . The weight used later is the weight of $v$ itself (all members of a coset are separately considered, so the minimum is over all such $v$ ).
Exact Z-distance $d$ : there exists a nontrivial Z-logical of weight exactly $d$ , and every nontrivial Z-logical has weight $\ge d$ ; i.e. $d$ is the minimum weight. If no nontrivial Z-logical exists (e.g. zero logical qubits) this predicate is false for every $d$ . Exact X-distance $d$ is defined identically with X-logicals.
Number of logical qubits $k$ : $\operatorname{rank}_{\mathbb F_2}H_X+\operatorname{rank}_{\mathbb F_2}H_Z+k=2lm$ . Stated additively, so there is no truncated subtraction; $k$ is uniquely determined when it holds.
IsCode $(A,B,n,k,d)$ : $n=2lm$ , the logical count is $k$ , the X-distance is exactly $d$ , and the Z-distance is exactly $d$ (the same $d$ for both). It contains no condition on the sizes of $A,B$ and no connectivity condition.
Tanner graph. A simple graph on vertex set $Q\sqcup(C_X\sqcup C_Z)$ , where $C_X$ and $C_Z$ are two further copies of $G$ (X-checks and Z-checks). Edges: qubit $q$ — X-check $c$ iff $(H_X)_{c,q}=1$ ; qubit $q$ — Z-check $c$ iff $(H_Z)_{c,q}=1$ ; no other edges (no qubit–qubit or check–check edges), symmetrised and loop-free.
IsConnected $(A,B)$ : the Tanner graph is connected (nonempty, and every two vertices are joined by a path). Both X- and Z-checks are in this single graph. No $l,m\ne0$ assumption is imposed here.

The docstrings cite Daugherty–Ryan–Ward and Bravyi et al.; those references have no formal content.

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

Bivariate-bicycle codes: circulants, HX=[A∣B]H_X=[A\mid B]HX​=[A∣B], HZ=[BT∣AT]H_Z=[B^{\mathsf T}\mid A^{\mathsf T}]HZ​=[BT∣AT], logicals and distances

Bivariate-bicycle codes: circulants, $H_X=[A\mid B]$ , $H_Z=[B^{\mathsf T}\mid A^{\mathsf T}]$ , logicals and distances