MerLean-example

47 Rem 22: Gross Code Gauging Example

This chapter provides a concrete example demonstrating the efficiency of the gauging approach, applied to measuring the logical operator \(\bar{X}_\alpha \) in the Gross code. The gauging graph construction is detailed, along with overhead calculations showing a significant improvement over previous schemes.

Definition 1526 Logical Weight
#

The weight of the logical operator \(\bar{X}_\alpha = X(\alpha f, 0)\), equal to the number of monomials in \(f\):

\[ W := 12. \]
Definition 1527 Code Distance

The code distance of the Gross code:

\[ d := 12. \]
Theorem 1528 Logical Weight Equals Distance

The weight of \(\bar{X}_\alpha \) equals the code distance: \(W = d\).

Proof

This holds by definitional equality, since both \(W\) and \(d\) are defined to be \(12\).

Definition 1529 Gross Gauging Graph

The structure recording the parameters of the gauging graph for \(\bar{X}_\alpha \) in the Gross code. It consists of:

  • numVertices : the number of vertices (monomials in \(f\)),

  • numInitialEdges : the number of initial edges from \(Z\)-check connectivity,

  • numExpansionEdges : the number of additional expansion edges,

  • numRedundantCycles : the number of redundant cycles from the BB code’s \(Z\)-check structure,

  • maxNewDegree : the maximum Tanner graph degree for new elements,

  • maxAffectedDegree : the maximum Tanner graph degree for affected existing elements.

Definition 1530 Concrete Gross Gauging Graph

The concrete gauging graph for \(\bar{X}_\alpha \) in the Gross code, with parameters:

  • \(|V| = 12\) vertices,

  • \(18\) initial edges from \(Z\)-check connectivity,

  • \(4\) expansion edges,

  • \(4\) redundant cycles,

  • maximum new degree \(6\),

  • maximum affected degree \(7\).

Theorem 1531 Number of Vertices

The gauging graph has \(12\) vertices: \(\texttt{grossGaugingGraph.numVertices} = 12\).

Proof

This holds by reflexivity from the definition.

Theorem 1532 Number of Initial Edges

The gauging graph has \(18\) initial edges: \(\texttt{grossGaugingGraph.numInitialEdges} = 18\).

Proof

This holds by reflexivity from the definition.

Theorem 1533 Number of Expansion Edges

The gauging graph has \(4\) expansion edges: \(\texttt{grossGaugingGraph.numExpansionEdges} = 4\).

Proof

This holds by reflexivity from the definition.

Theorem 1534 Vertices Equal Logical Weight

The vertices of the graph correspond to monomials in \(f\), so \(|V| = W\):

\[ \texttt{grossGaugingGraph.numVertices} = \texttt{logicalWeight}. \]
Proof

This holds by reflexivity, since both sides equal \(12\).

Definition 1535 Total Number of Edges

The total number of edges in the gauging graph:

\[ |E| = \texttt{numInitialEdges} + \texttt{numExpansionEdges}. \]
Theorem 1536 Total Edges Equal 22

The total number of edges in the gauging graph is \(22\):

\[ |E| = 18 + 4 = 22. \]
Proof

This holds by reflexivity from the definitions.

Theorem 1537 Edge Decomposition

The total edges decompose as initial plus expansion:

\[ |E| = |E_{\text{initial}}| + |E_{\text{expansion}}|. \]
Proof

This holds by reflexivity from the definition of numTotalEdges.

Definition 1538 Number of Independent Cycles

The number of independent cycles in the gauging graph, computed via Euler’s formula for connected graphs:

\[ \text{numIndependentCycles} = |E| - |V| + 1. \]
Theorem 1539 Independent Cycles Equal 11

The gauging graph has \(11\) independent cycles:

\[ 22 - 12 + 1 = 11. \]
Proof

This holds by reflexivity from the definitions.

Theorem 1540 Euler’s Formula Check

Euler’s formula gives \(|E| - |V| + 1 = 22 - 12 + 1 = 11\).

