Rem_18: Lattice Surgery as Gauging

Statement

Lattice surgery is a special case of gauging measurement. The gauging measurement can be interpreted as a direct generalization of lattice surgery for surface codes.

Example: Measuring X̄₁ ⊗ X̄₂ on a pair of equally sized surface code blocks using a ladder graph G joining the edge qubits produces:

1. A deformed code that is again a surface code on the union of the two patches
2. The final step of measuring out individual edge qubits matches conventional lattice surgery

Non-adjacent patches: Use a graph with a grid of dummy vertices between the two edges.

Generalization: Extends to any pair of matching logical X operators using two copies of graph G with bridge edges. G is allowed to have h(G) < 1 if path-length and cycle-weight desiderata are satisfied.

Insight: h(G) ≥ 1 is overkill; expansion is only needed for subsets of qubits relevant to the logical operators being measured.

Main Results

• LadderGraphWithCycles : Ladder graph as a GraphWithCycles instance
• ladder_gaussLaw_product_is_allOnes : Product of Gauss's law operators = L (logical op)
• ladder_deformed_code_generators : The deformed code has surface-code generator structure
• dummy_grid_walk_exists : Dummy grids provide walks between non-adjacent patch edges
• GeneralizedSurgeryGraph : Two copies of G with bridge edges
• full_expansion_implies_relaxed : h(G) ≥ 1 implies relaxed expansion for any support
• relaxed_expansion_vacuous_for_disjoint : Expansion not needed on irrelevant subsets

Ladder Graph as a GraphWithCycles

The ladder graph on n rungs has:

• Vertices: Bool × Fin n (left column = false, right column = true)
• Edges: n horizontal rungs + 2(n-1) vertical rails
• n-1 independent cycles (square faces of the ladder)

