Remark 21: Gauging Measurement Construction for X̄_α in the Gross Code

Statement

Explicit construction of the gauging graph G for measuring X̄_α = X(αf, 0) in the Gross code (Rem_20), with degree bounds on the Tanner graph of the deformed code.

Main Results

• gaugingVertices: the 12 vertices (support of f)
• gaugingAdj: the adjacency relation (18 matching + 4 expansion edges)
• gaugingGraph: the gauging graph as a SimpleGraph
• gaugingCyclesList: the 7 independent cycles
• gaugingVertices_card: |V(G)| = 12
• gaugingEdges_card: |E(G)| = 22
• gaugingCycles_count: 7 independent cycles
• total_overhead: additional checks + qubits = 41

The gauging graph vertices

def BivariateBicycle.GrossCode.gaugingVertices : Finset GrossMonomial

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

Equations

• BivariateBicycle.GrossCode.gaugingVertices = {γ : BivariateBicycle.GrossCode.GrossMonomial | BivariateBicycle.GrossCode.grossF γ ≠ 0}

theorem BivariateBicycle.GrossCode.gaugingVertices_card : gaugingVertices.card = 12

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

@[simp]

theorem BivariateBicycle.GrossCode.mem_gaugingVertices (γ : GrossMonomial) : γ ∈ gaugingVertices ↔ grossF γ ≠ 0

Matching edge condition

Two vertices γ, δ ∈ supp(f) share a Z check iff γ - δ = -B_i + B_j for B_i, B_j ∈ {y³, x², x} (the monomial terms of B = y³ + x² + x), with γ ≠ δ.

def BivariateBicycle.GrossCode.isMatchingDiff (d : GrossMonomial) : 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.GrossCode.isMatchingEdge (γ δ : GrossMonomial) : Bool

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

Equations

• BivariateBicycle.GrossCode.isMatchingEdge γ δ = (BivariateBicycle.GrossCode.grossF γ != 0 && BivariateBicycle.GrossCode.grossF δ != 0 && BivariateBicycle.GrossCode.isMatchingDiff (γ - δ))

Expansion edges

def BivariateBicycle.GrossCode.expansionEdges : List (GrossMonomial × GrossMonomial)

The 4 expansion edges ensuring the deformed code has distance 12.

Equations

• BivariateBicycle.GrossCode.expansionEdges = [((2, 0), 5, 3), ((2, 0), 6, 0), ((5, 3), 11, 3), ((7, 3), 11, 3)]

def BivariateBicycle.GrossCode.isExpansionEdge (γ δ : GrossMonomial) : Bool

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

Equations

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

The gauging graph adjacency

def BivariateBicycle.GrossCode.gaugingAdj (γ δ : GrossMonomial) : Prop

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

Equations

• BivariateBicycle.GrossCode.gaugingAdj γ δ = (γ ≠ δ ∧ (BivariateBicycle.GrossCode.isMatchingEdge γ δ || BivariateBicycle.GrossCode.isExpansionEdge γ δ) = true)

instance BivariateBicycle.GrossCode.instDecidableRelGaugingAdj : DecidableRel gaugingAdj

Equations

• BivariateBicycle.GrossCode.instDecidableRelGaugingAdj x✝¹ x✝ = instDecidableAnd

def BivariateBicycle.GrossCode.gaugingGraph : SimpleGraph GrossMonomial

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

Equations

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

instance BivariateBicycle.GrossCode.instDecidableRelGrossMonomialAdjGaugingGraph : DecidableRel gaugingGraph.Adj

Equations

• BivariateBicycle.GrossCode.instDecidableRelGrossMonomialAdjGaugingGraph = inferInstanceAs (DecidableRel BivariateBicycle.GrossCode.gaugingAdj)

Edge count

theorem BivariateBicycle.GrossCode.gaugingEdges_card : gaugingGraph.edgeFinset.card = 22

The gauging graph has exactly 22 edges.

The 7 independent cycles

def BivariateBicycle.GrossCode.gaugingCyclesList : List (List GrossMonomial)

The 7 independent cycles for the flux checks, as lists of vertices. Each list [v₁, v₂, ..., vₖ] represents the cycle v₁ → v₂ → ⋯ → vₖ → v₁.

Equations

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

theorem BivariateBicycle.GrossCode.gaugingCycles_count : gaugingCyclesList.length = 7

7 independent cycles are listed.

theorem BivariateBicycle.GrossCode.gaugingCycles_vertices_in_support (cyc : List GrossMonomial) : cyc ∈ gaugingCyclesList → ∀ v ∈ cyc, v ∈ gaugingVertices

