10 Rem 9: Worst-Case Graph Construction
This chapter formalizes the worst-case graph construction described in Remark 9 of [QEC1]. A graph \(G\) satisfying the desiderata from Remark 8 can be constructed with \(O(W \log ^2 W)\) qubit overhead, where \(W = |\mathrm{supp}(L)|\) is the weight of the logical operator being measured. The construction proceeds in three steps:
Perfect matching: For each original code check that overlaps the target logical \(L\), pick a \(\mathbb {Z}_2\)-perfect matching of the vertices in the \(Z\)-type support of that check. Add an edge to \(G\) for each pair of matched vertices, ensuring short paths (length 1) between matched vertices.
Expansion: Add edges to \(G\) until \(h(G) \ge 1\). This can be done by randomly adding edges while preserving constant degree, or by overlaying an existing constant-degree expander graph.
Cycle sparsification: Add \(R\) additional layers that are copies of the base graph \(G_0\) on dummy vertices, connected sequentially back to the original vertices. Add edges within each layer to cellulate (triangulate) cycles and reduce the cycle-degree. The Freedman–Hastings decongestion lemma establishes that \(R = O(\log ^2 W)\) layers suffice to achieve constant cycle-degree for any constant-degree graph with \(W\) vertices.
For a graph \(G\) on vertices \(V\) and any two adjacent vertices \(u, v \in V\) with \(G.\mathrm{Adj}(u,v)\), there exists a walk \(w\) from \(u\) to \(v\) of length exactly \(1\):
This captures the Step 1 property: matched pairs have a direct edge, giving path length 1.
We construct the walk explicitly as \(w = \mathrm{Walk.cons}(\mathrm{hadj},\, \mathrm{Walk.nil})\), which is the single-edge walk from \(u\) to \(v\) using the adjacency hypothesis \(\mathrm{hadj}\). Its length is \(1\) by reflexivity.
The expander existence specification is the proposition that for all \(W \ge 2\), there exists a simple graph \(G\) on \(\mathrm{Fin}(W)\) with decidable adjacency such that:
\(G\) has bounded degree: \(\exists \, d \in \mathbb {N}\) such that \(\forall \, v,\; \deg _G(v) \le d\);
\(G\) is a strong expander: \(\mathrm{IsStrongExpander}(G)\) holds (i.e., the Cheeger constant \(h(G) \ge 1\)).
This is a cited result from the expander graph literature (probabilistic method on random regular graphs, or explicit constructions such as Ramanujan graphs or Margulis–Gabber–Galil graphs).
The Freedman–Hastings decongestion specification asserts that there exists a constant \(C {\gt} 0\) such that for all \(W \ge 2\) and \(d \ge 1\) (representing any constant-degree-\(d\) graph on \(W\) vertices), there exist natural numbers \(R\) and \(\mathrm{cycleWeightBound}\) satisfying:
\(R \le C \cdot (\log _2 W)^2 + C\) (i.e., \(R = O(\log ^2 W)\));
\(\mathrm{cycleWeightBound} \le 3\) (all generating cycles have weight at most \(3\), achieved by triangulation).
This is a cited result from Freedman–Hastings requiring topological methods.
The vertex count with layers for \(W\) base vertices and \(R\) additional layers is defined as:
For all \(W, R \in \mathbb {N}\):
Unfolding the definition, \(\mathrm{vertexCountWithLayers}(W, R) = W \cdot (R + 1)\). By ring arithmetic, \(W \cdot (R + 1) = W \cdot R + W\).
For all \(W, R \in \mathbb {N}\):
Unfolding the definition, \(\mathrm{vertexCountWithLayers}(W, R) = W \cdot (R + 1)\). Since \(R + 1 \ge 1\) (as \(R + 1 = \mathrm{Nat.succ}(R) {\gt} 0\)), we have \(W \cdot (R + 1) \ge W \cdot 1 = W\) by \(\mathrm{Nat.le\_ mul\_ of\_ pos\_ right}\).
If \(R \le C \cdot (\log _2 W)^2 + C\), then
This is the proven arithmetic consequence of the Freedman–Hastings specification, showing \(O(W \log ^2 W)\) overhead.
Unfolding the definition, \(\mathrm{vertexCountWithLayers}(W, R) = W \cdot (R + 1)\). From the hypothesis \(R \le C \cdot (\log _2 W)^2 + C\), we deduce by integer arithmetic (omega) that \(R + 1 \le C \cdot (\log _2 W)^2 + C + 1\). The result then follows by \(\mathrm{Nat.mul\_ le\_ mul\_ left}\): multiplying both sides of this inequality by \(W\) yields \(W \cdot (R + 1) \le W \cdot (C \cdot (\log _2 W)^2 + C + 1)\).
The worst-case construction specification is the proposition:
More precisely, assuming expander existence and the Freedman–Hastings decongestion lemma, for every \(W \ge 2\) there exist types \(V\), \(E\), \(C\) (with decidable equality and finiteness) and a \(\mathrm{GraphWithCycles}\) structure \(G\) on \((V, E, C)\) together with a family of \(Z\)-type supports \(\mathrm{zTypeSupports}\), such that:
Desideratum 1 (Short paths): There exists \(\kappa \in \mathbb {N}\) such that \(\mathrm{ShortPathsProperty}(G.\mathrm{graph},\, \mathrm{zTypeSupports},\, \kappa )\) holds.
Desideratum 2 (Sufficient expansion): \(\mathrm{SufficientExpansion}(G.\mathrm{graph})\) holds.
Desideratum 3 (Low-weight cycles): \(\mathrm{LowWeightCyclesProperty}(G, 3)\) holds (all generating cycles have weight \(\le 3\)).
Overhead bound: There exists \(C \in \mathbb {N}\) with \(|V| \le W \cdot (C \cdot (\log _2 W)^2 + C + 1)\), i.e., \(O(W \log ^2 W)\) vertices.
Assuming \(\mathrm{ExpanderExistenceSpec}\) and \(\mathrm{FreedmanHastingsSpec}\), for every \(W \ge 2\):
Step 1 property: For any graph \(G\) on \(\mathrm{Fin}(W)\) and any adjacent vertices \(u, v\) with \(G.\mathrm{Adj}(u,v)\), there exists a walk of length \(1\) from \(u\) to \(v\).
Overhead arithmetic: For all \(R, C \in \mathbb {N}\) with \(R \le C \cdot (\log _2 W)^2 + C\), we have \(\mathrm{vertexCountWithLayers}(W, R) \le W \cdot (C \cdot (\log _2 W)^2 + C + 1)\).
Let the expander existence and Freedman–Hastings hypotheses be given. Let \(W \ge 2\). We prove both conjuncts separately using \(\mathrm{refine}\; \langle ?,\, ? \rangle \).
Part 1 (Step 1): Let \(G\) be a graph on \(\mathrm{Fin}(W)\), and let \(u, v\) be vertices with \(\mathrm{hadj} : G.\mathrm{Adj}(u,v)\). We apply \(\mathrm{Step1MatchingProperty}\) to \(\mathrm{hadj}\), which provides the desired walk of length \(1\).
Part 2 (Overhead): Let \(R, C \in \mathbb {N}\) with \(\mathrm{hR} : R \le C \cdot (\log _2 W)^2 + C\). We apply \(\mathrm{overhead\_ bound\_ from\_ FH}(W, R, C, \mathrm{hR})\) to obtain \(\mathrm{vertexCountWithLayers}(W, R) \le W \cdot (C \cdot (\log _2 W)^2 + C + 1)\).