9 Bivariate-bicycle codes and the gross code
Bivariate-bicycle codes are qLDPC codes built from two commuting polynomial shift operators on an abelian group. The gross code is the \([[144,12,12]]\) member of the family; the argument here derives its distance from that of its \([[72,12,6]]\) base by exhibiting the gross complex as a free \(\mathbb {Z}_2\) cover of the base and showing the distance doubles.
The data exhibiting one bivariate-bicycle complex as a free double cover of another: a deck transformation \(\sigma \) of order two acting freely, commuting with both boundary maps, with the base recovered as the quotient. The gross \([[144,12,12]]\) code covers the \([[72,12,6]]\) base exactly this way, and the doubling of the distance from \(6\) to \(12\) is what the cover is used to prove.
9.1 The base floor
The base contributes a floor of six, established by ruling out every light cycle with a finite certificate that the kernel checks directly.
The finite data certifying that a bivariate-bicycle complex has no light cycles: an enumeration showing that every nonzero cycle of weight below the target floor would produce an impossible syndrome pattern.
From a definition 73 certificate, every nonzero cycle has weight at least six.
The certificate rules out weights one through five by a finite case analysis on the possible supports, each case contradicting the syndrome constraint \(\partial _1 c = 0\). The enumeration is checked in the kernel rather than by compiled evaluation, so the result carries no compiler-trust axiom.
Every nonzero class in the homology of the base bivariate-bicycle complex is represented only by chains of weight at least six, and six is attained.
The lower bound is theorem 74 together with the check that no weight-six cycle is a boundary; the witness realises the bound.
Pulled back along the cover of definition 72, the base floor gives a weight-six lower bound for every nontrivial logical operator of the gross code.
Pushing a gross chain down to the base is a chain map, so it sends cycles to cycles and boundaries to boundaries, and it cannot increase weight. If the pushed-down chain is a nonzero class, theorem 75 applies directly.
9.2 Doubling
Pushing a gross logical down to the base gives weight at least six. Getting to twelve requires knowing when the two sheets of the cover contribute independently. They do outside a dangerous sector, where the deck transformation acts trivially on homology; there the light stabilizers are classified explicitly and the surviving classes are confined to Smith cosets whose floor is again twelve.
Every nontrivial gross logical operator falls into one of two sectors, and in each the weight is at least twelve: the *safe* sector, where the two sheets of the cover contribute independently, and the *dangerous* sector, where they do not and a finer argument is needed.
In the safe sector the class survives to each sheet separately, so theorem 76 applies twice and the weights add to at least \(6 + 6 = 12\). The dangerous sector is where the deck transformation acts trivially on homology; there the hexagon and direction-pair bounds take over, classifying the light stabilizers and confining the remaining classes to Smith cosets whose floor is again twelve.
IBM’s gross code presented as a definition 37 with \(n = 144\) and \(k = 12\).
The gross code (definition 78) has distance exactly \(12\), unconditionally.
The lower bound is theorem 77, moved from chains to Pauli weights by theorem 58. A weight-twelve logical operator is exhibited explicitly, making the distance exact rather than a bound. Every finite check in the argument is discharged in the kernel, so the theorem depends on exactly the three standard axioms.
The \([[144,12,12]]\) gross code as an inhabitant of definition 41 — the headline result of this development.