Proof

By numerical computation, \(22 - 12 + 1 = 11\).

Definition 1541 Number of Needed Flux Checks

The number of needed \(B_p\) flux checks, after accounting for redundancy from the BB code’s \(Z\) checks:

\[ \text{numNeededFluxChecks} = \text{numIndependentCycles} - \text{numRedundantCycles}. \]
Theorem 1542 Needed Flux Checks Equal 7

Only \(7\) independent \(B_p\) checks are needed: \(11 - 4 = 7\).

Proof

This holds by reflexivity from the definitions.

Theorem 1543 Flux Check Reduction

The redundancy reduces \(11\) cycles to \(7\) checks:

\[ \text{numIndependentCycles} - \text{numRedundantCycles} = 11 - 4 = 7. \]
Proof

This holds by reflexivity.

Definition 1544 Number of New X Checks

The number of new \(X\) checks equals the number of vertices (one Gauss’s law operator \(A_v\) per vertex):

\[ \text{numNewXChecks} = |V|. \]
Definition 1545 Number of New Z Checks

The number of new \(Z\) checks equals the number of needed flux checks:

\[ \text{numNewZChecks} = \text{numNeededFluxChecks}. \]
Definition 1546 Number of New Qubits

The number of new qubits equals the total number of edges (one gauge qubit per edge):

\[ \text{numNewQubits} = |E|. \]
Theorem 1547 New X Checks Equal 12

The number of new \(X\) checks is \(12\).

Proof

This holds by reflexivity from the definitions.

Theorem 1548 New Z Checks Equal 7

The number of new \(Z\) checks is \(7\).

Proof

This holds by reflexivity from the definitions.

Theorem 1549 New Qubits Equal 22

The number of new qubits is \(22\).

Proof

This holds by reflexivity from the definitions.

Definition 1550 Total Overhead

The total overhead of the gauging approach:

\[ \text{totalOverhead} = \text{numNewXChecks} + \text{numNewZChecks} + \text{numNewQubits}. \]
Theorem 1551 Total Overhead Equals 41

The total overhead is \(41\):

\[ 12 + 7 + 22 = 41. \]
Proof

This holds by reflexivity from the definitions.

The total overhead decomposes into its three components:

\[ \text{totalOverhead} = \text{numNewXChecks} + \text{numNewZChecks} + \text{numNewQubits}. \]
Proof

This holds by reflexivity from the definition of totalOverhead.

Definition 1553 Previous Scheme Overhead

The overhead of previous schemes, which scales as \(O(Wd)\) where \(W\) is the logical operator weight and \(d\) is the code distance:

\[ \text{previousSchemeOverhead} = W \cdot d = 12 \times 12 = 144. \]
Theorem 1554 Previous Scheme Overhead Equals 144

The previous scheme overhead is \(144\).

Proof

This holds by reflexivity, since \(12 \times 12 = 144\).

The gauging overhead (\(41\)) is strictly less than the previous scheme overhead (\(144\)):

\[ \text{totalOverhead}(\text{grossGaugingGraph}) {\lt} \text{previousSchemeOverhead}. \]
Proof

By numerical computation, \(41 {\lt} 144\).

The gauging overhead is less than \(29\% \) of the previous scheme overhead:

\[ 100 \cdot \text{totalOverhead}(\text{grossGaugingGraph}) {\lt} 29 \cdot \text{previousSchemeOverhead}. \]
Proof

By numerical computation, \(100 \times 41 = 4100 {\lt} 4176 = 29 \times 144\).

The gauging approach saves \(103\) elements compared to previous schemes:

\[ \text{previousSchemeOverhead} - \text{totalOverhead}(\text{grossGaugingGraph}) = 144 - 41 = 103. \]
Proof

By numerical computation, \(144 - 41 = 103\).

Theorem 1558 New Elements Degree Bound

New checks and qubits have Tanner graph degree at most \(6\):

