41 Rem 18: Lattice Surgery as Gauging
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. Measuring \(\bar{X}_1 \otimes \bar{X}_2\) on a pair of equally sized surface code blocks using a ladder graph \(G\) joining the edge qubits produces a deformed code that is again a surface code on the union of the two patches. The final step of measuring out individual edge qubits matches conventional lattice surgery. For non-adjacent patches, one uses a graph with a grid of dummy vertices between the two edges. The procedure extends to any pair of matching logical \(X\) operators using two copies of graph \(G\) with bridge edges. The Cheeger condition \(h(G) \geq 1\) is overkill; expansion is only needed for subsets of qubits relevant to the logical operators being measured.
41.1 Ladder Graph
The edge type for the ladder graph on \(n\) rungs is an inductive type with three constructors:
\(\mathrm{rung}(i)\) for \(i \in \mathrm{Fin}(n)\): horizontal rung connecting \((\mathrm{false}, i)\) to \((\mathrm{true}, i)\).
\(\mathrm{leftRail}(i)\) for \(i \in \mathrm{Fin}(n-1)\): left vertical rail connecting \((\mathrm{false}, i)\) to \((\mathrm{false}, i+1)\).
\(\mathrm{rightRail}(i)\) for \(i \in \mathrm{Fin}(n-1)\): right vertical rail connecting \((\mathrm{true}, i)\) to \((\mathrm{true}, i+1)\).
The cycle type for the ladder: one square face for each pair of consecutive rungs. Formally, \(\mathrm{LadderCycle}(n) := \mathrm{Fin}(n-1)\).
The adjacency relation for the ladder graph on \(n\) rungs. Two vertices \(x, y \in \mathrm{Bool} \times \mathrm{Fin}(n)\) are adjacent if:
\(x_1 \neq y_1\) and \(x_2 = y_2\) (horizontal rung), or
\(x_1 = y_1\) and \(x_2 + 1 = y_2\) (vertical rail going up), or
\(x_1 = y_1\) and \(y_2 + 1 = x_2\) (vertical rail going down).
The ladder graph on \(n\) rungs as a simple graph on vertex set \(\mathrm{Bool} \times \mathrm{Fin}(n)\), with adjacency given by \(\mathrm{ladderAdj}\).
The endpoint function for each ladder edge:
\(\mathrm{rung}(i) \mapsto ((\mathrm{false}, i), (\mathrm{true}, i))\),
\(\mathrm{leftRail}(i) \mapsto ((\mathrm{false}, i), (\mathrm{false}, i+1))\),
\(\mathrm{rightRail}(i) \mapsto ((\mathrm{true}, i), (\mathrm{true}, i+1))\).
Each ladder edge connects adjacent vertices: for every edge \(e\) of the ladder graph on \(n\) rungs,
We proceed by cases on the edge \(e\).
Case \(e = \mathrm{rung}(i)\): By simplification of the endpoint and adjacency definitions, the adjacency holds via the first disjunct: \(\mathrm{false} \neq \mathrm{true}\) and the second coordinates are equal.
Case \(e = \mathrm{leftRail}(i)\): By simplification, the adjacency holds via the second disjunct: the first coordinates are equal (both \(\mathrm{false}\)) and the second coordinate satisfies \(i + 1 = i + 1\).
Case \(e = \mathrm{rightRail}(i)\): Analogous to the left rail case, with both first coordinates equal to \(\mathrm{true}\).
Each ladder edge is symmetric: the graph adjacency holds in both directions for the endpoints of every edge.
This follows directly from the symmetry of the ladder graph applied to the adjacency of each edge (Theorem 1305).
The edges forming cycle \(c\) of the ladder: each square face consists of
The ladder graph on \(n \geq 2\) rungs, built as a \(\mathrm{GraphWithCycles}\) instance to connect to the gauging framework (Gauss’s law operators from Def 2, flux operators from Def 3). The graph is the ladder graph, with edge endpoints and cycle structure as defined above.
41.2 Gauss’s Law Product Equals Logical Operator
The sum of all Gauss’s law vertex supports on the ladder is the all-ones vector:
This is an instantiation of the general property from the Gauss’s law operator definition.
This follows directly from the general theorem \(\mathrm{gaussLaw\_ product\_ vertexSupport\_ all\_ ones}\) applied to the ladder graph.
The edge support of the Gauss’s law product on the ladder is zero (edges cancel pairwise):
This follows directly from the general theorem \(\mathrm{gaussLaw\_ product\_ edgeSupport\_ zero}\) applied to the ladder graph.
Combining: \(\prod _v A_v = L\) on the ladder, i.e., the vertex support equals the all-ones vector and the edge support equals zero:
This follows directly from the general theorem \(\mathrm{gaussLaw\_ product\_ is\_ L}\) applied to the ladder graph.
41.3 Deformed Code Structure on the Merged Patch
The ladder has \(2n\) vertices:
By simplification using the product cardinality formula: \(|\mathrm{Bool}| \cdot |\mathrm{Fin}(n)| = 2 \cdot n\).
For \(n \geq 1\), the ladder has \(3n - 2\) edges:
This counts \(n\) rungs \(+ 2(n-1)\) rails.
The universal finset of \(\mathrm{LadderEdge}(n)\) decomposes as the disjoint union of the images of the three constructors (rung, leftRail, rightRail). We verify pairwise disjointness: elements of different constructors are unequal since the constructors are injective and distinct. By the disjoint union cardinality formula, the total count is \(|\mathrm{Fin}(n)| + |\mathrm{Fin}(n-1)| + |\mathrm{Fin}(n-1)| = n + (n-1) + (n-1) = 3n - 2\), where the final equality holds by integer arithmetic since \(n \geq 1\).
The number of independent cycles in the ladder is \(n - 1\):
This holds by definition since \(\mathrm{LadderCycle}(n) = \mathrm{Fin}(n-1)\) and \(|\mathrm{Fin}(n-1)| = n-1\).
For \(n \geq 2\), each cycle (square face) of the ladder consists of exactly 4 edges:
By simplification of the cycle edge definition, the set contains four elements: \(\mathrm{rung}(c)\), \(\mathrm{rung}(c+1)\), \(\mathrm{leftRail}(c)\), and \(\mathrm{rightRail}(c)\). We verify non-membership at each insertion step: \(\mathrm{rung}(c) \neq \mathrm{rung}(c+1)\) since their indices differ (by \(\omega \)-arithmetic on the injected index), and elements from different constructors are always distinct. Thus the cardinality of the four-element set is 4.
The deformed code has the correct generator counts for a surface code:
Here \(2n - 1\) is the number of independent Gauss’s law operators and \(n - 1\) is the number of flux operators.
This follows by integer arithmetic (\(\omega \)).
41.4 Split Step
After the split step, gauge qubits are discarded and only original code qubits remain. For surface code blocks of size \(\mathrm{rows} \times \mathrm{cols}\) with \(\mathrm{rows}, \mathrm{cols} \geq 2\):
This follows by integer arithmetic (\(\omega \)).
41.5 Non-Adjacent Patches via Dummy Grid
A dummy grid bridges non-adjacent patches. It is a structure consisting of:
\(\mathrm{rows} : \mathbb {N}\) with \(\mathrm{rows} \geq 2\),
\(\mathrm{gap\_ width} : \mathbb {N}\) with \(\mathrm{gap\_ width} \geq 1\).
Grid graph adjacency on \(\mathrm{Fin}(\mathrm{rows}) \times \mathrm{Fin}(\mathrm{gap\_ width} + 2)\): two vertices \(x, y\) are adjacent if they are unit-distance neighbors, i.e.,
The grid graph on \(\mathrm{Fin}(\mathrm{rows}) \times \mathrm{Fin}(\mathrm{gap\_ width} + 2)\) as a simple graph with adjacency \(\mathrm{gridAdj}\).
For each row \(i\), there exists a horizontal walk of length \(\mathrm{gap\_ width} + 1\) in the grid graph from \((i, 0)\) to \((i, \mathrm{gap\_ width} + 1)\).
It suffices to show: for all \(a \leq b\) with \(a, b {\lt} \mathrm{gap\_ width} + 2\), there exists a walk from \((i, a)\) to \((i, b)\) of length \(b - a\). We prove this by induction on \(b\).
Base case (\(b = 0\)): Since \(a \leq 0\), we have \(a = 0\), so the nil walk suffices with length \(0 = 0 - 0\).
Inductive step (\(b = b' + 1\)): If \(a = b' + 1\), the nil walk suffices. Otherwise \(a \leq b'\), and by the induction hypothesis there exists a walk \(w'\) from \((i, a)\) to \((i, b')\) of length \(b' - a\). Since \((i, b')\) and \((i, b'+1)\) are adjacent in the grid graph (by the first disjunct of grid adjacency), we append a single-step walk to obtain a walk of length \((b' - a) + 1 = (b'+1) - a\).
Instantiating with \(a = 0\) and \(b = \mathrm{gap\_ width} + 1\) yields the desired walk of length \(\mathrm{gap\_ width} + 1\).
The dummy grid has \(\mathrm{rows} \times (\mathrm{gap\_ width} + 2)\) total qubits.
By simplification using the product cardinality formula: \(|\mathrm{Fin}(\mathrm{rows})| \cdot |\mathrm{Fin}(\mathrm{gap\_ width}+2)| = \mathrm{rows} \cdot (\mathrm{gap\_ width}+2)\).
The dummy qubits decompose into edge qubits and dummy qubits:
This follows by ring arithmetic.
41.6 Generalized Surgery Graph
The adjacency relation for the combined graph used in generalized lattice surgery: two copies of a graph \(G\) on vertex set \(V\) with a set of bridge edges. Two vertices \(x, y \in \mathrm{Bool} \times V\) are adjacent if:
\(x_1 = y_1\) and \(G.\mathrm{Adj}\; x_2\; y_2\) (intra-copy adjacency), or
\(x_1 \neq y_1\) and \(((x_2, y_2) \in \mathrm{bridges}\) or \((y_2, x_2) \in \mathrm{bridges})\) (cross-copy bridge).
The combined graph for generalized lattice surgery: two copies of \(G\) with bridge edges, forming a valid simple graph on \(\mathrm{Bool} \times V\).
The combined graph has \(2|V|\) vertices:
By simplification using the product cardinality formula and \(|\mathrm{Bool}| = 2\).
Bridge edges provide direct cross-copy connections: if \((u, v) \in \mathrm{bridges}\), then \((\mathrm{false}, u)\) and \((\mathrm{true}, v)\) are adjacent in the generalized surgery graph.
By simplification of the adjacency definition, the adjacency holds via the second disjunct: \(\mathrm{false} \neq \mathrm{true}\) and \((u, v) \in \mathrm{bridges}\).
Intra-copy adjacency is preserved: if \(G.\mathrm{Adj}\; u\; v\), then for any \(b \in \mathrm{Bool}\), \((b, u)\) and \((b, v)\) are adjacent in the generalized surgery graph.
By simplification of the adjacency definition, the adjacency holds via the first disjunct: the boolean components are equal (both \(b\)) and \(G.\mathrm{Adj}\; u\; v\) holds by assumption.
41.7 Relaxed Expansion
Relaxed expansion: the condition \(|\partial S| \geq |S|\) is required only for subsets \(S \subseteq V\) satisfying \(0 {\lt} |S|\), \(2|S| \leq |V|\), and \((S \cap \mathrm{logicalSupport}) \neq \emptyset \). Formally,
Full Cheeger expansion \(h(G) \geq 1\) implies relaxed expansion for any logical support set.
Let \(S\) be a subset with \(0 {\lt} |S|\), \(2|S| \leq |V|\), and \((S \cap \mathrm{logicalSupport}) \neq \emptyset \). Since \(|S| {\gt} 0\), the set \(S\) is nonempty.
We first establish that \(h(G) \leq |\partial _E S| / |S|\). By definition of the Cheeger constant as the infimum over all nonempty subsets \(S'\) with \(2|S'| \leq |V|\) of \(|\partial _E S'| / |S'|\), we apply \(\mathrm{ciInf\_ le}\) (using that the range is bounded below by 0, which we verify by checking that each term in the infimum is a ratio of nonneg quantities, handling the cases where the inner conditional infima may be empty). Evaluating at the specific subset \(S\) and simplifying the conditional infima using the positive cardinality and size bound hypotheses, we obtain \(h(G) \leq |\partial _E S| / |S|\).
Since \(h(G) \geq 1\) by the strong expansion hypothesis, we have \(1 \leq |\partial _E S| / |S|\). As \(|S| {\gt} 0\) (cast to \(\mathbb {R}\)), we multiply both sides by \(|S|\) to obtain \(|S| \leq |\partial _E S|\) in \(\mathbb {R}\), hence \(|\partial _E S| \geq |S|\) in \(\mathbb {N}\).
Relaxed expansion is strictly weaker than full expansion: subsets \(S\) disjoint from the logical support are unconstrained. If \(\mathrm{Disjoint}(S, \mathrm{logicalSupport})\), then \((S \cap \mathrm{logicalSupport})\) is not nonempty.
We rewrite the goal to show \(S \cap \mathrm{logicalSupport} = \emptyset \). This follows directly from the disjointness hypothesis via the equivalence \(\mathrm{Disjoint}(S, \mathrm{logicalSupport}) \iff S \cap \mathrm{logicalSupport} = \emptyset \).
When the logical support equals the full vertex set \(V\), relaxed expansion implies full expansion, since every nonempty subset intersects the full vertex set:
Let \(S\) be nonempty with \(2|S| \leq |V|\). We apply the relaxed expansion hypothesis with logical support equal to \(\mathrm{univ}\). The intersection condition \((S \cap \mathrm{univ}).\mathrm{Nonempty}\) is verified by rewriting \(\mathrm{univ} \cap S = S\) (using commutativity of intersection) and using the nonemptiness of \(S\).
Full expansion (strong expander) implies relaxed expansion on the full vertex set. This is the converse direction establishing the equivalence when logical support is \(V\).
This follows directly from \(\mathrm{full\_ expansion\_ implies\_ relaxed}\) applied with \(\mathrm{logicalSupport} = \mathrm{univ}\).
When the total vertex count exceeds the logical support cardinality, there exist vertices outside the support (i.e., unconstrained by relaxed expansion):
We proceed by contradiction. Assume for all \(v\), \(v \in \mathrm{logicalSupport}\). Then by extensionality, \(\mathrm{logicalSupport} = \mathrm{univ}\). Rewriting the cardinality hypothesis, we get \(|\mathrm{univ}| {\lt} |\mathrm{univ}|\) (i.e., \(|V| {\lt} |V|\)), which contradicts irreflexivity of \({\lt}\).