We build it as a GraphWithCycles to connect to the gauging framework (Gauss's law operators from Def_2, flux operators from Def_3).

inductive QEC1.LatticeSurgeryAsGauging.LadderEdge (n : ℕ) : Type

Edge type for the ladder graph: horizontal rungs and vertical rails.

• rung {n : ℕ} : Fin n → LadderEdge n

  Horizontal rung connecting (false, i) to (true, i)

• leftRail {n : ℕ} : Fin (n - 1) → LadderEdge n

  Left vertical rail connecting (false, i) to (false, i+1)

• rightRail {n : ℕ} : Fin (n - 1) → LadderEdge n

  Right vertical rail connecting (true, i) to (true, i+1)

instance QEC1.LatticeSurgeryAsGauging.instDecidableEqLadderEdge {n✝ : ℕ} : DecidableEq (LadderEdge n✝)

Equations

• QEC1.LatticeSurgeryAsGauging.instDecidableEqLadderEdge = QEC1.LatticeSurgeryAsGauging.instDecidableEqLadderEdge.decEq

def QEC1.LatticeSurgeryAsGauging.instDecidableEqLadderEdge.decEq {n✝ : ℕ} (x✝ x✝¹ : LadderEdge n✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• QEC1.LatticeSurgeryAsGauging.instDecidableEqLadderEdge.decEq (QEC1.LatticeSurgeryAsGauging.LadderEdge.rung a) (QEC1.LatticeSurgeryAsGauging.LadderEdge.leftRail a_1) = isFalse ⋯
• QEC1.LatticeSurgeryAsGauging.instDecidableEqLadderEdge.decEq (QEC1.LatticeSurgeryAsGauging.LadderEdge.rung a) (QEC1.LatticeSurgeryAsGauging.LadderEdge.rightRail a_1) = isFalse ⋯
• QEC1.LatticeSurgeryAsGauging.instDecidableEqLadderEdge.decEq (QEC1.LatticeSurgeryAsGauging.LadderEdge.leftRail a) (QEC1.LatticeSurgeryAsGauging.LadderEdge.rung a_1) = isFalse ⋯
• QEC1.LatticeSurgeryAsGauging.instDecidableEqLadderEdge.decEq (QEC1.LatticeSurgeryAsGauging.LadderEdge.leftRail a) (QEC1.LatticeSurgeryAsGauging.LadderEdge.rightRail a_1) = isFalse ⋯
• QEC1.LatticeSurgeryAsGauging.instDecidableEqLadderEdge.decEq (QEC1.LatticeSurgeryAsGauging.LadderEdge.rightRail a) (QEC1.LatticeSurgeryAsGauging.LadderEdge.rung a_1) = isFalse ⋯
• QEC1.LatticeSurgeryAsGauging.instDecidableEqLadderEdge.decEq (QEC1.LatticeSurgeryAsGauging.LadderEdge.rightRail a) (QEC1.LatticeSurgeryAsGauging.LadderEdge.leftRail a_1) = isFalse ⋯

@[reducible, inline]

abbrev QEC1.LatticeSurgeryAsGauging.LadderCycle (n : ℕ) : Type

Cycle type for the ladder: one square face for each pair of consecutive rungs.

Equations

• QEC1.LatticeSurgeryAsGauging.LadderCycle n = Fin (n - 1)

instance QEC1.LatticeSurgeryAsGauging.instFintypeLadderEdge (n : ℕ) : Fintype (LadderEdge n)

Equations

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

def QEC1.LatticeSurgeryAsGauging.ladderAdj (n : ℕ) (x y : Bool × Fin n) : Prop

The adjacency relation for the ladder graph.

Equations

• QEC1.LatticeSurgeryAsGauging.ladderAdj n x y = (x.1 ≠ y.1 ∧ x.2 = y.2 ∨ x.1 = y.1 ∧ ↑x.2 + 1 = ↑y.2 ∨ x.1 = y.1 ∧ ↑y.2 + 1 = ↑x.2)

instance QEC1.LatticeSurgeryAsGauging.instDecidableRelProdBoolFinLadderAdj (n : ℕ) : DecidableRel (ladderAdj n)

Equations

• QEC1.LatticeSurgeryAsGauging.instDecidableRelProdBoolFinLadderAdj n x y = id inferInstance

def QEC1.LatticeSurgeryAsGauging.ladderGraph (n : ℕ) : SimpleGraph (Bool × Fin n)

The ladder graph as a SimpleGraph.

Equations

• QEC1.LatticeSurgeryAsGauging.ladderGraph n = { Adj := QEC1.LatticeSurgeryAsGauging.ladderAdj n, symm := ⋯, loopless := ⋯ }

instance QEC1.LatticeSurgeryAsGauging.instDecidableRelProdBoolFinAdjLadderGraph (n : ℕ) : DecidableRel (ladderGraph n).Adj

Equations

• QEC1.LatticeSurgeryAsGauging.instDecidableRelProdBoolFinAdjLadderGraph n x y = id inferInstance

def QEC1.LatticeSurgeryAsGauging.ladderEdgeEndpoints (n : ℕ) : LadderEdge n → (Bool × Fin n) × Bool × Fin n

Endpoints for each ladder edge.

Equations

• QEC1.LatticeSurgeryAsGauging.ladderEdgeEndpoints n (QEC1.LatticeSurgeryAsGauging.LadderEdge.rung i) = ((false, i), true, i)
• QEC1.LatticeSurgeryAsGauging.ladderEdgeEndpoints n (QEC1.LatticeSurgeryAsGauging.LadderEdge.leftRail i) = ((false, ⟨↑i, ⋯⟩), false, ⟨↑i + 1, ⋯⟩)
• QEC1.LatticeSurgeryAsGauging.ladderEdgeEndpoints n (QEC1.LatticeSurgeryAsGauging.LadderEdge.rightRail i) = ((true, ⟨↑i, ⋯⟩), true, ⟨↑i + 1, ⋯⟩)

theorem QEC1.LatticeSurgeryAsGauging.ladderEdge_adj (n : ℕ) (e : LadderEdge n) : (ladderGraph n).Adj (ladderEdgeEndpoints n e).1 (ladderEdgeEndpoints n e).2

Each ladder edge connects adjacent vertices.

theorem QEC1.LatticeSurgeryAsGauging.ladderEdge_adj_symm (n : ℕ) (e : LadderEdge n) : (ladderGraph n).Adj (ladderEdgeEndpoints n e).2 (ladderEdgeEndpoints n e).1

Each ladder edge is symmetric.

def QEC1.LatticeSurgeryAsGauging.ladderCycleEdges (n : ℕ) (c : LadderCycle n) : Finset (LadderEdge n)

The cycles of the ladder: each square face consists of rung(i), rightRail(i), rung(i+1), leftRail(i).

Equations

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

noncomputable def QEC1.LatticeSurgeryAsGauging.LadderGraphWithCycles (n : ℕ) (_hn : n ≥ 2) : GraphWithCycles (Bool × Fin n) (LadderEdge n) (LadderCycle n)

Build the ladder as a GraphWithCycles to connect to the gauging framework.

Equations

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

Gauss's Law Product = Logical Operator (Gauging Measures L)

By Property 3 of Gauss's law operators (Def_2), ∏_v A_v = L. In binary vectors: the sum of all vertex supports equals the all-ones vector on the ladder vertices, which represents L = X̄₁ ⊗ X̄₂.

This is the core mechanism making lattice surgery a gauging measurement: measuring all A_v and multiplying outcomes yields the eigenvalue of L.

theorem QEC1.LatticeSurgeryAsGauging.ladder_gaussLaw_product_is_allOnes (n : ℕ) (hn : n ≥ 2) : (LadderGraphWithCycles n hn).gaussLaw_product_vertexSupport = fun (x : Bool × Fin n) => 1

The sum of all Gauss's law vertex supports on the ladder is the all-ones vector. (Instantiation of gaussLaw_product_vertexSupport_all_ones from Def_2.)

theorem QEC1.LatticeSurgeryAsGauging.ladder_gaussLaw_edge_support_zero (n : ℕ) (hn : n ≥ 2) : (LadderGraphWithCycles n hn).gaussLaw_product_edgeSupport = 0

The edge support of the Gauss's law product is zero (edges cancel pairwise).

theorem QEC1.LatticeSurgeryAsGauging.ladder_gaussLaw_product_is_L_pair (n : ℕ) (hn : n ≥ 2) : ((LadderGraphWithCycles n hn).gaussLaw_product_vertexSupport = fun (x : Bool × Fin n) => 1) ∧ (LadderGraphWithCycles n hn).gaussLaw_product_edgeSupport = 0

Combining: ∏_v A_v = L on the ladder (vertex support = all-ones, edge support = 0).

Deformed Code Structure on the Merged Patch

For the ladder with n rungs:

• |V| = 2n vertices → 2n Gauss's law operators (2n - 1 independent)
• |E| = 3n - 2 edges → n - 1 independent cycles → n - 1 flux operators
• Each cycle (square face) has exactly 4 edges → each B_p has weight 4

theorem QEC1.LatticeSurgeryAsGauging.ladder_vertex_count (n : ℕ) : Fintype.card (Bool × Fin n) = 2 * n

The ladder has 2n vertices.

theorem QEC1.LatticeSurgeryAsGauging.ladder_edge_count (n : ℕ) (hn : n ≥ 1) : Fintype.card (LadderEdge n) = 3 * n - 2

The ladder has n rungs + 2(n-1) rails = 3n - 2 edges when n ≥ 1.

theorem QEC1.LatticeSurgeryAsGauging.ladder_independent_cycle_count (n : ℕ) : Fintype.card (LadderCycle n) = n - 1

The number of independent cycles in the ladder is n - 1.

theorem QEC1.LatticeSurgeryAsGauging.ladder_cycle_weight_four (n : ℕ) (_hn : n ≥ 2) (c : LadderCycle n) : (ladderCycleEdges n c).card = 4

Each cycle (square face) of the ladder consists of exactly 4 edges.

theorem QEC1.LatticeSurgeryAsGauging.ladder_deformed_code_generators (n : ℕ) (_hn : n ≥ 2) : 2 * n - 1 + (n - 1) = 3 * n - 2

The deformed code has the correct generator counts for a surface code.

Split Step: Measuring Out Edge Qubits Matches Conventional Surgery

theorem QEC1.LatticeSurgeryAsGauging.split_step_removes_gauge_qubits (rows cols : ℕ) (_hr : rows ≥ 2) (_hc : cols ≥ 2) : 2 * (rows * cols) + (3 * rows - 2) - (3 * rows - 2) = 2 * (rows * cols)

After the split step, gauge qubits are discarded and only original code qubits remain.

Non-Adjacent Patches via Dummy Grid

For non-adjacent patches, the gauging graph includes a grid of dummy vertices. The key property is that the dummy grid provides walks of bounded length between the left and right edges.

structure QEC1.LatticeSurgeryAsGauging.DummyGridConfig : Type

A dummy grid bridges non-adjacent patches.

• rows : ℕ
• gap_width : ℕ
• h_rows : self.rows ≥ 2
• h_gap : self.gap_width ≥ 1

def QEC1.LatticeSurgeryAsGauging.gridAdj (D : DummyGridConfig) (x y : Fin D.rows × Fin (D.gap_width + 2)) : Prop

Grid graph adjacency: unit-distance neighbors on the grid.

Equations

• QEC1.LatticeSurgeryAsGauging.gridAdj D x y = (x.1 = y.1 ∧ ↑x.2 + 1 = ↑y.2 ∨ x.1 = y.1 ∧ ↑y.2 + 1 = ↑x.2 ∨ x.2 = y.2 ∧ ↑x.1 + 1 = ↑y.1 ∨ x.2 = y.2 ∧ ↑y.1 + 1 = ↑x.1)

instance QEC1.LatticeSurgeryAsGauging.instDecidableRelProdFinRowsHAddNatGap_widthOfNatGridAdj (D : DummyGridConfig) : DecidableRel (gridAdj D)

Equations

• QEC1.LatticeSurgeryAsGauging.instDecidableRelProdFinRowsHAddNatGap_widthOfNatGridAdj D x y = id inferInstance

def QEC1.LatticeSurgeryAsGauging.gridGraph (D : DummyGridConfig) : SimpleGraph (Fin D.rows × Fin (D.gap_width + 2))

Equations

• QEC1.LatticeSurgeryAsGauging.gridGraph D = { Adj := QEC1.LatticeSurgeryAsGauging.gridAdj D, symm := ⋯, loopless := ⋯ }

theorem QEC1.LatticeSurgeryAsGauging.dummy_grid_walk_exists (D : DummyGridConfig) (i : Fin D.rows) : ∃ (w : (gridGraph D).Walk (i, ⟨0, ⋯⟩) (i, ⟨D.gap_width + 1, ⋯⟩)), w.length = D.gap_width + 1

For each row, there exists a horizontal walk of length gap_width + 1.

theorem QEC1.LatticeSurgeryAsGauging.dummy_grid_qubit_count (D : DummyGridConfig) : Fintype.card (Fin D.rows × Fin (D.gap_width + 2)) = D.rows * (D.gap_width + 2)

The dummy grid has rows × (gap_width + 2) total qubits.

theorem QEC1.LatticeSurgeryAsGauging.dummy_grid_qubit_decomposition (D : DummyGridConfig) : D.rows * (D.gap_width + 2) = 2 * D.rows + D.rows * D.gap_width

The dummy qubits decompose: 2 * rows edge qubits + rows * gap_width dummy qubits.

Generalization: Two Copies of G with Bridge Edges

For any pair of matching logical X operators on two code blocks, use two copies of graph G with additional bridge edges connecting corresponding vertices.

def QEC1.LatticeSurgeryAsGauging.GeneralizedSurgeryAdj {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (bridges : Finset (V × V)) (x y : Bool × V) : Prop

The combined graph for generalized lattice surgery: two copies of G with bridges.

Equations

• QEC1.LatticeSurgeryAsGauging.GeneralizedSurgeryAdj G bridges x y = (x.1 = y.1 ∧ G.Adj x.2 y.2 ∨ x.1 ≠ y.1 ∧ ((x.2, y.2) ∈ bridges ∨ (y.2, x.2) ∈ bridges))

def QEC1.LatticeSurgeryAsGauging.GeneralizedSurgeryGraph {V : Type u_1} (G : SimpleGraph V) [DecidableRel G.Adj] (bridges : Finset (V × V)) : SimpleGraph (Bool × V)

The combined graph is a valid SimpleGraph.

Equations

• QEC1.LatticeSurgeryAsGauging.GeneralizedSurgeryGraph G bridges = { Adj := QEC1.LatticeSurgeryAsGauging.GeneralizedSurgeryAdj G bridges, symm := ⋯, loopless := ⋯ }

theorem QEC1.LatticeSurgeryAsGauging.generalized_surgery_vertex_count {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (_bridges : Finset (V × V)) : Fintype.card (Bool × V) = 2 * Fintype.card V

The combined graph has 2|V| vertices.

theorem QEC1.LatticeSurgeryAsGauging.bridge_provides_cross_path {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (bridges : Finset (V × V)) (u v : V) (h : (u, v) ∈ bridges) : (GeneralizedSurgeryGraph G bridges).Adj (false, u) (true, v)

Bridge edges provide direct cross-copy connections.

theorem QEC1.LatticeSurgeryAsGauging.intra_copy_adj_preserved {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (bridges : Finset (V × V)) (b : Bool) (u v : V) (h : G.Adj u v) : (GeneralizedSurgeryGraph G bridges).Adj (b, u) (b, v)

Intra-copy adjacency is preserved.

Relaxed Expansion: h(G) ≥ 1 is Overkill

The full Cheeger condition h(G) ≥ 1 constrains ALL subsets S ⊆ V with |S| ≤ |V|/2. For lattice surgery, expansion is only needed for subsets that intersect the logical operator's support supp(L). Subsets disjoint from supp(L) are irrelevant.

def QEC1.LatticeSurgeryAsGauging.RelaxedExpansionProperty {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (logicalSupport : Finset V) : Prop

Relaxed expansion: |∂S| ≥ |S| required only for S intersecting logical support.

Equations

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

theorem QEC1.LatticeSurgeryAsGauging.full_expansion_implies_relaxed {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (logicalSupport : Finset V) (hexp : IsStrongExpander G) : RelaxedExpansionProperty G logicalSupport

Full Cheeger expansion h(G) ≥ 1 implies relaxed expansion for any support.

theorem QEC1.LatticeSurgeryAsGauging.relaxed_expansion_vacuous_for_disjoint {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (logicalSupport S : Finset V) (_hS_pos : 0 < S.card) (_hS_size : 2 * S.card ≤ Fintype.card V) (hdisjoint : Disjoint S logicalSupport) : ¬(S ∩ logicalSupport).Nonempty

Relaxed expansion is strictly weaker: subsets disjoint from logical support are unconstrained.

theorem QEC1.LatticeSurgeryAsGauging.relaxed_on_full_support_implies_strong {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (_hV : 0 < Fintype.card V) (hrel : RelaxedExpansionProperty G Finset.univ) (S : Finset V) : S.Nonempty → 2 * S.card ≤ Fintype.card V → (edgeBoundary G S).card ≥ S.card

When logical support = full vertex set, relaxed expansion implies full expansion (both conditions coincide since every subset intersects the full vertex set).

theorem QEC1.LatticeSurgeryAsGauging.strong_implies_relaxed {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hexp : IsStrongExpander G) : RelaxedExpansionProperty G Finset.univ

Full expansion implies relaxed expansion (converse direction).

theorem QEC1.LatticeSurgeryAsGauging.exists_unconstrained_subset {V : Type u_1} [DecidableEq V] [Fintype V] (_G : SimpleGraph V) [DecidableRel _G.Adj] (logicalSupport : Finset V) (h_small : logicalSupport.card < Fintype.card V) : ∃ (v : V), v ∉ logicalSupport

When the total vertex count exceeds the logical support, there exist vertices outside the support (i.e., unconstrained by relaxed expansion).