bb72
[[72,12,6]] engineering not started[[72,12,6]] BB6 code
Description
A bivariate bicycle (BB) code with parameters [[72,12,6]] and weight-six stabilizer generators \cite{arxiv:2308.07915}. One defining presentation uses \((\ell,m)=(6,6)\) with x^{\ell}=y^{m}=1, and A=x^3+y+y^2, B=y^3+x+x^2 in…
Introduced in: arxiv:2308.07915
Rationale
Re-scored 2026-07-18: the gross program left bb72's hard math DONE on main. The strong small-cycle theorem gives the unconditional chain-level floor `base_distance_ge_6` and `base_chain_distance_eq_6` (d(base) = 6 exactly, weight-6 witness) in Codes/BivariateBicycle/BaseDistance.lean, and the A16 class small-cycle theorem subsumes it analytically. What remains is engineering, not research: Pauli-level StabilizerCode packaging + chain-to-Pauli distance transport mirroring the gross Phase-5 / pair72 S3.9 recipe (trimmed generator list, decoder-certified independence, `StabilizerCodeWithDistance 72 12 6`); the pair72 data-generator script pattern adapts directly. Highest-value BB deliverable per marginal cost: IBM's published [[72,12,6]] companion to the formalized gross code. Previous rationale: Re-scored 2026-05-23: `QEC/Stabilizer/Homological/BBChainComplex.lean` (~285 LoC, on main from the gross moonshot Approach A) now provides the generic BB chain complex framework for any finite abelian G + polynomial pair (A,B) in F_2[G], plus convolution algebra and the abstract `chainWeight_lower_bound_transfers` distance-bridge combinator. Prerequisites bumped from 4 -> 6 (partial unblock). Distance-bound machinery (tight algebraic / homological argument) is still open per the gross Approach A + B negative results, so tractability remains low.