Remark 18: Relation to Lattice Surgery

Statement

The gauging measurement procedure (Def_5) generalizes surface code lattice surgery.

Surface code lattice surgery as gauging: Choose graph G to be a ladder graph connecting the boundary qubits (support of X̄₁ and X̄₂). The vertex set is supp(X̄₁) ∪ supp(X̄₂), edges are rungs (connecting corresponding qubits across boundaries) plus two rails (connecting consecutive qubits within each boundary). The product ∏_v A_v = L = X̄₁ ⊗ X̄₂ (the logical being measured). The deformed code is again a surface code on the union of two patches. Phase 3 edge measurements (Z_e readout) correspond to the standard lattice surgery "splitting" step that disentangles the merged patches.

Non-adjacent surface codes: Add a grid of dummy vertices between two boundary edges, forming a connected graph. This implements long-range lattice surgery with constant qubit overhead per unit spatial distance.

Generalization to LDPC codes: For two stabilizer code blocks with logical X operators of the same weight W, choose the same graph G for both logicals (with low Cheeger expansion being acceptable provided the remaining desiderata from Rem_11 are satisfied, namely short paths for deformation and low-weight cycle basis). Add bridge edges to form a single connected graph. This generalizes lattice surgery to arbitrary LDPC codes.

Main Results

• LadderGraph : the ladder graph connecting two boundary qubit sets
• ladderGraph_connected : the ladder graph is connected
• ladderGraph_degree_le_three : each vertex has degree ≤ 3
• ladderGraph_edge_count_le : edge count is at most 3n
• ladder_deformed_code_is_stabilizer : the deformed code on the ladder graph is a valid stabilizer code (pairwise commuting checks)
• ladder_phase3_disentangles : Phase 3 Z_e measurements on edges are pure Z-type, mutually commuting, and self-inverse — corresponding to the splitting step that disentangles merged patches
• DummyGridGraph : extended graph with dummy ancilla grid
• dummyGridGraph_connected : the extended graph is connected
• dummy_overhead_per_unit_distance : qubit overhead per unit spatial distance is constant (= n), independent of distance D
• BridgeGraph : graph with bridge edges for LDPC generalization
• bridgeGraph_connected : the bridge graph is connected
• bridge_desiderata_transfer : short paths and low-weight cycle basis transfer from G to the bridge graph within each copy

Part 1: Ladder Graph Construction

For lattice surgery on a pair of surface codes, the graph G is a ladder graph. The vertex set is the disjoint union of the two boundary qubit sets (support of X̄₁ and X̄₂). The edges consist of:

• Rungs: connecting corresponding boundary qubits across the two codes
• Rails: connecting consecutive qubits within each boundary

We model this using Fin n for each boundary, so vertices are Bool × Fin n (Bool selects the code, Fin n selects the boundary qubit position).

def RelationToLatticeSurgery.ladderAdj (n : ℕ) : Bool × Fin n → Bool × Fin n → Prop

The adjacency relation for the ladder graph on 2n vertices. Two vertices are adjacent if they are:

1. A rung: same position i, different boundaries (false,i)-(true,i)
2. A rail: same boundary, consecutive positions i and i+1

Equations

• RelationToLatticeSurgery.ladderAdj n p q = (p ≠ q ∧ (p.1 ≠ q.1 ∧ p.2 = q.2 ∨ p.1 = q.1 ∧ (↑p.2 + 1 = ↑q.2 ∨ ↑q.2 + 1 = ↑p.2)))

theorem RelationToLatticeSurgery.ladderAdj_symm (n : ℕ) (p q : Bool × Fin n) : ladderAdj n p q → ladderAdj n q p

theorem RelationToLatticeSurgery.ladderAdj_irrefl (n : ℕ) (p : Bool × Fin n) : ¬ladderAdj n p p

instance RelationToLatticeSurgery.ladderAdj_decidable (n : ℕ) : DecidableRel (ladderAdj n)

Equations

• RelationToLatticeSurgery.ladderAdj_decidable n p q = id inferInstance