Each vertex in the cycles is in the support of f.

theorem BivariateBicycle.GrossCode.gaugingCycles_length_ge_3 (cyc : List GrossMonomial) : cyc ∈ gaugingCyclesList → 3 ≤ cyc.length

Each cycle has at least 3 vertices.

theorem BivariateBicycle.GrossCode.gaugingCycles_edges_valid (cyc : List GrossMonomial) : cyc ∈ gaugingCyclesList → ∀ (i : Fin cyc.length), gaugingGraph.Adj cyc[i] cyc[⟨(↑i + 1) % cyc.length, ⋯⟩]

Consecutive vertices in each cycle are adjacent in the gauging graph.

Cycle properties

theorem BivariateBicycle.GrossCode.gaugingCycles_short (cyc : List GrossMonomial) : cyc ∈ gaugingCyclesList → cyc.length = 3 ∨ cyc.length = 4

All cycles have length 3 or 4.

theorem BivariateBicycle.GrossCode.gaugingCycles_max_length (cyc : List GrossMonomial) : cyc ∈ gaugingCyclesList → cyc.length ≤ 4

The maximum cycle length is 4.

Euler's formula

theorem BivariateBicycle.GrossCode.cycle_space_dim : gaugingGraph.edgeFinset.card + 1 = gaugingVertices.card + 11

The cycle space dimension by Euler's formula: |E| - |V| + 1 = 22 - 12 + 1 = 11.

Overhead calculation

theorem BivariateBicycle.GrossCode.additional_gauss_checks : gaugingVertices.card = 12

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

theorem BivariateBicycle.GrossCode.additional_flux_checks : gaugingCyclesList.length = 7

Additional flux checks (B_p): one per independent cycle = 7.

theorem BivariateBicycle.GrossCode.additional_qubits : gaugingGraph.edgeFinset.card = 22

Additional qubits (edge qubits): one per edge of G = 22.

theorem BivariateBicycle.GrossCode.total_overhead : gaugingVertices.card + gaugingCyclesList.length + gaugingGraph.edgeFinset.card = 41

Total overhead: 12 + 7 + 22 = 41 additional checks and qubits.

Expansion edges are valid

theorem BivariateBicycle.GrossCode.expansion_edges_valid (p : GrossMonomial × GrossMonomial) : p ∈ expansionEdges → gaugingGraph.Adj p.1 p.2

All 4 expansion edges are edges of the gauging graph.

theorem BivariateBicycle.GrossCode.expansion_edges_in_support (p : GrossMonomial × GrossMonomial) : p ∈ expansionEdges → p.1 ∈ gaugingVertices ∧ p.2 ∈ gaugingVertices

All expansion edge endpoints are in supp(f).

Degree bounds

theorem BivariateBicycle.GrossCode.gaugingDegree_le_six (v : GrossMonomial) : gaugingGraph.degree v ≤ 6

The maximum degree in the gauging graph is at most 6.

Matching edges

theorem BivariateBicycle.GrossCode.matching_edges_count : {e ∈ gaugingGraph.edgeFinset | (!expansionEdges.any fun (x : GrossMonomial × GrossMonomial) => match x with | (a, b) => decide (e = s(a, b)) || decide (e = s(b, a))) = true}.card = 18

The number of matching edges is 18.

theorem BivariateBicycle.GrossCode.expansion_edges_count : {e ∈ gaugingGraph.edgeFinset | (expansionEdges.any fun (x : GrossMonomial × GrossMonomial) => match x with | (a, b) => decide (e = s(a, b)) || decide (e = s(b, a))) = true}.card = 4

The number of expansion edges is 4.

Adjacency between logical support and Z checks

theorem BivariateBicycle.GrossCode.adjacent_z_checks_count : {β : GrossMonomial | {γ ∈ gaugingVertices | grossB (β - γ) ≠ 0}.card ≥ 1}.card = 18

The number of Z checks adjacent to the support of X̄_α is 18.

Summary

theorem BivariateBicycle.GrossCode.gauging_construction_summary : gaugingVertices.card = 12 ∧ gaugingGraph.edgeFinset.card = 22 ∧ gaugingCyclesList.length = 7 ∧ gaugingVertices.card + gaugingCyclesList.length + gaugingGraph.edgeFinset.card = 41 ∧ (∀ (v : GrossMonomial), gaugingGraph.degree v ≤ 6) ∧ ∀ cyc ∈ gaugingCyclesList, cyc.length ≤ 4

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