44 Rem 22: The Double Gross Code Definition
The Double Gross code is a \([\! [288, 12, 18]\! ]\) bivariate bicycle (BB) code with parameters \(\ell = 12\), \(m = 12\), \(A = x^3 + y^7 + y^2\), \(B = y^3 + x^2 + x\). The logical operators take the form \(\bar{X}_\alpha = X(\alpha f, 0)\) where \(f\) has weight 18. The gauging measurement construction involves 18 vertices (the support of \(f\)), 27 matching edges plus 7 expansion edges (one double edge, for 34 edges counting multiplicity), and 13 independent cycles (out of a cycle rank of 17). The total overhead is \(18 + 13 + 34 = 65\).
44.1 Code Parameters
The monomial group for the Double Gross code is \(\operatorname {DGMonomial} := \operatorname {BBMonomial}(12, 12) = \mathbb {Z}_{12} \times \mathbb {Z}_{12}\).
The group algebra for the Double Gross code is \(\operatorname {DGAlgebra} := \operatorname {BBGroupAlgebra}(12, 12) = \mathbb {F}_2[x,y]/(x^{12} - 1, y^{12} - 1)\).
The qubit type for the Double Gross code is \(\operatorname {DGQubit} := \operatorname {BBQubit}(12, 12)\).
The polynomial \(A = x^3 + y^7 + y^2\) in \(\mathbb {F}_2[x,y]/(x^{12} - 1, y^{12} - 1)\), defined as
The polynomial \(B = y^3 + x^2 + x\) in \(\mathbb {F}_2[x,y]/(x^{12} - 1, y^{12} - 1)\), defined as
44.2 Check Commutation
For all \(\alpha , \beta \in \operatorname {DGMonomial}\), the X-type check \(\operatorname {bbCheckX}(A, B, \alpha )\) and the Z-type check \(\operatorname {bbCheckZ}(A, B, \beta )\) commute as Pauli operators.
We use classical logic and rewrite with the commutation criterion bbCheckXZ_commute_iff, which reduces the Pauli commutation condition to a sum-of-products identity over the monomial group. The resulting identity
for all \(\alpha , \beta \) is verified by native_decide.
For all check indices \(i, j \in \operatorname {BBCheckIndex}(12, 12)\), the checks \(\operatorname {bbCheck}(A, B, i)\) and \(\operatorname {bbCheck}(A, B, j)\) commute.
We case-split on the check indices \(i\) and \(j\), each of which is either \(\operatorname {inl}(\alpha )\) (X-type) or \(\operatorname {inr}(\beta )\) (Z-type):
Case \((\operatorname {inl}(\alpha _1), \operatorname {inl}(\alpha _2))\): Both are X-type checks, and their commutation follows from bbCheckX_commute.
Case \((\operatorname {inl}(\alpha ), \operatorname {inr}(\beta ))\): An X-type and Z-type check commute by doubleGrossChecks_XZ_commute.
Case \((\operatorname {inr}(\beta ), \operatorname {inl}(\alpha ))\): By commutativity of Pauli commutation and the previous case.
Case \((\operatorname {inr}(\beta _1), \operatorname {inr}(\beta _2))\): Both are Z-type checks, and their commutation follows from bbCheckZ_commute.
44.3 The Double Gross Stabilizer Code
The Double Gross code is a stabilizer code on qubits \(\operatorname {DGQubit}\), with check index set \(I = \operatorname {BBCheckIndex}(12, 12)\), check map \(\operatorname {bbCheck}(A, B)\), and commutation proof from the theorem above.
The Double Gross code has \(n = 288 = 2 \times 12 \times 12\) physical qubits.
By simplification using the definition of numQubits, the cardinality of the sum type, and the cardinality of the product \(\mathbb {Z}_{12} \times \mathbb {Z}_{12}\), we obtain \(|\operatorname {Fin}(12) \times \operatorname {Fin}(12)| + |\operatorname {Fin}(12) \times \operatorname {Fin}(12)| = 144 + 144 = 288\). The result follows by numerical computation.
The Double Gross code has 288 checks: 144 X-type and 144 Z-type.
By simplification using the definition of numChecks and the cardinality of \(\operatorname {BBCheckIndex}(12, 12) = (\mathbb {Z}_{12} \times \mathbb {Z}_{12}) \oplus (\mathbb {Z}_{12} \times \mathbb {Z}_{12})\), we obtain \(144 + 144 = 288\) by numerical computation.
The Double Gross code encodes \(k = 12\) logical qubits. This is computed as \(k = 2 \times \operatorname {nullity}([A; B])\), where \([A; B]\) is the stacked convolution matrix of size \(288 \times 144\) over \(\mathbb {F}_2\). The rank of \([A; B]\) is 138, so the nullity is \(144 - 138 = 6\), giving \(k = 2 \times 6 = 12\). The factor of 2 comes from the CSS structure (6 X-type + 6 Z-type independent logical operators).
Rewriting with the computed rank \(\operatorname {f2GaussRank}(144, \text{rows}) = 138\) (verified by native_decide via Gaussian elimination over \(\mathbb {F}_2\)), we obtain \(2 \times (144 - 138) = 2 \times 6 = 12\).
44.4 Logical Operator Polynomial
The logical operator polynomial \(f \in \mathbb {F}_2[x,y]/(x^{12} - 1, y^{12} - 1)\) is defined as:
44.5 Logical X Operators
For \(\alpha \in \operatorname {DGMonomial}\), the logical X operator is \(\bar{X}_\alpha = X(\alpha f, 0) = \operatorname {pauliXBB}(\operatorname {bbShift}(\alpha , f), 0)\).
For all \(\alpha \), the logical operator \(\bar{X}_\alpha \) has no Z-support: \((\bar{X}_\alpha ).\operatorname {zVec} = 0\).
By simplification using the definitions of \(\operatorname {dblLogicalXBar}\) and \(\operatorname {pauliXBB}\), the Z-component is identically zero.
For all \(\alpha \) and all R-type qubits \(\delta \), \((\bar{X}_\alpha ).\operatorname {xVec}(\operatorname {inr}(\delta )) = 0\).
By simplification using the definitions of \(\operatorname {dblLogicalXBar}\) and \(\operatorname {pauliXBB}\), the X-component on R-type qubits is zero.
For all \(\alpha \), \(\bar{X}_\alpha \cdot \bar{X}_\alpha = \mathbf{1}\).
Unfolding\(\operatorname {dblLogicalXBar}\) and applying \(\operatorname {pauliXBB\_ mul}\), we verify equality by extensionality on the X and Z components. For the X-component, we case-split on the qubit type:
For L-type qubits (\(\operatorname {inl}\)): the X-component satisfies \(f(\gamma - \alpha ) + f(\gamma - \alpha ) = 0\) by the characteristic-two identity \(a + a = 0\).
For R-type qubits (\(\operatorname {inr}\)): the X-component is \(0 + 0 = 0\) by the definition of \(\operatorname {pauliXBB}\).
For the Z-component, both sides are zero by the definition of \(\operatorname {pauliXBB}\).
44.6 Support and Weight
The polynomial \(f\) has 18 nonzero coefficients:
This is verified by native_decide, which evaluates \(f\) at all \(144\) monomials in \(\mathbb {Z}_{12} \times \mathbb {Z}_{12}\) and counts the nonzero values.
\(|\{ \gamma : A(\gamma ) \neq 0\} | = 3\).
Verified by native_decide.
\(|\{ \gamma : B(\gamma ) \neq 0\} | = 3\).
Verified by native_decide.
For all \(\alpha \in \operatorname {DGMonomial}\), \(\operatorname {weight}(\bar{X}_\alpha ) = 18\).
Using classical logic, we unfold the weight as the cardinality of the support. We apply the shift-invariance lemma, which shows that the support cardinality of \(\operatorname {pauliXBB}(\operatorname {bbShift}(\alpha , f), 0)\) equals that of \(\operatorname {pauliXBB}(f, 0)\) for any \(\alpha \) (via a bijection \(\gamma \mapsto \gamma - \alpha \) on L-type qubits). The base case \(\operatorname {weight}(\operatorname {pauliXBB}(f, 0)) = 18\) is then verified by native_decide.
44.7 Commutation with Checks
For all \(\alpha , \beta \), \(\bar{X}_\alpha \) commutes with \(\operatorname {bbCheckX}(A, B, \beta )\).
Using classical logic, we simplify the Pauli commutation condition and the symplectic inner product. Since both \(\bar{X}_\alpha \) and \(\operatorname {bbCheckX}(A, B, \beta )\) are pure X-type operators (having no Z-support), their symplectic inner product is trivially zero.
For all \(\alpha , \beta \), \(\bar{X}_\alpha \) commutes with \(\operatorname {bbCheckZ}(A, B, \beta )\).
Using classical logic, we expand the Pauli commutation condition and the symplectic inner product. Unfolding the definitions of \(\bar{X}_\alpha \) (pure X-type) and \(\operatorname {bbCheckZ}\) (pure Z-type), the cross terms reduce the symplectic inner product to:
We split the sum over L and R qubit types using \(\operatorname {Fintype.sum\_ sum\_ type}\); the R-qubit contribution vanishes since \(\bar{X}_\alpha \) has no X-support on R qubits. After re-indexing the sum via the substitution \(\delta = \gamma - \alpha \), we obtain \(\sum _\delta f(\delta ) \cdot B(-(\delta - (\beta - \alpha ))) = 0\), which follows from the kernel condition \(f \in \ker (B^T)\) verified by native_decide.
For all \(\alpha \) and all check indices \(i \in \operatorname {BBCheckIndex}(12, 12)\), \(\bar{X}_\alpha \) commutes with \(\operatorname {bbCheck}(A, B, i)\).
We case-split on the check index \(i\): if \(i = \operatorname {inl}(\beta )\) (X-type), the result follows from dblLogicalXBar_commute_xCheck; if \(i = \operatorname {inr}(\beta )\) (Z-type), the result follows from dblLogicalXBar_commute_zCheck.
For all \(\alpha \), \(\bar{X}_\alpha \) is in the centralizer of the Double Gross code.
Let \(i\) be an arbitrary check index. The commutation \(\bar{X}_\alpha \) with check \(i\) follows directly from dblLogicalXBar_commute_allChecks.
44.8 The Gauging Graph
The gauging vertices are the support of \(f\):
\(|\operatorname {dblGaugingVertices}| = 18\).
Verified by native_decide.
A monomial difference \(d \in \mathbb {Z}_{12} \times \mathbb {Z}_{12}\) satisfies the matching condition if \(d = -B_i + B_j\) for some distinct terms \(B_i, B_j\) of \(B\), where the terms of \(B = y^3 + x^2 + x\) are \((0,3)\), \((2,0)\), and \((1,0)\).
Two monomials \(\gamma , \delta \) form a matching edge if both lie in \(\operatorname {supp}(f)\) and share a Z check, i.e., \(f(\gamma ) \neq 0\), \(f(\delta ) \neq 0\), and \(\operatorname {dblIsMatchingDiff}(\gamma - \delta )\).
The 6 distinct expansion edges (as ordered pairs in \(\mathbb {Z}_{12} \times \mathbb {Z}_{12}\)):
The edge \((x^2, x^6 y^3)\) has multiplicity 2 in the paper’s construction (yielding 7 expansion edges counting multiplicity).
\(\operatorname {dblIsExpansionEdge}(\gamma , \delta )\) holds iff \((\gamma , \delta )\) or \((\delta , \gamma )\) appears in the expansion edge list.
Two monomials \(\gamma , \delta \) are adjacent in the gauging graph if \(\gamma \neq \delta \) and either they form a matching edge or an expansion edge.
The gauging graph \(G\) for measuring \(\bar{X}_\alpha \) in the Double Gross code is the simple graph on \(\mathbb {Z}_{12} \times \mathbb {Z}_{12}\) with adjacency \(\operatorname {dblGaugingAdj}\). Its symmetry is verified by native_decide, and irreflexivity follows from the \(\gamma \neq \delta \) condition.
44.9 Edge Counts
The gauging graph has 27 matching edges (edges that are not expansion edges).
Verified by native_decide.
The gauging graph has 6 distinct expansion edges.
Verified by native_decide.
The gauging graph has 33 distinct edges as a simple graph. Counting the one double edge \((x^2, x^6 y^3)\) with multiplicity 2, the total is 34.
Verified by native_decide.
\(|\operatorname {edgeFinset}(G)| + 1 = 33 + 1 = 34\).
Rewriting with \(|\operatorname {edgeFinset}(G)| = 33\).
44.10 Expansion Edge Validity
All 6 distinct expansion edges are edges of the gauging graph.
Verified by native_decide.
All expansion edge endpoints lie in \(\operatorname {supp}(f)\).
Verified by native_decide.
44.11 Graph Connectivity and Cycle Rank
The gauging graph is connected on the 18-vertex support of \(f\). This is verified by a BFS traversal starting from the vertex \((0, 0) \in \operatorname {supp}(f)\), confirming that all 18 vertices are reachable.
Verified by native_decide.
By Euler’s formula for a connected graph, the cycle rank (first Betti number) of the simple graph is \(|E| - |V| + 1 = 33 - 18 + 1 = 16\).
Rewriting with \(|E| = 33\) and \(|V| = 18\), we verify \(33 + 1 = 18 + 16\).
With one double edge, the effective cycle rank is \((|E| + 1) - |V| + 1 = 34 - 18 + 1 = 17\).
Rewriting with \(|E| = 33\) and \(|V| = 18\), we verify \((33 + 1) + 1 = 18 + 17\).
The number of flux checks (13) is bounded by the cycle rank with multiplicity (17): \(13 \leq 17\). The paper shows that 13 of the 17 independent cycles suffice because 4 become redundant due to dependencies among Z checks restricted to \(\operatorname {supp}(f)\).
By integer arithmetic, \(13 \leq 17\).
44.12 Overhead Calculation
The number of additional Gauss’s law checks (\(A_v\), one per vertex of \(G\)) is 18.
This is exactly dblGaugingVertices_card.
The restricted Z-check matrix (with rows indexed by \(\beta \in \mathbb {Z}_{12} \times \mathbb {Z}_{12}\) and columns indexed by \(\gamma \in \operatorname {supp}(f)\), with entry \(B(\beta - \gamma ) \neq 0\)) has rank 17. For a connected 18-vertex subgraph, the boundary map has rank \(|V| - 1 = 17\), which matches.
Verified by native_decide via Gaussian elimination over \(\mathbb {F}_2\).
The number of independent flux checks is \(|E_{\text{mult}}| - \operatorname {restrictedZCheckRank} = 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.
Rewriting with \(|E| = 33\) and \(\operatorname {restrictedZCheckRank} = 17\), we verify \((33 + 1) - 17 = 17\).
The number of additional qubits (one per edge of \(G\), counting multiplicity) is 34.
This is exactly dblGaugingEdges_with_multiplicity.
The total overhead is \(|\text{vertices}| + |\text{flux checks}| + |\text{edge qubits}| = 18 + 13 + 34 = 65\). The 13 comes from the paper’s claim that 13 of the 17 independent cycles (cycle rank with multiplicity) suffice for the flux checks.
Rewriting with \(|\operatorname {dblGaugingVertices}| = 18\) and \(|\operatorname {edgeFinset}(G)| = 33\), we verify \(18 + 13 + (33 + 1) = 65\).
44.13 Tanner Expansion Property
For all \(\alpha \): (1) \(\bar{X}_\alpha \) has weight 18, (2) \(\bar{X}_\alpha \) is pure X-type (\(\operatorname {zVec} = 0\)), (3) \(\bar{X}_\alpha \) acts only on L qubits (\(\operatorname {xVec}(\operatorname {inr}(\delta )) = 0\) for all \(\delta \)), and (4) each L qubit participates in at most \(|\operatorname {supp}(A)| = 3\) X-type checks. This shows that the Tanner graph expansion is insufficient: a weight-18 operator only triggers \(\leq 3 \times 18 = 54\) check violations, which may not suffice for robust error detection.
The four properties are assembled from the previously proven theorems: dblLogicalXBar_weight, dblLogicalXBar_pure_X, dblLogicalXBar_acts_only_on_L, and doubleGrossA_support_card.
44.14 Check Weight
Each X-type check of the Double Gross code has weight 6: for all \(\alpha \in \operatorname {DGMonomial}\), \(\operatorname {weight}(\operatorname {bbCheckX}(A, B, \alpha )) = 6\).
Using classical logic, we unfold the weight as the support cardinality. We apply a shift-invariance argument: the support of \(\operatorname {bbCheckX}(A, B, \alpha )\) has the same cardinality as that of \(\operatorname {bbCheckX}(A, B, 0)\), via the injective bijection \(q \mapsto q - \alpha \) on qubit indices (separately on L and R components). The Z-component of an X-type check is zero, so the support reduces to the X-component support. The base case \(\operatorname {weight}(\operatorname {bbCheckX}(A, B, 0)) = 6\) is verified by native_decide.
44.15 Summary
The Double Gross code has 288 qubits and 288 checks: \(n = 288 \land |\text{checks}| = 288\).
This follows directly from doubleGrossCode_numQubits and doubleGrossCode_numChecks.
Summary of the gauging construction for \(\bar{X}_\alpha \) in the Double Gross code:
\(|\operatorname {dblGaugingVertices}| = 18\),
\(|\operatorname {edgeFinset}(G)| = 33\),
\(|\operatorname {edgeFinset}(G)| + 1 = 34\) (with multiplicity),
\((|\operatorname {edgeFinset}(G)| + 1) + 1 = |\operatorname {dblGaugingVertices}| + 17\) (cycle rank),
\(13 \leq 17\) (flux checks \(\leq \) cycle rank),
\(|\operatorname {dblGaugingVertices}| + 13 + (|\operatorname {edgeFinset}(G)| + 1) = 65\) (total overhead).
The six-tuple is assembled directly from the previously proven theorems: dblGaugingVertices_card, dblGaugingEdges_card, dblGaugingEdges_with_multiplicity, dblCycleRank_with_multiplicity, dblFluxChecks_le_cycleRank, and dblTotal_overhead.