Remark 22: The Double Gross Code Definition

Statement

The Double Gross code is a [[288, 12, 18]] BB code (Rem_19) with parameters ℓ = 12, m = 12, A = x³ + y⁷ + y², B = y³ + x² + x.

Logical operators: X̄_α = X(αf, 0) where f has weight 18.

Gauging measurement construction:

• 18 vertices (support of f)
• 27 matching edges + 7 expansion edges (one double edge, for 34 edges counting multiplicity)
• 13 independent cycles (≤ cycle rank of 17)
• Total overhead: 18 + 13 + 34 = 65

Main Results

• doubleGrossA, doubleGrossB: the polynomials A and B
• doubleGrossCode: the Double Gross code as a valid stabilizer code
• doubleGrossF: the logical operator polynomial f with weight 18
• dblLogicalXBar: the logical X operator X̄_α = X(αf, 0)
• doubleGrossCode_numQubits: n = 288
• doubleGrossCode_numChecks: 288 checks
• doubleGrossCode_k: k = 12 (from joint kernel dimension)
• dblLogicalXBar_weight: X̄_α has weight 18
• dblGaugingVertices_card: 18 vertices
• dblGaugingEdges_card: 33 distinct edges (34 counting multiplicity)
• dblGaugingGraph_connected_on_support: gauging graph is connected on supp(f)
• dblCycleRank_with_multiplicity: cycle rank = 17 (with multiplicity)
• dblFluxChecks_le_cycleRank: 13 ≤ 17 (sufficient cycles exist)
• dblTotal_overhead: total overhead = 65

The Double Gross code parameters

@[reducible, inline]

abbrev BivariateBicycle.DoubleGrossCode.ℓ : ℕ

ℓ = 12 for the Double Gross code.

Equations

• BivariateBicycle.DoubleGrossCode.ℓ = 12

@[reducible, inline]

abbrev BivariateBicycle.DoubleGrossCode.m : ℕ

m = 12 for the Double Gross code.

Equations

• BivariateBicycle.DoubleGrossCode.m = 12

@[reducible, inline]

abbrev BivariateBicycle.DoubleGrossCode.DGMonomial : Type

The monomial group for the Double Gross code: Z₁₂ × Z₁₂.

Equations

• BivariateBicycle.DoubleGrossCode.DGMonomial = BivariateBicycle.BBMonomial BivariateBicycle.DoubleGrossCode.ℓ BivariateBicycle.DoubleGrossCode.m

@[reducible, inline]

abbrev BivariateBicycle.DoubleGrossCode.DGAlgebra : Type

The group algebra for the Double Gross code: F₂[x,y]/(x¹² - 1, y¹² - 1).

Equations

• BivariateBicycle.DoubleGrossCode.DGAlgebra = BivariateBicycle.BBGroupAlgebra BivariateBicycle.DoubleGrossCode.ℓ BivariateBicycle.DoubleGrossCode.m

@[reducible, inline]

abbrev BivariateBicycle.DoubleGrossCode.DGQubit : Type

The qubit type for the Double Gross code.

Equations

• BivariateBicycle.DoubleGrossCode.DGQubit = BivariateBicycle.BBQubit BivariateBicycle.DoubleGrossCode.ℓ BivariateBicycle.DoubleGrossCode.m

Polynomial definitions

def BivariateBicycle.DoubleGrossCode.doubleGrossA : DGAlgebra

A = x³ + y⁷ + y² in F₂[x,y]/(x¹² - 1, y¹² - 1).

Equations

• BivariateBicycle.DoubleGrossCode.doubleGrossA = BivariateBicycle.bbMonomial 3 0 + BivariateBicycle.bbMonomial 0 7 + BivariateBicycle.bbMonomial 0 2

def BivariateBicycle.DoubleGrossCode.doubleGrossB : DGAlgebra

B = y³ + x² + x in F₂[x,y]/(x¹² - 1, y¹² - 1).

Equations

• BivariateBicycle.DoubleGrossCode.doubleGrossB = BivariateBicycle.bbMonomial 0 3 + BivariateBicycle.bbMonomial 2 0 + BivariateBicycle.bbMonomial 1 0

Check commutation

theorem BivariateBicycle.DoubleGrossCode.doubleGrossChecks_XZ_commute (α β : DGMonomial) : (bbCheckX doubleGrossA doubleGrossB α).PauliCommute (bbCheckZ doubleGrossA doubleGrossB β)