\[ \texttt{grossGaugingGraph.maxNewDegree} \leq 6. \]
Proof

By numerical computation, \(6 \leq 6\).

Theorem 1559 Affected Elements Degree Bound

Affected existing elements (the \(12\) qubits in \(\bar{X}_\alpha \) and the \(18\) adjacent \(Z\) checks) have degree at most \(7\):

\[ \texttt{grossGaugingGraph.maxAffectedDegree} \leq 7. \]
Proof

By numerical computation, \(7 \leq 7\).

Theorem 1560 Degree Increase

The degree increase for affected elements is exactly \(1\) (from \(6\) to \(7\)):

\[ \texttt{maxAffectedDegree} - \texttt{maxNewDegree} = 7 - 6 = 1. \]
Proof

By numerical computation, \(7 - 6 = 1\).

Definition 1561 Gross Monomial Type
#

The type alias for monomials in the Gross code group:

\[ \texttt{GrossMon} := \mathbb {Z}/12\mathbb {Z} \times \mathbb {Z}/6\mathbb {Z}. \]
Definition 1562 Expansion Edge 1

Expansion edge 1 connects \(x^2\) and \(x^5 y^3\):

\[ \text{expansionEdge1} = ((2, 0), (5, 3)). \]
Definition 1563 Expansion Edge 2

Expansion edge 2 connects \(x^2\) and \(x^6\):

\[ \text{expansionEdge2} = ((2, 0), (6, 0)). \]
Definition 1564 Expansion Edge 3

Expansion edge 3 connects \(x^5 y^3\) and \(x^{11} y^3\):

\[ \text{expansionEdge3} = ((5, 3), (11, 3)). \]
Definition 1565 Expansion Edge 4

Expansion edge 4 connects \(x^7 y^3\) and \(x^{11} y^3\):

\[ \text{expansionEdge4} = ((7, 3), (11, 3)). \]
Theorem 1566 Expansion Edge 1 Distinct

The endpoints of expansion edge 1 are distinct: \((2, 0) \neq (5, 3)\).

Proof

This is verified by computation (decide).

Theorem 1567 Expansion Edge 2 Distinct

The endpoints of expansion edge 2 are distinct: \((2, 0) \neq (6, 0)\).

Proof

This is verified by computation (decide).

Theorem 1568 Expansion Edge 3 Distinct

The endpoints of expansion edge 3 are distinct: \((5, 3) \neq (11, 3)\).

Proof

This is verified by computation (decide).

Theorem 1569 Expansion Edge 4 Distinct

The endpoints of expansion edge 4 are distinct: \((7, 3) \neq (11, 3)\).

Proof

This is verified by computation (decide).

The list of expansion edges has exactly \(4\) elements.

Proof

This holds by reflexivity, since \([\text{e}_1, \text{e}_2, \text{e}_3, \text{e}_4].\text{length} = 4\).

Definition 1571 Monomials of \(f\)

The \(12\) monomials appearing in \(f\), represented as elements of \(\mathbb {Z}/12\mathbb {Z} \times \mathbb {Z}/6\mathbb {Z}\):

\[ \{ (0,0),\, (1,0),\, (2,0),\, (3,0),\, (6,0),\, (7,0),\, (8,0),\, (9,0),\, (1,3),\, (5,3),\, (7,3),\, (11,3)\} . \]

These correspond to the monomials of \(f = 1 + x + x^2 + x^3 + x^6 + x^7 + x^8 + x^9 + (x + x^5 + x^7 + x^{11})y^3\).

Theorem 1572 Monomials of \(f\) Count

The polynomial \(f\) has exactly \(12\) monomials: \(|\text{monomialsOfF}| = 12\).

Proof

This holds by reflexivity from the list definition.

Theorem 1573 Monomials Count Equals Vertices

The number of monomials equals the number of graph vertices:

\[ |\text{monomialsOfF}| = |V|. \]
Proof

This holds by reflexivity, since both sides equal \(12\).

