17 Rem 10: Flexibility of Graph G
The gauging measurement procedure allows arbitrary choice of the connected graph \(G\) with vertex set equal to the support of the logical operator \(L\). The properties of the deformed code depend strongly on this choice. In particular:
Dummy vertices: \(G\) can have additional vertices beyond the support of \(L\), achieved by gauging \(L' = L \cdot \prod _{\text{dummy}} X_v\).
Graph properties: The choice of \(G\) determines \(|E|\) (the edge qubit count), deformed check weights (via path lengths), and code distance (via expansion).
The original logical operator \(L\) on vertex set \(V\) is defined as
i.e., the Pauli operator with \(\mathrm{xVec}(v) = 1\) for all \(v \in V\) and \(\mathrm{zVec} = 0\).
The extended logical operator \(L'\) on the extended vertex type \(V \oplus D\) is defined as
i.e., the Pauli operator with \(\mathrm{xVec}(q) = 1\) for all \(q \in V \oplus D\) and \(\mathrm{zVec} = 0\).
The dummy \(X\) product \(\prod _{d \in D} X_d\) acting on \(V \oplus D\) is the Pauli operator with
The lifted logical operator \(L_{\mathrm{lift}}\) on \(V \oplus D\) acts as \(X\) on all \(V\)-qubits and as the identity on \(D\)-qubits:
The extended logical operator satisfies
on \(V \oplus D\).
By extensionality, it suffices to show equality for each component for an arbitrary qubit \(q\). We consider both the \(\mathrm{xVec}\) and \(\mathrm{zVec}\) components, and case-split on whether \(q \in V\) or \(q \in D\). In each case, the equality follows by simplification using the definitions of \(L'\), \(L_{\mathrm{lift}}\), and the dummy \(X\) product, together with the formulas for multiplication of Pauli operators.
The extended logical operator is self-inverse: \(L' \cdot L' = \mathbf{1}\).
This follows directly from the fact that every Pauli operator satisfies \(P \cdot P = \mathbf{1}\) (the mul_self lemma).
The extended logical operator \(L'\) is pure \(X\)-type: it has no \(Z\)-support, i.e., \(\mathrm{zVec}(L') = 0\).
By extensionality over qubits \(q\), we simplify using the definition of \(L'\), which has \(\mathrm{zVec} = 0\).
The \(X\)-support of \(L'\) is all of \(V \oplus D\): \(\operatorname {supportX}(L') = V \oplus D\).
By extensionality, for each qubit \(q\), membership in \(\operatorname {supportX}(L')\) is equivalent to \(\mathrm{xVec}(q) \ne 0\). By the definition of \(L'\), \(\mathrm{xVec}(q) = 1\) for all \(q\), so every qubit is in the support, yielding \(\operatorname {supportX}(L') = \operatorname {univ}\).
The extended logical operator equals \(\operatorname {prodX}(\operatorname {univ})\) on \(V \oplus D\).
By extensionality over both the \(\mathrm{xVec}\) and \(\mathrm{zVec}\) components, this follows by simplification using the definitions of \(L'\) and \(\operatorname {prodX}\).
Let \(\sigma _V : V \to \mathbb {Z}/2\mathbb {Z}\) be the measurement outcomes on original vertices and \(\sigma _D : D \to \mathbb {Z}/2\mathbb {Z}\) the outcomes on dummy vertices. If all dummy vertices give \(+1\) outcomes (i.e., \(\sigma _D(d) = 0\) for all \(d \in D\)), then
That is, dummy vertices do not affect the logical measurement sign.
We rewrite the sum over \(V \oplus D\) as \(\sum _{v \in V} \sigma _V(v) + \sum _{d \in D} \sigma _D(d)\) using the decomposition of a sum over a sum type. Since \(\sigma _D(d) = 0\) for all \(d \in D\) by hypothesis, the second sum vanishes by simplification, yielding the result.
The weight of the extended logical operator is \(|V| + |D|\):
Unfolding the definitions of weight and support, and simplifying using the definition of \(L'\) (which has \(\mathrm{xVec}(q) = 1\) for all \(q\) and \(\mathrm{zVec} = 0\)), the support is all of \(V \oplus D\). The cardinality of \(V \oplus D\) equals \(|V| + |D|\).
When \(D\) is empty, the weight of \(L'\) restricted to \(V\) equals \(|V|\):
Rewriting using the weight formula \(\operatorname {weight}(L') = |V| + |D|\), and noting that \(|D| = 0\) since \(D\) is empty, we obtain \(|V| + 0 = |V|\).
For every qubit \(q \in V \oplus D\), \(\mathrm{zVec}(\prod _{d \in D} X_d)(q) = 0\). This means the dummy \(X\) product commutes with everything on the \(Z\) side, and adding dummy \(X\) operators never changes \(Z\)-support parity.
By simplification using the definition of the dummy \(X\) product, which has \(\mathrm{zVec} = 0\).
For every qubit \(q \in V \oplus D\), \(\mathrm{zVec}(L_{\mathrm{lift}})(q) = 0\). The lifted logical is pure \(X\)-type.
By simplification using the definition of \(L_{\mathrm{lift}}\), which has \(\mathrm{zVec} = 0\).
The dummy \(X\) product is self-inverse: \(\bigl(\prod _{d \in D} X_d\bigr)^2 = \mathbf{1}\).
This follows directly from mul_self, since every Pauli operator squares to the identity.
The lifted logical operator is self-inverse: \(L_{\mathrm{lift}}^2 = \mathbf{1}\).
This follows directly from mul_self, since every Pauli operator squares to the identity.
The lifted logical and dummy \(X\) product commute:
This follows directly from commutativity of Pauli operator multiplication (PauliOp.mul_comm).
The deformed code’s qubit count is \(|V| + |E|\), so the edge qubit overhead (the additional qubits beyond the original \(|V|\)) is exactly \(|E(G)|\). Different graphs \(G\) give different overhead via their edge count:
This follows directly from deformedStabilizerCode_numQubits.
The deformed code’s check count is \(|V| + |C| + |J|\): \(|V|\) Gauss law checks, \(|C|\) flux checks, and \(|J|\) deformed original checks. The overhead in checks beyond the original \(|J|\) is \(|V| + |C|\):
This follows directly from deformedStabilizerCode_numChecks.
Two graphs \(G_1, G_2\) on the same vertex set \(V\) with different edge counts (\(|E(G_1)| \ne |E(G_2)|\)) produce deformed codes with different qubit counts:
This follows by integer arithmetic (omega): if \(|E(G_1)| \ne |E(G_2)|\), then \(|V| + |E(G_1)| \ne |V| + |E(G_2)|\).
For an expander graph \(G\) with expansion constant \(c\), every nonempty subset \(S \subseteq V\) with \(2|S| \le |V|\) satisfies
where \(\partial S\) denotes the edge boundary. This is the mechanism by which expansion of \(G\) controls the distance of the deformed code: logical operators supported on small subsets necessarily have large edge boundary.
This follows directly from edgeBoundary_card_ge_of_cheeger, applied to the graph \(G\), expansion constant \(c\), the expander hypothesis, subset \(S\), its nonemptiness, and the size bound \(2|S| \le |V|\).
For a connected graph \(G\) on \(|V| \ge 2\) vertices, the edge set is nonempty (\(0 {\lt} |E(G)|\)). This means gauging always introduces at least one auxiliary qubit.
We rewrite the goal using the characterization that \(|E(G)| {\gt} 0\) iff the edge set is nonempty. From the hypothesis \(|V| \ge 2\), we obtain the existence of a nonempty valid subset \(S\) via cheegerValidSubsets’_nonempty_of_card_ge_two. Since \(|V| {\gt} 1\), the type \(V\) is nontrivial, so there exist distinct vertices \(a, b \in V\) with \(a \ne b\). By connectedness of \(G\), there exists a walk from \(a\) to \(b\). We proceed by induction on the walk. In the base case (nil), the walk from \(a\) to \(a\) contradicts \(a \ne b\). In the inductive case (cons), the walk starts with an edge from \(u\) to \(v'\) via an adjacency \(\mathrm{hadj}\), and we exhibit the edge \(\{ u, v'\} \) as an element of \(E(G)\) (using \(\mathrm{hadj}\) to verify membership in the edge set), proving the edge set is nonempty.
The edge \(Z\)-support of a deformed check equals the support of the edge-path \(\gamma \). For any original check \(s\), edge-path \(\gamma : E(G) \to \mathbb {Z}/2\mathbb {Z}\), and edge \(e \in E(G)\):
More edges in \(\gamma \) means more \(Z\)-support on edge qubits, hence higher weight.
This follows directly from deformedOpExt_zVec_edge, which states that the \(Z\)-component of the deformed operator extension on edge qubits equals \(\gamma \).
The edge \(X\)-support of a deformed check is empty: deformed checks have no \(X\)-action on edge qubits. For any original check \(s\), edge-path \(\gamma \), and edge \(e\):
This follows directly from deformedOpExt_xVec_edge, which states that the \(X\)-component of the deformed operator extension on edge qubits is zero.
The number of edge qubits where the deformed check acts non-trivially (via \(Z\)) equals the number of edges in \(\gamma \) with \(\gamma (e) \ne 0\):
This is the “edge contribution” to the deformed check weight.
The two finite sets are equal by congruence: the filter predicates are definitionally equal since \(\mathrm{zVec}(\tilde{s})(e) = \gamma (e)\) for all edges \(e\).
A zero edge-path adds no edge weight: when \(\gamma = 0\), the deformed check acts only on vertices:
By simplification using the fact that \(\mathrm{zVec}(\tilde{s})(e) = \gamma (e) = 0\) for all edges \(e\) when \(\gamma = 0\), the filter set is empty and has cardinality \(0\).