theorem BivariateBicycle.DoubleGrossCode.doubleGrossChecks_commute (i j : BBCheckIndex ℓ m) : (bbCheck doubleGrossA doubleGrossB i).PauliCommute (bbCheck doubleGrossA doubleGrossB j)

The Double Gross code as a stabilizer code

noncomputable def BivariateBicycle.DoubleGrossCode.doubleGrossCode : StabilizerCode DGQubit

The Double Gross code as a valid stabilizer code.

Equations

• One or more equations did not get rendered due to their size.

theorem BivariateBicycle.DoubleGrossCode.doubleGrossCode_numQubits : doubleGrossCode.numQubits = 288

The Double Gross code has 288 = 2 × 12 × 12 physical qubits.

theorem BivariateBicycle.DoubleGrossCode.doubleGrossCode_numChecks : doubleGrossCode.numChecks = 288

The Double Gross code has 288 = 2 × 12 × 12 checks.

Code parameter k = 12

For BB codes, the 2ℓm checks are not independent. The nominal parameter k = n - rank(H) where H is the check matrix. For the CSS structure, k = 2 · dim(ker(A) ∩ ker(B)) where "ker(A)" is the kernel of left-convolution by A in the group algebra.

We compute this by Gaussian elimination over F₂ on the stacked convolution matrix [A; B] of size 288 × 144.

theorem BivariateBicycle.DoubleGrossCode.doubleGrossCode_k : 2 * (144 - BivariateBicycle.DoubleGrossCode.f2GaussRank✝ 144 BivariateBicycle.DoubleGrossCode.dblStackedMatrixRows✝) = 12

The Double Gross code encodes k = 12 logical qubits. This is 2 × nullity(stacked matrix [A; B]), where the nullity is 144 - rank([A; B]) = 144 - 138 = 6. The factor 2 comes from the CSS structure (6 X-type + 6 Z-type independent logical operators).

Logical operator polynomial

def BivariateBicycle.DoubleGrossCode.doubleGrossF : DGAlgebra

f = 1 + x + x² + x⁷ + x⁸ + x⁹ + x¹⁰ + x¹¹

• (1 + x⁶ + x⁸ + x¹⁰)y³
• (x⁵ + x⁶ + x⁹ + x¹⁰)y⁶
• (x⁴ + x⁸)y⁹

Equations

• One or more equations did not get rendered due to their size.

Logical X operators

def BivariateBicycle.DoubleGrossCode.dblLogicalXBar (α : DGMonomial) : PauliOp DGQubit

The logical X operator X̄_α = X(αf, 0) for α ∈ M.

Equations

• BivariateBicycle.DoubleGrossCode.dblLogicalXBar α = BivariateBicycle.pauliXBB (BivariateBicycle.bbShift α BivariateBicycle.DoubleGrossCode.doubleGrossF) 0

theorem BivariateBicycle.DoubleGrossCode.dblLogicalXBar_pure_X (α : DGMonomial) : (dblLogicalXBar α).zVec = 0

X̄_α is pure X-type: it has no Z-support.

theorem BivariateBicycle.DoubleGrossCode.dblLogicalXBar_acts_only_on_L (α δ : DGMonomial) : (dblLogicalXBar α).xVec (Sum.inr δ) = 0

X̄_α acts only on L qubits: xVec on R qubits is zero.

theorem BivariateBicycle.DoubleGrossCode.dblLogicalXBar_mul_self (α : DGMonomial) : dblLogicalXBar α * dblLogicalXBar α = 1

X̄_α is self-inverse.

Support and weight

theorem BivariateBicycle.DoubleGrossCode.doubleGrossF_weight_eq_18 : {γ : DGMonomial | doubleGrossF γ ≠ 0}.card = 18

The polynomial f has weight 18 (18 nonzero coefficients).

theorem BivariateBicycle.DoubleGrossCode.doubleGrossA_support_card : {γ : DGMonomial | doubleGrossA γ ≠ 0}.card = 3

A has 3 nonzero coefficients.

theorem BivariateBicycle.DoubleGrossCode.doubleGrossB_support_card : {γ : DGMonomial | doubleGrossB γ ≠ 0}.card = 3

B has 3 nonzero coefficients.

Shift-invariance of support cardinality

theorem BivariateBicycle.DoubleGrossCode.dblLogicalXBar_weight (α : DGMonomial) : (dblLogicalXBar α).weight = 18

X̄_α has weight 18.

Kernel conditions for logical operator commutation

theorem BivariateBicycle.DoubleGrossCode.dblLogicalXBar_commute_xCheck (α β : DGMonomial) : (dblLogicalXBar α).PauliCommute (bbCheckX doubleGrossA doubleGrossB β)