Theorem 1574 Monomials of \(f\) Are Distinct

All monomials in \(f\) are distinct (the list has no duplicates).

Proof

This is verified by computation (decide).

Definition 1575 Number of Adjacent Z Checks

The number of \(Z\) checks adjacent to \(\bar{X}_\alpha \):

\[ \text{numAdjacentZChecks} := 18. \]

These arise from the connectivity condition: vertices \(\gamma , \delta \in f\) are connected if \(\gamma = B_i^T B_j \delta \) for some \(i, j \in \{ 1,2,3\} \).

Theorem 1576 Adjacent Checks Equal Initial Edges

The number of adjacent \(Z\) checks equals the number of initial edges:

\[ \text{numAdjacentZChecks} = \text{numInitialEdges} = 18. \]
Proof

This holds by reflexivity.

Definition 1577 Target Distance

The target distance for the gauging graph, set to match the Gross code distance:

\[ \text{targetDistance} := 12. \]
Theorem 1578 Target Distance Equals Code Distance

The target distance equals the Gross code distance: \(\text{targetDistance} = d\).

Proof

This holds by reflexivity.

Theorem 1579 Target Distance Equals Number of Vertices

The target distance equals the number of vertices (a coincidence for this code):

\[ \text{targetDistance} = |V| = 12. \]
Proof

This holds by reflexivity.

Theorem 1580 X Checks from Gauss’s Law

The number of new \(X\) checks equals the number of vertices (one Gauss’s law operator \(A_v\) per vertex):

\[ \text{numNewXChecks} = |V|. \]
Proof

This holds by reflexivity from the definition.

The number of new \(Z\) checks is determined by cycle analysis:

\[ \text{numNewZChecks} = \text{numNeededFluxChecks}. \]
Proof

This holds by reflexivity from the definition.

The number of new qubits equals the total edges (one gauge qubit per edge):

\[ \text{numNewQubits} = |E|. \]
Proof

This holds by reflexivity from thedefinition.

Theorem 1583 Overhead Sum Check

All three overhead components add to \(41\): \(12 + 7 + 22 = 41\).

Proof

By numerical computation, \(12 + 7 + 22 = 41\).

Theorem 1584 Vertices Match Gross Code Distance

The number of vertices matches the Gross code’s distance parameter:

\[ |V| = d_{\text{GrossCode}}. \]
Proof

By simplification using the definition of grossCodeParams, both sides equal \(12\).

Theorem 1585 Previous Overhead Is \(Wd\)

The previous scheme overhead equals \(d \times d = d^2\):

\[ \text{previousSchemeOverhead} = d_{\text{GrossCode}}^2. \]
Proof

By simplification using the definitions of previousSchemeOverhead, logicalWeight, codeDistance, and grossCodeParams, both sides equal \(144\).

Theorem 1586 Previous Overhead Equals \(n\)

The previous scheme overhead equals the number of physical qubits \(n\) of the Gross code:

\[ \text{previousSchemeOverhead} = n_{\text{GrossCode}} = 144. \]
Proof

By simplification using the definitions, both sides equal \(144\).

Theorem 1587 Overhead At Most 41

The gauging overhead is at most \(41\):

\[ \text{totalOverhead}(\text{grossGaugingGraph}) \leq 41. \]
Proof

This follows by reflexivity of \(\leq \) since both sides equal \(41\).

The gauging overhead is less than \(1/3\) of the previous scheme overhead:

\[ 3 \cdot \text{totalOverhead}(\text{grossGaugingGraph}) {\lt} \text{previousSchemeOverhead}. \]
Proof

By numerical computation, \(3 \times 41 = 123 {\lt} 144\).

The gauging overhead is strictly less than half the previous scheme overhead:

\[ 2 \cdot \text{totalOverhead}(\text{grossGaugingGraph}) {\lt} \text{previousSchemeOverhead}. \]
Proof

By numerical computation, \(2 \times 41 = 82 {\lt} 144\).