def RelationToLatticeSurgery.LadderGraph (n : ℕ) : SimpleGraph (Bool × Fin n)

The ladder graph connecting two boundary qubit sets of size n. Vertices: Bool × Fin n (2n vertices total). Edges: rungs (across boundaries) + rails (within each boundary).

Equations

• RelationToLatticeSurgery.LadderGraph n = { Adj := RelationToLatticeSurgery.ladderAdj n, symm := ⋯, loopless := ⋯ }

instance RelationToLatticeSurgery.instDecidableRelProdBoolFinAdjLadderGraph (n : ℕ) : DecidableRel (LadderGraph n).Adj

Equations

• RelationToLatticeSurgery.instDecidableRelProdBoolFinAdjLadderGraph n = RelationToLatticeSurgery.ladderAdj_decidable n

theorem RelationToLatticeSurgery.ladderGraph_card (n : ℕ) : Fintype.card (Bool × Fin n) = 2 * n

The ladder graph has 2n vertices.

theorem RelationToLatticeSurgery.rung_is_edge (n : ℕ) (i : Fin n) : (LadderGraph n).Adj (false, i) (true, i)

Rungs are edges of the ladder graph: (false, i) ~ (true, i).

theorem RelationToLatticeSurgery.rail_is_edge (n : ℕ) (b : Bool) (i j : Fin n) (hij : ↑i + 1 = ↑j) : (LadderGraph n).Adj (b, i) (b, j)

Rails are edges of the ladder graph: (b, i) ~ (b, i+1).

theorem RelationToLatticeSurgery.ladderGraph_connected (n : ℕ) (hn : 0 < n) : (LadderGraph n).Connected

The ladder graph is connected when n ≥ 1.

theorem RelationToLatticeSurgery.ladderGraph_degree_le_three (n : ℕ) (v : Bool × Fin n) : (LadderGraph n).degree v ≤ 3

Each vertex of the ladder graph has degree at most 3. The rung contributes 1 neighbor, and each rail direction contributes at most 1.

theorem RelationToLatticeSurgery.ladderGraph_edge_count_le (n : ℕ) : (LadderGraph n).edgeFinset.card ≤ 3 * n

The edge count of the ladder graph: at most 3n (via handshaking lemma).

Part 2: Lattice Surgery as a Special Case of Gauging

The key conceptual identification: the gauging measurement procedure on a ladder graph connecting two surface code boundary edges reproduces the standard lattice surgery protocol.

We formalize the structural correspondence:

1. The vertex set of G = supp(X̄₁) ∪ supp(X̄₂)
2. The gauging procedure measures all A_v = X_v ∏_{e ∋ v} X_e (Gauss operators)
3. The product ∏_v A_v = L = X̄₁ ⊗ X̄₂ (the logical being measured)
4. The deformed code on the merged system is a valid stabilizer code
5. Phase 3 edge Z_e measurements disentangle the merged patches (splitting step)

Key insight: the deformed code is a surface code on the merged patches. The Gauss checks A_v correspond to surface code vertex stabilizers on the union, the flux checks B_p correspond to face stabilizers, and the deformed original checks s̃_j correspond to boundary stabilizers. Since all checks pairwise commute (Lem_1), the deformed code is a valid stabilizer code. On the ladder graph, the topology of the merged system is exactly the surface code on the union of two patches.

