18 Rem 11: Desiderata for Graph \(G\)
When choosing a constant-degree graph \(G\) for the gauging measurement, three desiderata must be satisfied:
Short paths for deformation: \(G\) should contain a constant-length edge-path between any pair of vertices in the \(Z\)-type support of the same original check, ensuring deformed checks have bounded weight.
Sufficient expansion: The Cheeger constant should satisfy \(h(G) \geq 1\), ensuring the deformed code has distance at least \(d\).
Low-weight cycle basis: There should exist a generating set of cycles where each cycle has weight at most some constant, ensuring the flux operators \(B_p\) have bounded weight.
When all three conditions are satisfied with constants independent of \(n\), the gauging measurement procedure has constant overhead per qubit, the LDPC property is preserved, and there is no distance reduction.
18.1 Desideratum 1: Short Paths for Deformation
Let \(G\) be a simple graph on vertices \(V\), let \(\{ s_j\} _{j \in J}\) be a family of Pauli operators, and let \(D \in \mathbb {N}\). We say \(G\) satisfies short paths for deformation with parameter \(D\) if for every check \(s_j\) and every pair of vertices \(u, v\) in the \(Z\)-support of \(s_j\), the graph distance satisfies \(\operatorname {dist}_G(u,v) \leq D\).
If \(G\) satisfies short paths for deformation with parameter \(D\), then for any check \(s_j\) and any \(u, v \in \operatorname {supportZ}(s_j)\), we have \(\operatorname {dist}_G(u,v) \leq D\).
This follows directly from the definition of short paths for deformation applied to \(j\), \(u\), \(v\), and the membership hypotheses.
If \(G\) is connected, then for any check \(s_j\) and any \(u, v \in \operatorname {supportZ}(s_j)\), the vertex \(v\) is reachable from \(u\) in \(G\).
This follows directly from the connectedness of \(G\): since \(G\) is connected, any two vertices \(u\) and \(v\) are reachable from each other.
For any check \(s_j\), we have \(|\operatorname {supportZ}(s_j)| \leq \operatorname {weight}(s_j)\).
We unfold the definition of weight as \(|\operatorname {support}(s_j)|\). We show \(\operatorname {supportZ}(s_j) \subseteq \operatorname {support}(s_j)\) by taking any \(v \in \operatorname {supportZ}(s_j)\), rewriting via the membership characterization of \(\operatorname {supportZ}\), then showing \(v \in \operatorname {support}(s_j)\) via the right disjunct of the support membership condition. The result then follows by monotonicity of cardinality.
Let \(\gamma : E(G) \to \mathbb {Z}/2\mathbb {Z}\) be an edge-path with at most \(B\) nonzero entries. Then the number of edges where the deformed check \(\tilde{s}_j(\gamma )\) acts nontrivially in the \(Z\)-component is at most \(B\).
Rewriting using the edge action count characterization from the flexibility analysis, the number of edges where the deformed check has nonzero \(Z\)-action equals the number of nonzero entries of \(\gamma \), which is at most \(B\) by hypothesis.
When \(\gamma = 0\) (the zero edge-path), the deformed check \(\tilde{s}_j(0)\) has no nonzero \(Z\)-action on any edge. That is, the number of edges with nontrivial \(Z\)-action is \(0\).
This follows directly from the zero-path edge count result.
18.2 Desideratum 2: Sufficient Expansion
A simple graph \(G\) has sufficient expansion if \(1 \leq h(G)\), where \(h(G)\) is the Cheeger constant of \(G\).
If \(G\) has sufficient expansion, then \(G\) is a \(1\)-expander.
We construct the pair: the positivity condition \(0 {\lt} 1\) holds by norm_num, and the Cheeger bound \(1 \leq h(G)\) is exactly the sufficient expansion hypothesis.
If \(G\) has sufficient expansion, then for every nonempty \(S \subseteq V\) with \(2|S| \leq |V|\), we have \(|S| \leq |\partial S|\), where \(\partial S\) is the edge boundary.
From the Cheeger constant bound theorem, we have \(h(G) \cdot |S| \leq |\partial S|\) as real numbers. Since \(h(G) \geq 1\) by the sufficient expansion hypothesis, we obtain \(|S| \leq |\partial S|\) by linear arithmetic.
If \(G\) has sufficient expansion, then \(h(G) {\gt} 0\).
Since \(0 {\lt} 1\) and \(1 \leq h(G)\), we have \(0 {\lt} h(G)\) by transitivity.
18.3 Desideratum 3: Low-Weight Cycle Basis
Let \(G\) be a simple graph, let \(\{ \text{cycle}_c\} _{c \in C}\) be a family of subsets of edges, and let \(W \in \mathbb {N}\). The cycle basis is low-weight with parameter \(W\) if for every \(c \in C\), the number of edges in \(\text{cycle}_c\) is at most \(W\).
If the cycle basis has low weight with parameter \(W\), then for every plaquette \(p\), the weight of the flux check \(B_p\) is at most \(W\).
Rewriting the weight of the flux check using the flux check weight characterization, the weight equals the number of edges in cycle \(p\), which is at most \(W\) by the low-weight hypothesis.
If the cycle basis has low weight with parameter \(W\), then for all plaquettes \(p\), \(\operatorname {weight}(B_p) \leq W\).
For each \(p\), this follows directly from the low-weight cycles bound on flux weight.
18.4 Constant Degree and Edge Overhead
A simple graph \(G\) has constant degree with parameter \(\Delta \) if for every vertex \(v\), \(\deg (v) \leq \Delta \).
If \(G\) has constant degree \(\Delta \), then \(2|E| \leq \Delta \cdot |V|\).
We first establish that \(\sum _{v \in V} \deg (v) \leq \Delta \cdot |V|\). By the degree bound, \(\sum _v \deg (v) \leq \sum _v \Delta = \Delta \cdot |V|\), where the first inequality uses the constant degree hypothesis applied to each vertex, and the second equality follows by simplification with the sum of a constant. By the handshaking lemma, \(\sum _v \deg (v) = 2|E|\). We obtain this from the graph’s sum-of-degrees-equals-twice-edges result, adjusting for the fintype edge set instance by subsingleton elimination. The conclusion \(2|E| \leq \Delta \cdot |V|\) then follows by integer arithmetic.
If \(G\) has constant degree \(\Delta \) and \(|V| {\gt} 0\), then \(\frac{|E|}{|V|} \leq \frac{\Delta }{2}\).
From the constant degree bound \(2|E| \leq \Delta \cdot |V|\), we rewrite the division inequality using the characterization \(\frac{a}{b} \leq \frac{c}{d}\) iff \(a \cdot d \leq c \cdot b\) (for positive denominators). The positivity of \(|V|\) and \(2\) are verified. Casting the natural number inequality \(2|E| \leq \Delta \cdot |V|\) to \(\mathbb {R}\) and rearranging by linear arithmetic yields the result.
If \(G\) has constant degree \(\Delta \), then \(2(|V| + |E|) \leq (2 + \Delta ) \cdot |V|\).
From the bound \(2|E| \leq \Delta \cdot |V|\), the result \(2(|V| + |E|) \leq (2 + \Delta ) \cdot |V|\) follows by nonlinear arithmetic.
18.5 Gauss Check Weight Characterization
For any vertices \(v, w\), the \(X\)-component of \(A_v\) at vertex \(w\) is given by \((A_v)^X_{w} = \begin{cases} 1 & \text{if } w = v \\ 0 & \text{otherwise} \end{cases}\).
This follows by simplification from the definition of the Gauss law operator.
For any vertex \(v\) and edge \(e\), the \(X\)-component of \(A_v\) at edge \(e\) is \((A_v)^X_e = \begin{cases} 1 & \text{if } v \in e \\ 0 & \text{otherwise} \end{cases}\).
This follows by simplification from the definition of the Gauss law operator.
\(A_v\) acts nontrivially at vertex \(w\) if and only if \(w = v\).
We simplify using the support membership characterization, the \(X\)-vector formula at vertices, and the fact that the \(Z\)-vector of \(A_v\) is zero. For the forward direction, given that \(w\) is in the support, we case split: if the \(X\)-component is nonzero, then by contradiction if \(w \neq v\) the component would be zero; if the \(Z\)-component is nonzero, this contradicts it being zero. For the reverse direction, assuming \(w = v\), the left disjunct holds by simplification.
\(A_v\) acts nontrivially at edge \(e\) if and only if \(v \in e\).
We simplify using the support membership, the \(X\)-vector formula at edges, and the zero \(Z\)-vector. For the forward direction, case splitting: if the \(X\)-component is nonzero, by contradiction if \(v \notin e\) the component would be zero; the \(Z\)-component case gives a contradiction. For the reverse, assuming \(v \in e\), the left disjunct holds by simplification.
The support of \(A_v\) is
By extensionality, we take an arbitrary element \(q\) and case split. If \(q = \operatorname {inl}(w)\): membership in the left-hand side is equivalent to \(w = v\) by the vertex support lemma; membership in the right-hand side reduces to the singleton condition or being in the image of the edge filter, where the latter is impossible for a vertex element. If \(q = \operatorname {inr}(e)\): membership in the left-hand side is equivalent to \(v \in e\) by the edge support lemma; for the right-hand side, the forward direction constructs the witness \(e\) with its membership proof, and the reverse direction extracts the edge from the existential and applies injectivity of \(\operatorname {inr}\).
The weight of \(A_v\) equals \(1 + |\{ e \in E(G) \mid v \in e\} |\).
Unfolding the weight as the cardinality of the support and rewriting with the support characterization, we compute the cardinality of the disjoint union. Disjointness holds because \(\operatorname {inl}(v)\) cannot equal any \(\operatorname {inr}(e)\): assuming membership in both the singleton and the mapped filter set, we obtain a contradiction from the impossibility of \(\operatorname {inl}(v) = \operatorname {inr}(e)\). The cardinality of the union of disjoint sets is the sum of cardinalities, giving \(1 + |\{ e \mid v \in e\} |\) since the map preserves cardinality.
The number of edges \(e\) with \(v \in e\) equals the cardinality of \(\operatorname {incidentEdges}(G, v)\).
The two finsets have equal underlying sets, so their cardinalities agree by congruence.
The weight of \(A_v\) equals \(1 + |\operatorname {incidentEdges}(G, v)|\).
Rewriting with the weight formula and the incident edges characterization, we obtain the result directly.
The cardinality of \(\operatorname {incidentEdges}(G, v)\) equals \(\deg _G(v)\).
We first rewrite \(\deg _G(v)\) as \(|\operatorname {incidenceFinset}(v)|\) using the standard characterization. We then show the images under the subtype coercion agree: for the forward direction, given an edge in \(\operatorname {incidentEdges}(G,v)\), its underlying \(\operatorname {Sym2}(V)\) element satisfies both the edge membership and incidence conditions; for the reverse, given an element of the incidence finset, we construct the corresponding subtype element. The cardinality equality follows from injectivity of the subtype coercion.
On a constant-degree graph with parameter \(\Delta \), the weight of \(A_v\) is at most \(1 + \Delta \).
Rewriting the weight as \(1 + |\operatorname {incidentEdges}(G,v)|\) and then as \(1 + \deg _G(v)\), the bound \(\deg _G(v) \leq \Delta \) from the constant degree hypothesis yields \(\operatorname {weight}(A_v) \leq 1 + \Delta \) by linear arithmetic.
18.6 All Desiderata Satisfied
A structure bundling all three desiderata for graph \(G\) with parameters \(D\) and \(W\):
short_paths: \(G\) satisfies short paths for deformation with parameter \(D\).
expansion: \(G\) has sufficient expansion (\(h(G) \geq 1\)).
low_weight_cycles: The cycle basis of \(G\) has low weight with parameter \(W\).
When all desiderata are satisfied with parameters \(D, W\), the flux checks have weight at most \(W\).
This follows directly from the low-weight cycles bound on flux weight, using the low-weight cycle component of the all-desiderata structure.
When all desiderata are satisfied, \(G\) is a \(1\)-expander.
This follows by applying the sufficient expansion implies expander result to the expansion component of the all-desiderata structure.
When all desiderata are satisfied, every nonempty \(S \subseteq V\) with \(2|S| \leq |V|\) satisfies \(|S| \leq |\partial S|\).
This follows by applying the expansion boundary bound to the expansion component of the all-desiderata structure.
18.7 LDPC Preservation
The deformed code is LDPC with weight bound \(w\) and check bound \(c\) if the deformed stabilizer code satisfies the \(\operatorname {IsQLDPC}\) predicate with parameters \(w\) and \(c\).
On a constant-degree graph with parameter \(\Delta \), the Gauss law check \(A_v\) has weight at most \(1 + \Delta \).
This follows directly from the Gauss law weight bound.
If the cycle basis has low weight \(W\), then the flux check \(B_p\) has weight at most \(W\).
This follows directly from the low-weight cycles bound on flux weight.
18.8 Summary: Combined Consequences
When all three desiderata and constant degree \(\Delta \) are satisfied, the following hold simultaneously:
Flux checks bounded: for all plaquettes \(p\), \(\operatorname {weight}(B_p) \leq W\).
\(G\) is a \(1\)-expander.
Edge overhead is linear: \(2|E| \leq \Delta \cdot |V|\).
Gauss checks bounded: for all vertices \(v\), \(\operatorname {weight}(A_v) \leq 1 + \Delta \).
We construct the four-tuple directly: (1) for each plaquette \(p\), apply the low-weight cycles bound; (2) apply the sufficient expansion implies expander result; (3) apply the constant degree bounds edges result; (4) for each vertex \(v\), apply the Gauss law weight bound.
When all three desiderata and constant degree \(\Delta \) are satisfied with \(|V| {\gt} 0\), the additional qubit overhead per vertex satisfies \(\frac{|E|}{|V|} \leq \frac{\Delta }{2}\).
This follows directly from the edge overhead per vertex result applied to the constant degree hypothesis.