Rem_9: Worst-Case Graph Construction

Statement

A graph $G$ satisfying the desiderata in Rem_8 can be constructed with $O(W \log^2 W)$ qubit overhead, where $W = |\text{supp}(L)|$ is the weight of the logical operator being measured. The construction proceeds in three steps:

Step 1 (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. This ensures short paths between vertices in the $Z$-type support of each check.

Step 2 (Expansion): Add edges to $G$ until $h(G) \geq 1$. This can be done by randomly adding edges while preserving constant degree, or by overlaying an existing constant-degree expander graph. Let $G_0$ denote the graph constructed so far.

Step 3 (Cycle sparsification): Add $R$ additional layers that are copies of $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.

Formalization Approach

This remark describes a construction procedure citing external results. We formalize:

1. The structure of the three-step construction
2. Step 1 property: matched pairs have direct edges, giving path length 1
3. Overhead arithmetic: IF R = O(log² W) THEN total = O(W log² W) (PROVEN)
4. External results (expander existence, F-H decongestion) as SPECIFICATIONS

Main Results

• Step1MatchingProperty: Step 1 ensures matched pairs have path length 1
• vertexCountWithLayers: Vertex count formula W · (R + 1)
• overhead_bound_from_FH: IF R ≤ log²W + C THEN vertices ≤ O(W log² W)
• ExpanderExistenceSpec: Specification of expander existence (external)
• FreedmanHastingsSpec: Specification of F-H decongestion lemma (external)
• WorstCaseConstructionSpec: Full specification of what the construction produces

Step 1: Z₂-Perfect Matching

For each check with Z-type support overlapping L, we pick a Z₂-perfect matching of vertices in that support. Adding an edge for each matched pair ensures that matched vertices have a direct edge (path length 1).

theorem QEC1.Step1MatchingProperty {V : Type u_1} {G : SimpleGraph V} {u v : V} (hadj : G.Adj u v) : ∃ (w : G.Walk u v), w.length = 1

Step 1 matching property: For a matching on a set S, matched pairs (u,v) have a direct edge in the resulting graph, giving path length exactly 1.

Step 2: Expansion Edges - External Specification

Add edges until h(G) ≥ 1. This cites expander existence from random graph theory or explicit constructions (Ramanujan graphs, Margulis graphs).

def QEC1.ExpanderExistenceSpec : Prop

SPECIFICATION: Constant-degree expanders with h ≥ 1 exist for any W ≥ 2 vertices.

This is a cited result from the expander graph literature. Proving it requires either:

• Probabilistic method: random d-regular graphs are expanders with high probability
• Explicit constructions: Ramanujan graphs, Margulis-Gabber-Galil graphs, etc.

We state this as a specification capturing what the remark cites.

Equations

• QEC1.ExpanderExistenceSpec = ∀ W ≥ 2, ∃ (G : SimpleGraph (Fin W)) (x : DecidableRel G.Adj), (∃ (d : ℕ), ∀ (v : Fin W), G.degree v ≤ d) ∧ QEC1.IsStrongExpander G

Step 3: Cycle Sparsification - Freedman-Hastings Specification

The Freedman-Hastings decongestion lemma: adding R = O(log² W) layers of dummy vertices and triangulating cycles achieves constant cycle-degree.

def QEC1.FreedmanHastingsSpec : Prop

SPECIFICATION: Freedman-Hastings decongestion lemma.

For any constant-degree graph G₀ with W vertices:

• Adding R = O(log² W) layers of dummy vertices (copies of G₀)
• Connected sequentially to original vertices
• With cycles cellulated (triangulated) Achieves constant cycle-degree (all generating cycles have bounded weight).

This is a cited result from Freedman-Hastings requiring topological methods.

Equations

• QEC1.FreedmanHastingsSpec = ∃ C > 0, ∀ (W d : ℕ), W ≥ 2 → d ≥ 1 → ∃ (R : ℕ) (cycleWeightBound : ℕ), R ≤ C * Nat.log 2 W ^ 2 + C ∧ cycleWeightBound ≤ 3

Overhead Arithmetic

The key arithmetic: with W base vertices and R layers, total vertices = W · (R + 1). When R = O(log² W), this gives O(W log² W) total.

def QEC1.vertexCountWithLayers (W R : ℕ) : ℕ

Vertex count formula: W base vertices × (R + 1) total layers

Equations

• QEC1.vertexCountWithLayers W R = W * (R + 1)

@[simp]

theorem QEC1.vertexCountWithLayers_eq (W R : ℕ) : vertexCountWithLayers W R = W * R + W

theorem QEC1.vertexCountWithLayers_ge_W (W R : ℕ) : vertexCountWithLayers W R ≥ W

Vertex count is at least W (base graph)

theorem QEC1.overhead_bound_from_FH (W R C : ℕ) (hR : R ≤ C * Nat.log 2 W ^ 2 + C) : vertexCountWithLayers W R ≤ W * (C * Nat.log 2 W ^ 2 + C + 1)

Main overhead bound: IF the F-H bound R ≤ C · log²(W) + C holds, THEN total vertex count is ≤ W · (C · log²(W) + C + 1) = O(W log² W).

This is the PROVEN arithmetic consequence of the F-H specification.

The Complete Construction Specification

The full specification of what Remark 9 claims: a graph satisfying the Rem_8 desiderata can be constructed with O(W log² W) overhead.

def QEC1.WorstCaseConstructionSpec : Prop

Worst-Case Construction Specification

This captures the main claim of Remark 9: given the external results (expander existence, F-H decongestion), one can construct a graph G satisfying all three desiderata from Rem_8 with O(W log² W) qubit overhead.

We state this as a specification (not a proof) because the construction requires:

1. Expander existence (cited from random graph theory / explicit constructions)
2. Freedman-Hastings decongestion lemma (cited, requires topological methods)

Equations

• One or more equations did not get rendered due to their size.

theorem QEC1.construction_yields_desiderata : ExpanderExistenceSpec → FreedmanHastingsSpec → ∀ W ≥ 2, (∀ (G : SimpleGraph (Fin W)) (u v : Fin W), G.Adj u v → ∃ (w : G.Walk u v), w.length = 1) ∧ ∀ (R C : ℕ), R ≤ C * Nat.log 2 W ^ 2 + C → vertexCountWithLayers W R ≤ W * (C * Nat.log 2 W ^ 2 + C + 1)

The construction yields the three desiderata. This theorem states the logical structure of Remark 9's claim.

Summary

PROVEN (unconditional):

1. Step1MatchingProperty: Matched pairs have path length 1
2. overhead_bound_from_FH: R ≤ C·log²W + C ⟹ V ≤ W·(C·log²W + C + 1)
3. construction_yields_desiderata: The logical structure of the remark

SPECIFICATIONS (external results cited in the remark):

1. ExpanderExistenceSpec: Constant-degree expanders with h ≥ 1 exist
2. FreedmanHastingsSpec: F-H gives R = O(log² W) layers for constant cycle-degree

MAIN CLAIM:

• WorstCaseConstructionSpec: IF external specs hold, THEN construction produces a graph satisfying all three desiderata with O(W log² W) overhead