X̄_α commutes with all X checks (both pure X-type).

theorem BivariateBicycle.DoubleGrossCode.dblLogicalXBar_commute_zCheck (α β : DGMonomial) : (dblLogicalXBar α).PauliCommute (bbCheckZ doubleGrossA doubleGrossB β)

X̄_α commutes with all Z checks.

theorem BivariateBicycle.DoubleGrossCode.dblLogicalXBar_commute_allChecks (α : DGMonomial) (i : BBCheckIndex ℓ m) : (dblLogicalXBar α).PauliCommute (bbCheck doubleGrossA doubleGrossB i)

X̄_α commutes with all checks of the Double Gross code.

theorem BivariateBicycle.DoubleGrossCode.dblLogicalXBar_inCentralizer (α : DGMonomial) : doubleGrossCode.inCentralizer (dblLogicalXBar α)

X̄_α is in the centralizer of the Double Gross code.

xVec characterization

@[simp]

theorem BivariateBicycle.DoubleGrossCode.dblLogicalXBar_xVec_left (α γ : DGMonomial) : (dblLogicalXBar α).xVec (Sum.inl γ) = doubleGrossF (γ - α)

@[simp]

theorem BivariateBicycle.DoubleGrossCode.dblLogicalXBar_xVec_right (α δ : DGMonomial) : (dblLogicalXBar α).xVec (Sum.inr δ) = 0

@[simp]

theorem BivariateBicycle.DoubleGrossCode.dblLogicalXBar_zVec (α : DGMonomial) : (dblLogicalXBar α).zVec = 0

The gauging graph

def BivariateBicycle.DoubleGrossCode.dblGaugingVertices : Finset DGMonomial

The support of f: the 18 monomials γ with f(γ) ≠ 0 in the Double Gross code.

Equations

• BivariateBicycle.DoubleGrossCode.dblGaugingVertices = {γ : BivariateBicycle.DoubleGrossCode.DGMonomial | BivariateBicycle.DoubleGrossCode.doubleGrossF γ ≠ 0}

theorem BivariateBicycle.DoubleGrossCode.dblGaugingVertices_card : dblGaugingVertices.card = 18

The vertices of the gauging graph are exactly the 18 monomials in supp(f).

@[simp]

theorem BivariateBicycle.DoubleGrossCode.mem_dblGaugingVertices (γ : DGMonomial) : γ ∈ dblGaugingVertices ↔ doubleGrossF γ ≠ 0

Matching edge condition

Two vertices γ, δ ∈ supp(f) with γ ≠ δ share a Z check iff γ - δ = -B_i + B_j for B_i, B_j ∈ {y³, x², x} (the monomial terms of B), where B_i^T = B_i(x⁻¹, y⁻¹). In the additive group: -B_i + B_j means (in Z₁₂ × Z₁₂) negate B_i and add B_j. The terms of B = y³ + x² + x are (0,3), (2,0), (1,0).

def BivariateBicycle.DoubleGrossCode.dblIsMatchingDiff (d : DGMonomial) : Bool

Whether a difference d equals -B_i + B_j for some distinct terms B_i, B_j of B. The terms of B are (0,3), (2,0), (1,0) in Z₁₂ × Z₁₂.

Equations

• One or more equations did not get rendered due to their size.

def BivariateBicycle.DoubleGrossCode.dblIsMatchingEdge (γ δ : DGMonomial) : Bool

The matching edge condition: γ and δ are in supp(f) and share a Z check.

Equations

• One or more equations did not get rendered due to their size.

Expansion edges

def BivariateBicycle.DoubleGrossCode.dblExpansionEdges : List (DGMonomial × DGMonomial)

The 6 distinct expansion edges (as unordered pairs). The paper lists 7 expansion edges including one double edge (x², x⁶y³). As a SimpleGraph, we have 6 distinct edges. Monomials in Z₁₂ × Z₁₂:

• (x⁴y⁹, x⁹y⁶) = ((4,9), (9,6))
• (y³, x¹¹) = ((0,3), (11,0))
• (x⁷, x¹⁰y⁶) = ((7,0), (10,6))
• (x⁸y³, x¹⁰y⁶) = ((8,3), (10,6))
• (1, x⁸) = ((0,0), (8,0))
• (x², x⁶y³) = ((2,0), (6,3)) with multiplicity 2

Equations