theorem RelationToLatticeSurgery.ladder_deformed_code_is_stabilizer {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (i j : DeformedCode.CheckIndex V C J) : (DeformedCode.allChecks G cycles checks data i).PauliCommute (DeformedCode.allChecks G cycles checks data j)

The deformed code on G is a valid stabilizer code (pairwise commuting checks). For the ladder graph, this means the deformed code is a surface code on the union of the two patches. The Gauss checks A_v become vertex stabilizers, the flux checks B_p become face stabilizers, and the deformed checks s̃_j become boundary stabilizers — all pairwise commuting, forming a valid stabilizer code on the merged system V ⊕ E(G).

theorem RelationToLatticeSurgery.gauss_check_is_pure_X {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : (GaussFlux.gaussLawOp G v).zVec = 0

The Gauss check structure matches surface code vertex stabilizers. Each Gauss check A_v = X_v ∏_{e ∋ v} X_e (from Def 2) acts as X on the vertex qubit v and X on all edge qubits incident to v. On the ladder graph, this is exactly the vertex stabilizer of the surface code on the merged patch: a star of X operators centered at v. The key structural property: A_v is pure X-type (no Z support).

theorem RelationToLatticeSurgery.logical_is_gauss_product {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : GaussFlux.logicalOp G = ∏ v : V, GaussFlux.gaussLawOp G v

The product of all Gauss operators is the logical being measured. On the ladder graph where V = supp(X̄₁) ∪ supp(X̄₂), the product ∏_v A_v = L = X̄₁ ⊗ X̄₂ is a pure X operator on all vertex qubits. For the ladder graph, L = logicalOp G represents X̄₁ ⊗ X̄₂ because the vertex set is exactly supp(X̄₁) ∪ supp(X̄₂).

theorem RelationToLatticeSurgery.ladder_phase3_disentangles {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (e : ↑G.edgeSet) : (GaugingMeasurement.edgeZOperatorMeasured G e).xVec = 0 ∧ (∀ (e' : ↑G.edgeSet), (GaugingMeasurement.edgeZOperatorMeasured G e).PauliCommute (GaugingMeasurement.edgeZOperatorMeasured G e')) ∧ GaugingMeasurement.edgeZOperatorMeasured G e * GaugingMeasurement.edgeZOperatorMeasured G e = 1

Phase 3 splitting step: structural correspondence. Phase 3 of the gauging procedure measures Z_e on each edge qubit e ∈ E(G). For lattice surgery, this is the "splitting" step that disentangles the merged surface code patches. The key properties that make this a valid splitting step:

1. Each Z_e is pure Z-type (no X support) — so it does not disturb vertex qubits
2. All Z_e mutually commute — so they can be measured simultaneously
3. Each Z_e is self-inverse — so it is a valid projective measurement After measuring all Z_e, the edge qubits are projected onto Z eigenstates, effectively disentangling them from the vertex qubits and recovering the two separate surface code patches.

theorem RelationToLatticeSurgery.logical_is_pure_X {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : (GaussFlux.logicalOp G).zVec = 0

The logical operator is pure X-type: it has no Z support on any qubit.

theorem RelationToLatticeSurgery.logical_self_inverse {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : GaussFlux.logicalOp G * GaussFlux.logicalOp G = 1

The logical operator is self-inverse: L² = 1.

theorem RelationToLatticeSurgery.ladder_vertex_decomposition (n : ℕ) : Fintype.card (Bool × Fin n) = n + n

For the ladder graph, the vertex set is a disjoint union of two boundary sets of equal size. This models supp(X̄₁) ∪ supp(X̄₂) with |supp(X̄₁)| = |supp(X̄₂)| = n.

theorem RelationToLatticeSurgery.lattice_surgery_is_gauging (n : ℕ) (hn : 0 < n) : (LadderGraph n).Connected ∧ Fintype.card (Bool × Fin n) = 2 * n ∧ (∀ (v : Bool × Fin n), (LadderGraph n).degree v ≤ 3) ∧ (LadderGraph n).edgeFinset.card ≤ 3 * n

Lattice surgery is a special case of gauging — structural summary. For a ladder graph G connecting two boundary qubit sets of size n ≥ 1:

1. G is connected (ladder graph is connected)
2. G has 2n vertices = |supp(X̄₁)| + |supp(X̄₂)|
3. G has bounded degree ≤ 3 (constant overhead per qubit)
4. The edge count is O(n) (at most 3n)

Part 3: Non-Adjacent Surface Codes — Dummy Grid Extension

For surface codes whose boundary edges are separated by spatial distance D, we add a grid of dummy (ancilla) vertices between the two boundary edges. The graph G has vertex set supp(X̄₁) ∪ supp(X̄₂) ∪ {ancilla vertices}, with constant qubit overhead per unit distance.

def RelationToLatticeSurgery.gridAdj (n D : ℕ) : Fin n × Fin (D + 2) → Fin n × Fin (D + 2) → Prop

The adjacency relation for the grid graph: vertices are adjacent if they are in the same row and adjacent columns, or in the same column and adjacent rows.

Equations

• RelationToLatticeSurgery.gridAdj n D p q = (p ≠ q ∧ (p.1 = q.1 ∧ (↑p.2 + 1 = ↑q.2 ∨ ↑q.2 + 1 = ↑p.2) ∨ p.2 = q.2 ∧ (↑p.1 + 1 = ↑q.1 ∨ ↑q.1 + 1 = ↑p.1)))

instance RelationToLatticeSurgery.gridAdj_decidable (n D : ℕ) : DecidableRel (gridAdj n D)

Equations

• RelationToLatticeSurgery.gridAdj_decidable n D p q = id inferInstance

def RelationToLatticeSurgery.DummyGridGraph (n D : ℕ) : SimpleGraph (Fin n × Fin (D + 2))

The grid graph connecting two boundary edges with D columns of dummy ancillas. Column 0 is boundary 1, column D+1 is boundary 2, columns 1..D are dummy ancillas.

Equations

• RelationToLatticeSurgery.DummyGridGraph n D = { Adj := RelationToLatticeSurgery.gridAdj n D, symm := ⋯, loopless := ⋯ }

instance RelationToLatticeSurgery.instDecidableRelProdFinHAddNatOfNatAdjDummyGridGraph (n D : ℕ) : DecidableRel (DummyGridGraph n D).Adj

Equations

• RelationToLatticeSurgery.instDecidableRelProdFinHAddNatOfNatAdjDummyGridGraph n D = RelationToLatticeSurgery.gridAdj_decidable n D

theorem RelationToLatticeSurgery.dummyGridGraph_card (n D : ℕ) : Fintype.card (Fin n × Fin (D + 2)) = n * (D + 2)

The grid graph has n × (D + 2) vertices.

theorem RelationToLatticeSurgery.grid_horizontal_edge (n D : ℕ) (i : Fin n) (j j' : Fin (D + 2)) (hjj' : ↑j + 1 = ↑j') : (DummyGridGraph n D).Adj (i, j) (i, j')

Horizontal edges (same row, adjacent columns) in the grid.

theorem RelationToLatticeSurgery.grid_vertical_edge (n D : ℕ) (i i' : Fin n) (j : Fin (D + 2)) (hii' : ↑i + 1 = ↑i') : (DummyGridGraph n D).Adj (i, j) (i', j)

Vertical edges (same column, adjacent rows) in the grid.

theorem RelationToLatticeSurgery.dummyGridGraph_connected (n D : ℕ) (hn : 0 < n) : (DummyGridGraph n D).Connected

The grid graph is connected when n ≥ 1.

theorem RelationToLatticeSurgery.dummyGridGraph_degree_le_four (n D : ℕ) (v : Fin n × Fin (D + 2)) : (DummyGridGraph n D).degree v ≤ 4

Each vertex of the grid graph has degree at most 4 (up/down/left/right).

theorem RelationToLatticeSurgery.dummy_overhead_per_unit_distance (n D : ℕ) : n * D + 2 * n = n * (D + 2)

Constant qubit overhead per unit spatial distance. For boundary qubit sets of size n separated by distance D:

• Total vertices: n × (D + 2)
• Boundary qubits: 2n (n on each side, columns 0 and D+1)
• Dummy ancilla qubits: n × D
• Overhead per unit distance: n qubits per column, independent of D. This is the key claim: the overhead is constant (= n) per unit spatial distance. Expressed as: ancilla count n * D + boundary 2n = total n * (D + 2).

theorem RelationToLatticeSurgery.dummy_overhead_decomposition (n D : ℕ) : n * (D + 2) = 2 * n + n * D

The total qubit count decomposes into boundary + ancilla.

theorem RelationToLatticeSurgery.dummyGridGraph_edge_count_le (n D : ℕ) : (DummyGridGraph n D).edgeFinset.card ≤ 2 * (n * (D + 2))

The edge count of the grid graph, via the handshaking lemma and degree ≤ 4.

Part 4: Bridge Graph for LDPC Code Generalization

For two stabilizer code blocks with logical X operators of the same weight W, we combine two copies of the gauging graph G with "bridge" edges between them to form a single connected graph. The original remark says:

• Choose the same graph G for both logicals
• Low Cheeger expansion is acceptable provided remaining desiderata are satisfied
• Add bridge edges to form a single connected graph

We formalize the bridge graph and show that the desiderata (short paths, low-weight cycle basis) transfer from G to the bridge graph within each copy.

def RelationToLatticeSurgery.bridgeAdj {V : Type u_1} (G : SimpleGraph V) (bridges : Finset V) : V ⊕ V → V ⊕ V → Prop

The adjacency relation for the bridge graph: either an edge within a copy of G, or a bridge edge connecting corresponding vertices across the two copies.

Equations

• RelationToLatticeSurgery.bridgeAdj G bridges (Sum.inl v) (Sum.inl w) = G.Adj v w
• RelationToLatticeSurgery.bridgeAdj G bridges (Sum.inr v) (Sum.inr w) = G.Adj v w
• RelationToLatticeSurgery.bridgeAdj G bridges (Sum.inl v) (Sum.inr w) = (v = w ∧ v ∈ bridges)
• RelationToLatticeSurgery.bridgeAdj G bridges (Sum.inr v) (Sum.inl w) = (v = w ∧ v ∈ bridges)

theorem RelationToLatticeSurgery.bridgeAdj_symm {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (bridges : Finset V) (p q : V ⊕ V) : bridgeAdj G bridges p q → bridgeAdj G bridges q p

theorem RelationToLatticeSurgery.bridgeAdj_irrefl {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (bridges : Finset V) (p : V ⊕ V) : ¬bridgeAdj G bridges p p

instance RelationToLatticeSurgery.bridgeAdj_decidable {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (bridges : Finset V) : DecidableRel (bridgeAdj G bridges)

Equations

• RelationToLatticeSurgery.bridgeAdj_decidable G bridges (Sum.inl v) (Sum.inl w) = id inferInstance
• RelationToLatticeSurgery.bridgeAdj_decidable G bridges (Sum.inr v) (Sum.inr w) = id inferInstance
• RelationToLatticeSurgery.bridgeAdj_decidable G bridges (Sum.inl v) (Sum.inr w) = id instDecidableAnd
• RelationToLatticeSurgery.bridgeAdj_decidable G bridges (Sum.inr v) (Sum.inl w) = id instDecidableAnd

def RelationToLatticeSurgery.BridgeGraph {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (bridges : Finset V) : SimpleGraph (V ⊕ V)

The bridge graph: two copies of G connected by bridge edges at specified vertices.

Equations

• RelationToLatticeSurgery.BridgeGraph G bridges = { Adj := RelationToLatticeSurgery.bridgeAdj G bridges, symm := ⋯, loopless := ⋯ }

instance RelationToLatticeSurgery.instDecidableRelSumAdjBridgeGraph {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (bridges : Finset V) : DecidableRel (BridgeGraph G bridges).Adj

Equations

• RelationToLatticeSurgery.instDecidableRelSumAdjBridgeGraph G bridges = RelationToLatticeSurgery.bridgeAdj_decidable G bridges

theorem RelationToLatticeSurgery.bridgeGraph_copy1_adj {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (bridges : Finset V) {v w : V} (h : G.Adj v w) : (BridgeGraph G bridges).Adj (Sum.inl v) (Sum.inl w)

Internal edges of copy 1 are edges of the bridge graph.

theorem RelationToLatticeSurgery.bridgeGraph_copy2_adj {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (bridges : Finset V) {v w : V} (h : G.Adj v w) : (BridgeGraph G bridges).Adj (Sum.inr v) (Sum.inr w)

Internal edges of copy 2 are edges of the bridge graph.

theorem RelationToLatticeSurgery.bridgeGraph_bridge_adj {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (bridges : Finset V) {v : V} (hv : v ∈ bridges) : (BridgeGraph G bridges).Adj (Sum.inl v) (Sum.inr v)

Bridge edges connect corresponding vertices across copies.

theorem RelationToLatticeSurgery.bridgeGraph_card {V : Type u_1} [Fintype V] [DecidableEq V] : Fintype.card (V ⊕ V) = 2 * Fintype.card V

The bridge graph has 2|V| vertices.

def RelationToLatticeSurgery.bridgeGraph_copy1_embedding {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (bridges : Finset V) : G →g BridgeGraph G bridges

G embeds as a subgraph into each copy of the bridge graph. Paths in G correspond to paths in the bridge graph within a single copy.

Equations

• RelationToLatticeSurgery.bridgeGraph_copy1_embedding G bridges = { toFun := Sum.inl, map_rel' := ⋯ }

def RelationToLatticeSurgery.bridgeGraph_copy2_embedding {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (bridges : Finset V) : G →g BridgeGraph G bridges

Equations

• RelationToLatticeSurgery.bridgeGraph_copy2_embedding G bridges = { toFun := Sum.inr, map_rel' := ⋯ }

theorem RelationToLatticeSurgery.bridgeGraph_connected {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (bridges : Finset V) (hconn : G.Connected) (hbridge : bridges.Nonempty) : (BridgeGraph G bridges).Connected

The bridge graph is connected if G is connected and at least one bridge exists.

theorem RelationToLatticeSurgery.bridgeGraph_dist_le_copy1 {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (bridges : Finset V) (v w : V) (hr : G.Reachable v w) : (BridgeGraph G bridges).dist (Sum.inl v) (Sum.inl w) ≤ G.dist v w

The embedding preserves distances: dist in bridge graph ≤ dist in G. Paths within a copy of G are paths in the bridge graph.

Part 5: LDPC Desiderata on the Bridge Graph

The remark states that for LDPC generalization:

• Choose the same graph G for both logicals
• Low Cheeger expansion is acceptable provided the remaining desiderata are satisfied
• The key desiderata that must transfer: short paths for deformation and low-weight cycle basis

We formalize how short paths and low-weight cycle basis transfer from G to the bridge graph via the subgraph embedding. The Cheeger expansion condition is explicitly noted as acceptable (i.e., may be weaker on the bridge graph) provided the other desiderata hold.

theorem RelationToLatticeSurgery.bridge_short_paths_within_copy {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {J : Type u_2} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (D : ℕ) (hsp : DesiderataForGraphG.ShortPathsForDeformation G checks D) (hconn : G.Connected) (j : J) (u v : V) (hu : u ∈ (checks j).supportZ) (hv : v ∈ (checks j).supportZ) (bridges : Finset V) : (BridgeGraph G bridges).dist (Sum.inl u) (Sum.inl v) ≤ D

Short paths transfer from G to the bridge graph within each copy. If G has the short paths property with bound D (Rem_11 Desideratum 1), then vertices in the same copy of the bridge graph also have short paths. The key fact: dist in BridgeGraph restricted to copy 1 ≤ dist in G ≤ D. Requires G connected so that all vertices are reachable.

theorem RelationToLatticeSurgery.bridge_low_weight_cycles_in_copy {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (W : ℕ) (hlw : DesiderataForGraphG.LowWeightCycleBasis G cycles W) (c : C) : {e : ↑G.edgeSet | e ∈ cycles c}.card ≤ W

Low-weight cycle basis on the bridge graph. When G has a cycle basis where each cycle has weight ≤ W (Rem_11 Desideratum 3), the bridge graph inherits this bound for cycles within each copy.

theorem RelationToLatticeSurgery.cheeger_expansion_acceptable_with_desiderata {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (D W : ℕ) (hsp : DesiderataForGraphG.ShortPathsForDeformation G checks D) (hlw : DesiderataForGraphG.LowWeightCycleBasis G cycles W) (bridges : Finset V) (hconn : G.Connected) (hbridge : bridges.Nonempty) : (BridgeGraph G bridges).Connected ∧ (∀ (j : J) (u v : V), u ∈ (checks j).supportZ → v ∈ (checks j).supportZ → (BridgeGraph G bridges).dist (Sum.inl u) (Sum.inl v) ≤ D) ∧ ∀ (c : C), {e : ↑G.edgeSet | e ∈ cycles c}.card ≤ W

Cheeger expansion acceptability. The original remark states that "low Cheeger expansion is acceptable provided the remaining desiderata from Rem_11 are satisfied, namely short paths for deformation and low-weight cycle basis." We formalize: if G satisfies short paths and low-weight cycles, the bridge graph provides a valid gauging setup regardless of its Cheeger constant.

theorem RelationToLatticeSurgery.ldpc_lattice_surgery_generalization {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (D W : ℕ) (hsp : DesiderataForGraphG.ShortPathsForDeformation G checks D) (hlw : DesiderataForGraphG.LowWeightCycleBasis G cycles W) (bridges : Finset V) (hconn : G.Connected) (hbridge : bridges.Nonempty) : (BridgeGraph G bridges).Connected ∧ Fintype.card (V ⊕ V) = 2 * Fintype.card V ∧ (∀ (j : J) (u v : V), u ∈ (checks j).supportZ → v ∈ (checks j).supportZ → (BridgeGraph G bridges).dist (Sum.inl u) (Sum.inl v) ≤ D) ∧ ∀ (c : C), {e : ↑G.edgeSet | e ∈ cycles c}.card ≤ W

LDPC generalization of lattice surgery: main structural theorem. For two code blocks with weight-W logical X operators:

1. Take a connected graph G satisfying desiderata
2. Form BridgeGraph G bridges connecting the two copies
3. The bridge graph is connected with 2|V| vertices
4. Short paths and low-weight cycles within each copy are preserved
5. Low Cheeger expansion is acceptable (need not be preserved)

Part 6: Long-Range Lattice Surgery

For surface codes separated by distance D, the grid of dummy vertices provides long-range lattice surgery with overhead linear in D.

theorem RelationToLatticeSurgery.long_range_surgery_overhead (n : ℕ) (hn : 0 < n) (D : ℕ) : (DummyGridGraph n D).Connected ∧ Fintype.card (Fin n × Fin (D + 2)) = n * (D + 2) ∧ n * (D + 2) = 2 * n + n * D

Long-range lattice surgery via grid extension. For boundary qubit sets of size n separated by distance D:

1. The grid graph has n × (D + 2) vertices, which is connected
2. The qubit overhead (dummy ancilla count) is n × D
3. Overhead per unit distance is constant: n qubits per column

Summary

theorem RelationToLatticeSurgery.gauging_generalizes_lattice_surgery : (∀ (n : ℕ), 0 < n → (LadderGraph n).Connected ∧ Fintype.card (Bool × Fin n) = 2 * n ∧ (∀ (v : Bool × Fin n), (LadderGraph n).degree v ≤ 3) ∧ (LadderGraph n).edgeFinset.card ≤ 3 * n) ∧ (∀ (n : ℕ), 0 < n → ∀ (D : ℕ), (DummyGridGraph n D).Connected ∧ n * (D + 2) = 2 * n + n * D) ∧ ∀ (V : Type u_1) [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (bridges : Finset V), G.Connected → bridges.Nonempty → (BridgeGraph G bridges).Connected ∧ Fintype.card (V ⊕ V) = 2 * Fintype.card V

Summary theorem: Lattice surgery as gauging. The gauging measurement procedure (Def 5) generalizes lattice surgery:

1. Standard lattice surgery: ladder graph, O(n) overhead, degree ≤ 3, ∏_v A_v = L implements the measurement
2. Long-range lattice surgery: grid graph with dummy ancillas, overhead linear in spatial distance D, constant per unit distance
3. LDPC generalization: bridge graph, connectivity and desiderata (short paths, low-weight cycles) preserved within each copy; low Cheeger expansion is acceptable