21 Rem 12: Worst-Case Graph Construction
We outline a construction that produces a graph \(G\) with qubit overhead \(O(W \log ^2 W)\) satisfying all desiderata from Remark 11, for a logical operator \(L\) of weight \(W\).
Let \(L\) denote the support of \(L\) (so \(|L| = W\)), and let \(V = L\) be the vertex set.
Step 1: \(Z\)-type support matching. For each check \(s_j\) with \(S_Z(s_j) \cap L \neq \emptyset \), the intersection has even cardinality (since \(s_j\) commutes with \(L = \prod _v X_v\)). Pick a perfect matching and add edges, achieving Desideratum 1 with \(D = 1\).
Step 2: Achieve expansion. Add edges until \(h(G) \geq 1\) (Cheeger constant), satisfying Desideratum 2. The resulting graph \(G_0\) is constant-degree.
Step 3: Cycle sparsification. Apply Definition 6 to \(G_0\) with \(R = O(\log ^2 W)\) layers (Lemma 2). All generating cycles have weight \(\leq 4\), satisfying Desideratum 3.
Result:
Total qubits: \(O(W) \cdot O(\log ^2 W) = O(W \log ^2 W)\).
All checks have bounded weight.
Distance is preserved: \(d^* \geq d\).
Let \(V\) be a finite type and let \(P\) be a Pauli operator on \(V\). Then
Expanding the definition of the symplectic inner product and \(\operatorname {prodX}\), the \(X\)-vector of \(\operatorname {prodX}(\operatorname {univ})\) is the all-ones function and the \(Z\)-vector is identically zero. Thus the sum reduces to \(\sum _v P.\operatorname {zVec}(v) \cdot 1 + P.\operatorname {xVec}(v) \cdot 0 = \sum _v P.\operatorname {zVec}(v)\). By simplification and functional extensionality (using commutativity of the ring), the two sides are equal.
Let \(P\) be a Pauli operator on a finite type \(V\). Then
Unfolding the definitions of \(\operatorname {PauliCommute}\) and \(\operatorname {CommutesWithLogical}\), we rewrite using the identity \(\langle P, \operatorname {prodX}(V) \rangle _{\mathrm{symp}} = \sum _v P.\operatorname {zVec}(v)\) (from the previous theorem), and then use the equality \(\sum _v P.\operatorname {zVec}(v) = \sum _v \operatorname {zSupportOnVertices}(P)(v)\) to conclude.
Let \(P\) be a Pauli operator on a finite type \(V\). If \(\operatorname {PauliCommute}(P, \operatorname {prodX}(V))\), then
Rewriting the hypothesis using the equivalence \(\operatorname {PauliCommute}(P, \operatorname {prodX}(V)) \Leftrightarrow \operatorname {CommutesWithLogical}(P)\), the result follows from the implication \(\operatorname {CommutesWithLogical}(P) \Rightarrow \text{Even}(|\{ v : P.\operatorname {zVec}(v) \neq 0\} |)\).
Let \(P\) be a Pauli operator on a finite type \(V\). If \(\operatorname {PauliCommute}(P, \operatorname {prodX}(V))\), then
This follows directly from the previous theorem: since the cardinality is even, it is congruent to \(0\) modulo \(2\).
Let \(G\) be a simple graph on a finite type \(V\), and let \(\{ \operatorname {checks}(j)\} _{j \in J}\) be a family of Pauli operators. Suppose that for every check \(j\) and every pair of distinct vertices \(u, v\) in \(\operatorname {supportZ}(\operatorname {checks}(j))\), \(u\) and \(v\) are adjacent in \(G\). Then \(\operatorname {ShortPathsForDeformation}(G, \operatorname {checks}, 1)\) holds.
Let \(j\), \(u\), \(v\) be given with \(u \in \operatorname {supportZ}(\operatorname {checks}(j))\) and \(v \in \operatorname {supportZ}(\operatorname {checks}(j))\). We consider two cases. If \(u = v\), then \(\operatorname {dist}(u, v) = 0 \leq 1\) by reflexivity of the distance. If \(u \neq v\), then by hypothesis \(G.\operatorname {Adj}(u, v)\), so \(\operatorname {dist}(u, v) = 1 \leq 1\) by the characterization of graph distance equal to one.
Under the same hypotheses as the previous theorem (every check’s \(Z\)-support forms a clique in \(G\)), for any check \(j\) and any \(u, v \in \operatorname {supportZ}(\operatorname {checks}(j))\):
This follows directly from applying the theorem \(\operatorname {step1\_ achieves\_ desideratum1}\).
Let \(G\) be a simple graph on \(V\) with checks \(\{ \operatorname {checks}(j)\} _{j \in J}\). If every pair of distinct vertices in the \(Z\)-support of each check are adjacent in \(G\), and \(G\) has sufficient expansion, then both \(\operatorname {ShortPathsForDeformation}(G, \operatorname {checks}, 1)\) and \(\operatorname {SufficientExpansion}(G)\) hold.
The pair is constructed from \(\operatorname {step1\_ achieves\_ desideratum1}\) (giving Desideratum 1) and the hypothesis \(\operatorname {hexp}\) (giving Desideratum 2).
For natural numbers \(R\) and \(W\), the sparsified graph’s vertex count satisfies
Rewriting using the identity \(|\operatorname {SparsifiedVertex}(\operatorname {Fin}(W), R)| = (R+1) \cdot |\operatorname {Fin}(W)|\) and the fact that \(|\operatorname {Fin}(W)| = W\), the equality holds.
For natural numbers \(R\), \(K\), \(W\) with \(R \leq K \cdot (\log _2 W)^2\):
This follows directly from the sparsified vertex count bound established in Lemma 2.
Let \(G\) be a simple graph with a finite edge set, and let \(\{ \operatorname {cycles}(c)\} _{c \in C}\) be a collection of subsets of \(G.\operatorname {edgeSet}\). If every cycle \(c\) satisfies \(|\{ e \in G.\operatorname {edgeSet} \mid e \in \operatorname {cycles}(c)\} | \leq 4\), then \(\operatorname {LowWeightCycleBasis}(G, \operatorname {cycles}, 4)\) holds.
By definition, \(\operatorname {LowWeightCycleBasis}(G, \operatorname {cycles}, 4)\) requires exactly that every cycle has at most \(4\) edges, which is the hypothesis.
For natural numbers \(W\), \(R\), \(\Delta \), \(K\) with \(R \leq K \cdot (\log _2 W)^2\):
By monotonicity of multiplication on the right, it suffices to show \((R+1) \leq K \cdot (\log _2 W)^2 + 1\), which follows from \(R \leq K \cdot (\log _2 W)^2\) by integer arithmetic.
Let \(G\) be a simple graph on \(V\) with \(\operatorname {ConstantDegree}(G, \Delta )\). Then
This follows directly from the total qubits bounded theorem.
For natural numbers \(W\), \(R\), \(K\) with \(R \leq K \cdot (\log _2 W)^2\), \(K {\gt} 0\), and \(W \geq 2\):
By monotonicity of multiplication on the right, it suffices to show \((R+1) \leq K \cdot (\log _2 W)^2 + 1\), which follows from the hypothesis \(R \leq K \cdot (\log _2 W)^2\) by integer arithmetic.
Let \(G\) be a simple graph on \(V\) with \(\operatorname {ConstantDegree}(G, \Delta )\). For every vertex \(v \in V\):
This follows directly from the Gauss law checks weight bound.
Let \(G\) be a simple graph with cycles \(\{ \operatorname {cycles}(c)\} _{c \in C}\) satisfying \(\operatorname {LowWeightCycleBasis}(G, \operatorname {cycles}, W)\). For every plaquette \(p \in C\):
This follows directly from the flux checks weight bound.
Let \(G\) be a simple graph on \(V\) with checks \(\{ \operatorname {checks}(j)\} _{j \in J}\). Given a check index \(j\), an edge path \(\gamma : G.\operatorname {edgeSet} \to \mathbb {Z}/2\mathbb {Z}\), and a bound \(B\) such that \(|\{ e : \gamma (e) \neq 0\} | \leq B\), then
This follows directly from the deformed check edge bound.
Let \(G\) be a simple graph on \(V\) with \(\operatorname {SufficientExpansion}(G)\). For every nonempty subset \(S \subseteq V\) with \(2|S| \leq |V|\):
where \(\partial _G S\) is the edge boundary of \(S\) in \(G\).
This follows directly from the expansion gives boundary bound theorem.
Let \(G\) be a simple graph on \(V\) with checks \(\{ \operatorname {checks}(j)\} _{j \in J}\) and cycles \(\{ \operatorname {cycles}(c)\} _{c \in C}\). Suppose:
Every pair of distinct vertices in the \(Z\)-support of each check are adjacent in \(G\).
\(\operatorname {SufficientExpansion}(G)\) holds.
\(\operatorname {LowWeightCycleBasis}(G, \operatorname {cycles}, 4)\) holds.
\(\operatorname {ConstantDegree}(G, \Delta )\) holds.
Then \(\operatorname {AllDesiderataSatisfied}(G, \operatorname {cycles}, \operatorname {checks}, 1, 4)\).
The three components of \(\operatorname {AllDesiderataSatisfied}\) are constructed as a triple: \(\operatorname {step1\_ achieves\_ desideratum1}\) gives \(\operatorname {ShortPathsForDeformation}(G, \operatorname {checks}, 1)\), the hypothesis gives \(\operatorname {SufficientExpansion}(G)\), and the low-weight cycle basis hypothesis gives \(\operatorname {LowWeightCycleBasis}(G, \operatorname {cycles}, 4)\).
Let \(G\) be a simple graph on \(V\) with \(\operatorname {ConstantDegree}(G, \Delta )\), \(\operatorname {LowWeightCycleBasis}(G, \operatorname {cycles}, 4)\), and \(\operatorname {SufficientExpansion}(G)\). Then:
For all \(v \in V\): \(\operatorname {weight}(\operatorname {gaussLawChecks}(G, v)) \leq 1 + \Delta \).
For all \(p \in C\): \(\operatorname {weight}(\operatorname {fluxChecks}(G, \operatorname {cycles}, p)) \leq 4\).
\(G\) is a \(1\)-expander: \(\operatorname {IsExpander}(G, 1)\).
The three components are constructed as a triple:
For each vertex \(v\), the Gauss law check weight bound gives \(\operatorname {weight}(\operatorname {gaussLawChecks}(G, v)) \leq 1 + \Delta \).
For each plaquette \(p\), the flux check weight bound gives \(\operatorname {weight}(\operatorname {fluxChecks}(G, \operatorname {cycles}, p)) \leq 4\).
The sufficient expansion implies expander theorem gives \(\operatorname {IsExpander}(G, 1)\).
Let \(G\) be a connected simple graph on \(V\) with \(\operatorname {ConstantDegree}(G, \Delta )\), \(|V| \geq 2\), \(\operatorname {SufficientExpansion}(G)\), clique adjacency on each check’s \(Z\)-support, \(\operatorname {LowWeightCycleBasis}(G, \operatorname {cycles}, 4)\), and the cycle rank property \(|C| + |V| = |E(G)| + 1\). Given a positive bound parameter, the following all hold simultaneously:
\(\operatorname {AllDesiderataSatisfied}(G, \operatorname {cycles}, \operatorname {checks}, 1, 4)\).
Edge overhead is linear: \(2|E(G)| \leq \Delta \cdot |V|\).
Gauss checks bounded: \(\forall v,\; \operatorname {weight}(\operatorname {gaussLawChecks}(G, v)) \leq 1 + \Delta \).
Flux checks bounded: \(\forall p,\; \operatorname {weight}(\operatorname {fluxChecks}(G, \operatorname {cycles}, p)) \leq 4\).
Distance preserved: for all nonempty \(S \subseteq V\) with \(2|S| \leq |V|\), \(|S| \leq |\partial _G S|\).
Decongestion: there exist \(R\) and a layer assignment \(f : C \to \operatorname {Fin}(R+1)\) with \(\operatorname {LayerCycleDegreeBound}(\operatorname {cycles}, f, \operatorname {bound})\) and \(R \leq \Delta \cdot |V| / 2\).
The six-tuple is constructed from:
The construction satisfies all desiderata theorem gives the first component.
The constant degree bounds edges theorem gives \(2|E(G)| \leq \Delta \cdot |V|\).
For each vertex \(v\), the Gauss law checks weight bound applies.
For each plaquette \(p\), the flux checks weight bound applies.
For each valid subset \(S\), the expansion gives boundary bound applies.
The decongestion lemma bound provides the layer assignment with the required properties.
Let \(G\) be a connected simple graph on \(V\) with \(\operatorname {ConstantDegree}(G, \Delta )\), \(|V| \geq 2\), \(\operatorname {SufficientExpansion}(G)\), clique adjacency on each check’s \(Z\)-support, \(\operatorname {LowWeightCycleBasis}(G, \operatorname {cycles}, 4)\), the cycle rank property, and a König layer assignment \(f_0 : C \to \operatorname {Fin}(M+1)\) with \(\operatorname {LayerCycleDegreeBound}(\operatorname {cycles}, f_0, 1)\) and \(M \leq K \cdot (\log _2 |V|)^2\). Then for any positive \(c\):
\(\operatorname {AllDesiderataSatisfied}(G, \operatorname {cycles}, \operatorname {checks}, 1, 4)\).
There exist \(R\) and \(f : C \to \operatorname {Fin}(R+1)\) with \(\operatorname {LayerCycleDegreeBound}(\operatorname {cycles}, f, c)\) and \(R \leq K \cdot (\log _2 |V|)^2 / c\).
Distance preserved: for all nonempty \(S \subseteq V\) with \(2|S| \leq |V|\), \(|S| \leq |\partial _G S|\).
Vertex count bound: for all \(R \leq K \cdot (\log _2 |V|)^2 / c\), \((R+1) \cdot |V| \leq (K \cdot (\log _2 |V|)^2 / c + 1) \cdot |V|\).
We construct the four-tuple using a refinement:
The construction satisfies all desiderata theorem gives the first component.
The decongestion log-squared theorem, applied with \(\Delta \), the constant degree hypothesis, connectivity, \(|V| \geq 2\), the positivity of expansion (from \(\operatorname {sufficient\_ expansion\_ pos}\)), the cycles, \(c {\gt} 0\), the cycle rank property, and the König layer bound, provides \(R\) and \(f\) with the required properties.
For each valid subset \(S\), the expansion gives boundary bound applies.
For the vertex count bound, by monotonicity of multiplication on the right, it suffices to show \(R + 1 \leq K \cdot (\log _2 |V|)^2 / c + 1\), which follows from \(R \leq K \cdot (\log _2 |V|)^2 / c\) by integer arithmetic.
For natural numbers \(W\), \(R\), \(\Delta _{\mathrm{sp}}\) with \(R \leq (\log _2 W)^2\) and \(W {\gt} 0\):
By monotonicity of multiplication on the left (factor \(2\)) and on the right (factor \(W\)), it suffices to show \(R + 1 \leq (\log _2 W)^2 + 1\), which follows from \(R \leq (\log _2 W)^2\) by integer arithmetic.
For natural numbers \(W\), \(R\), \(K\) with \(R \leq K \cdot (\log _2 W)^2\) and \(W {\gt} 0\):
This follows immediately from the hypothesis \(R \leq K \cdot (\log _2 W)^2\) by integer arithmetic.
Let \(G\) be a simple graph on \(V\) with checks \(\{ \operatorname {checks}(j)\} _{j \in J}\), cycles \(\{ \operatorname {cycles}(c)\} _{c \in C}\), and deformed code data. Suppose: the cycles satisfy the even incidence property at every vertex, the checks pairwise commute, the original stabilizer code has parameters \([\! [n, k, d]\! ]\) with \(n = |V|\), \(n - |J| = k\), \(k \geq 1\), and the cycle rank property holds. Then the deformed stabilizer code satisfies
where \(n'\) and \(m'\) are the number of qubits and checks of the deformed code, respectively.
This follows directly from the codespace dimension change after gauging theorem.
I’ll start by reading the Lean file to understand its contents.Now I have the complete file. Let me produce the LaTeX translation.