• BivariateBicycle.DoubleGrossCode.dblExpansionEdges = [((4, 9), 9, 6), ((0, 3), 11, 0), ((7, 0), 10, 6), ((8, 3), 10, 6), ((0, 0), 8, 0), ((2, 0), 6, 3)]

def BivariateBicycle.DoubleGrossCode.dblIsExpansionEdge (γ δ : DGMonomial) : Bool

Whether (γ, δ) is one of the 6 distinct expansion edges (unordered).

Equations

• One or more equations did not get rendered due to their size.

The gauging graph adjacency

def BivariateBicycle.DoubleGrossCode.dblGaugingAdj (γ δ : DGMonomial) : Prop

The full adjacency: matching edges OR expansion edges, with γ ≠ δ.

Equations

• One or more equations did not get rendered due to their size.

instance BivariateBicycle.DoubleGrossCode.instDecidableRelDblGaugingAdj : DecidableRel dblGaugingAdj

Equations

• BivariateBicycle.DoubleGrossCode.instDecidableRelDblGaugingAdj x✝¹ x✝ = instDecidableAnd

def BivariateBicycle.DoubleGrossCode.dblGaugingGraph : SimpleGraph DGMonomial

The gauging graph G for measuring X̄_α in the Double Gross code. Vertices are DGMonomial = Z₁₂ × Z₁₂; the "active" vertices are supp(f).

Equations

• One or more equations did not get rendered due to their size.

instance BivariateBicycle.DoubleGrossCode.instDecidableRelDGMonomialAdjDblGaugingGraph : DecidableRel dblGaugingGraph.Adj

Equations

• BivariateBicycle.DoubleGrossCode.instDecidableRelDGMonomialAdjDblGaugingGraph = inferInstanceAs (DecidableRel BivariateBicycle.DoubleGrossCode.dblGaugingAdj)

Edge counts

theorem BivariateBicycle.DoubleGrossCode.dblMatching_edges_count : {e ∈ dblGaugingGraph.edgeFinset | (!dblExpansionEdges.any fun (x : DGMonomial × DGMonomial) => match x with | (a, b) => decide (e = s(a, b)) || decide (e = s(b, a))) = true}.card = 27

The number of matching edges is 27.

theorem BivariateBicycle.DoubleGrossCode.dblExpansion_edges_count : {e ∈ dblGaugingGraph.edgeFinset | (dblExpansionEdges.any fun (x : DGMonomial × DGMonomial) => match x with | (a, b) => decide (e = s(a, b)) || decide (e = s(b, a))) = true}.card = 6

The number of distinct expansion edges in the graph is 6.

theorem BivariateBicycle.DoubleGrossCode.dblGaugingEdges_card : dblGaugingGraph.edgeFinset.card = 33

The gauging graph has 33 distinct edges (as a SimpleGraph). Counting multiplicity (one double edge), we get 34.

theorem BivariateBicycle.DoubleGrossCode.dblGaugingEdges_with_multiplicity : dblGaugingGraph.edgeFinset.card + 1 = 34

The total edge count with multiplicity is 34. The SimpleGraph has 33 edges, plus one edge (x², x⁶y³) has multiplicity 2.

Expansion edges are valid

theorem BivariateBicycle.DoubleGrossCode.dblExpansion_edges_valid (p : DGMonomial × DGMonomial) : p ∈ dblExpansionEdges → dblGaugingGraph.Adj p.1 p.2

All 6 distinct expansion edges are edges of the gauging graph.

theorem BivariateBicycle.DoubleGrossCode.dblExpansion_edges_in_support (p : DGMonomial × DGMonomial) : p ∈ dblExpansionEdges → p.1 ∈ dblGaugingVertices ∧ p.2 ∈ dblGaugingVertices

All expansion edge endpoints are in supp(f).

Graph connectivity and cycle rank

The gauging graph restricted to supp(f) must be connected. The cycle rank (first Betti number) for a connected graph is |E| - |V| + 1. With the multigraph edge (multiplicity 2 for one edge), the effective number of edges is |E_mult| = 34, so the cycle rank is 34 - 18 + 1 = 17. The paper states that 13 of these 17 independent cycles suffice for the flux checks, because 4 cycles become redundant due to dependencies among Z checks of the original code when restricted to supp(f).

theorem BivariateBicycle.DoubleGrossCode.dblGaugingGraph_connected_on_support : BivariateBicycle.DoubleGrossCode.dblAllReachable✝ (0, 0) BivariateBicycle.DoubleGrossCode.dblGaugingVertexList✝ = true

The gauging graph is connected on the 18-vertex support of f. We verify by BFS from the vertex (0, 0) ∈ supp(f).

theorem BivariateBicycle.DoubleGrossCode.dblCycleRank_simple : dblGaugingGraph.edgeFinset.card + 1 = dblGaugingVertices.card + 16

Euler's formula: the cycle rank of the gauging graph (restricted to supp(f)) is |E| - |V| + 1 = 33 - 18 + 1 = 16 for the simple graph. With multiplicity (one double edge), the effective cycle rank is 34 - 18 + 1 = 17.

theorem BivariateBicycle.DoubleGrossCode.dblCycleRank_with_multiplicity : dblGaugingGraph.edgeFinset.card + 1 + 1 = dblGaugingVertices.card + 17

theorem BivariateBicycle.DoubleGrossCode.dblFluxChecks_le_cycleRank : 13 ≤ 17

The number of flux checks (13) is bounded by the cycle rank with multiplicity (17). The paper states 13 cycles suffice because 4 of the 17 become redundant due to dependencies among Z checks restricted to supp(f).

Overhead calculation

The overhead uses 13 flux checks (not the full cycle rank of 17) because the paper shows that 4 cycles become redundant from Z-check dependencies on the original code restricted to supp(f).

theorem BivariateBicycle.DoubleGrossCode.dblAdditional_gauss_checks : dblGaugingVertices.card = 18

Additional Gauss's law checks (A_v): one per vertex of G = 18.

theorem BivariateBicycle.DoubleGrossCode.dblRestrictedZCheckRank_eq : BivariateBicycle.DoubleGrossCode.dblRestrictedZCheckRank✝ = 17

The restricted Z-check matrix has rank 17. For a connected 18-vertex subgraph, the boundary map has rank |V| - 1 = 17, which matches.

theorem BivariateBicycle.DoubleGrossCode.dblNumFluxChecks_upper_bound : dblGaugingGraph.edgeFinset.card + 1 - BivariateBicycle.DoubleGrossCode.dblRestrictedZCheckRank✝ = 17

The number of independent flux checks = |E_mult| - restricted_Z_rank = 34 - 17 = 17 for the full cycle space. The paper shows 4 of these are already implied by original code Z checks, leaving 13 independent flux checks needed.

theorem BivariateBicycle.DoubleGrossCode.dblAdditional_qubits : dblGaugingGraph.edgeFinset.card + 1 = 34

Additional qubits (one per edge of G, counting multiplicity): 34.

theorem BivariateBicycle.DoubleGrossCode.dblTotal_overhead : dblGaugingVertices.card + 13 + (dblGaugingGraph.edgeFinset.card + 1) = 65

Total overhead: 18 + 13 + 34 = 65 additional checks and qubits. The 13 comes from the paper's claim that 13 of the 17 independent cycles (cycle rank with multiplicity) suffice for the flux checks.

Tanner expansion property

theorem BivariateBicycle.DoubleGrossCode.dblLogicalXBar_tanner_expansion_insufficient (α : DGMonomial) : (dblLogicalXBar α).weight = 18 ∧ (dblLogicalXBar α).zVec = 0 ∧ (∀ (δ : DGMonomial), (dblLogicalXBar α).xVec (Sum.inr δ) = 0) ∧ {γ : DGMonomial | doubleGrossA γ ≠ 0}.card = 3

Key property (Remark 22): X̄_α has weight 18, is pure X-type, and acts only on L qubits. Each L qubit participates in at most |supp(A)| = 3 X-type checks.

Check weight

theorem BivariateBicycle.DoubleGrossCode.dblXCheck_weight (α : DGMonomial) : (bbCheckX doubleGrossA doubleGrossB α).weight = 6

Each X check of the Double Gross code has weight 6.

Summary

theorem BivariateBicycle.DoubleGrossCode.doubleGrossCode_parameters : doubleGrossCode.numQubits = 288 ∧ doubleGrossCode.numChecks = 288

The Double Gross code has 288 qubits and 288 checks.

theorem BivariateBicycle.DoubleGrossCode.dblGauging_construction_summary : dblGaugingVertices.card = 18 ∧ dblGaugingGraph.edgeFinset.card = 33 ∧ dblGaugingGraph.edgeFinset.card + 1 = 34 ∧ dblGaugingGraph.edgeFinset.card + 1 + 1 = dblGaugingVertices.card + 17 ∧ 13 ≤ 17 ∧ dblGaugingVertices.card + 13 + (dblGaugingGraph.edgeFinset.card + 1) = 65

Summary of the gauging construction for X̄_α in the Double Gross code.