Remark 11: Desiderata for Graph G

Statement

When choosing a constant-degree graph G for the gauging measurement, the goals are:

1. 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. This ensures the deformed checks have bounded weight.

2. Sufficient expansion: The Cheeger constant should satisfy h(G) ≥ 1. This ensures the deformed code has distance at least d (the original distance).

3. Low-weight cycle basis: There should exist a generating set of cycles where each cycle has weight at most some constant. This ensures 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, LDPC property preserved, and no distance reduction.

Main Results

• ShortPathsForDeformation : Desideratum 1 — bounded graph distance within Z-support
• SufficientExpansion : Desideratum 2 — Cheeger constant ≥ 1
• LowWeightCycleBasis : Desideratum 3 — bounded cycle weights
• AllDesiderataSatisfied : All three conditions bundled
• sufficient_expansion_implies_expander : h(G) ≥ 1 ⟹ G is a 1-expander
• low_weight_cycles_bound_flux_weight : bounded cycle weight ⟹ bounded flux weight
• constant_degree_bounds_edges : constant degree ⟹ linear edge overhead
• desiderata_consequences : combined summary theorem

Desideratum 1: Short Paths for Deformation

G should contain a constant-length edge-path between any pair of vertices that are in the Z-type support of the same original check. This ensures that the edge-path γ used in the deformation has bounded length, giving bounded-weight deformed checks.

def DesiderataForGraphG.ShortPathsForDeformation {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) {J : Type u_2} (checks : J → PauliOp V) (D : ℕ) : Prop

Desideratum 1: Short paths for deformation. For every original check s_j, any two vertices in the Z-support of s_j have graph distance at most D in G.

Equations

• DesiderataForGraphG.ShortPathsForDeformation G checks D = ∀ (j : J) (u v : V), u ∈ (checks j).supportZ → v ∈ (checks j).supportZ → G.dist u v ≤ D

theorem DesiderataForGraphG.short_paths_bound_distance {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {J : Type u_2} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (D : ℕ) (hsp : ShortPathsForDeformation G checks D) (j : J) (u v : V) (hu : u ∈ (checks j).supportZ) (hv : v ∈ (checks j).supportZ) : G.dist u v ≤ D

Short paths give a direct distance bound.

theorem DesiderataForGraphG.short_paths_imply_reachable {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {J : Type u_2} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (hconn : G.Connected) (j : J) (u v : V) (_hu : u ∈ (checks j).supportZ) (_hv : v ∈ (checks j).supportZ) : G.Reachable u v

On a connected graph, short paths guarantee reachability: vertices in the same Z-support are reachable from each other.

theorem DesiderataForGraphG.zSupport_card_le_weight {V : Type u_1} [Fintype V] [DecidableEq V] {J : Type u_2} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (j : J) : (checks j).supportZ.card ≤ (checks j).weight

The Z-support of a check is a subset of the full support, so its cardinality is bounded by the check weight.

theorem DesiderataForGraphG.deformed_check_edge_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {J : Type u_2} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) [Fintype ↑G.edgeSet] (j : J) (γ : ↑G.edgeSet → ZMod 2) (B : ℕ) (hγ : {e : ↑G.edgeSet | γ e ≠ 0}.card ≤ B) : {e : ↑G.edgeSet | (DeformedCode.deformedCheck G (checks j) γ).zVec (Sum.inr e) ≠ 0}.card ≤ B

Short paths bound the edge contribution to deformed checks. The deformed check s̃_j(γ) has Z-action on exactly those edges where γ(e) ≠ 0. If γ has at most B nonzero entries, the edge contribution is at most B.

@[simp]

theorem DesiderataForGraphG.deformed_check_zero_path_no_edges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {J : Type u_2} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) [Fintype ↑G.edgeSet] (j : J) : {e : ↑G.edgeSet | (DeformedCode.deformedCheck G (checks j) 0).zVec (Sum.inr e) ≠ 0}.card = 0

Zero edge-path adds no edge weight to the deformed check.

Desideratum 2: Sufficient Expansion

The Cheeger constant should satisfy h(G) ≥ 1. This ensures the deformed code has distance at least d (the original distance), as shown in Lemma 3.

def DesiderataForGraphG.SufficientExpansion {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Prop

Desideratum 2: Sufficient expansion. The Cheeger constant of G is at least 1.

Equations

• DesiderataForGraphG.SufficientExpansion G = (1 ≤ QEC1.cheegerConstant G)

theorem DesiderataForGraphG.sufficient_expansion_implies_expander {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hexp : SufficientExpansion G) : QEC1.SimpleGraph.IsExpander G 1

Sufficient expansion implies G is a 1-expander.

theorem DesiderataForGraphG.expansion_gives_boundary_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hexp : SufficientExpansion G) (S : Finset V) (hne : S.Nonempty) (hsize : 2 * S.card ≤ Fintype.card V) : ↑S.card ≤ ↑(QEC1.SimpleGraph.edgeBoundary G S).card

With sufficient expansion, every valid subset S has |∂S| ≥ |S|.

theorem DesiderataForGraphG.sufficient_expansion_pos {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hexp : SufficientExpansion G) : 0 < QEC1.cheegerConstant G

Sufficient expansion implies the Cheeger constant is positive.

Desideratum 3: Low-Weight Cycle Basis

There should exist a generating set of cycles for G where each cycle has weight at most some constant W. This ensures the flux operators B_p have bounded weight.

def DesiderataForGraphG.LowWeightCycleBasis {V : Type u_1} (G : SimpleGraph V) [Fintype ↑G.edgeSet] {C : Type u_2} (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (W : ℕ) : Prop

Desideratum 3: Low-weight cycle basis. Each cycle in the generating set has at most W edges.

Equations

• DesiderataForGraphG.LowWeightCycleBasis G cycles W = ∀ (c : C), {e : ↑G.edgeSet | e ∈ cycles c}.card ≤ W

theorem DesiderataForGraphG.low_weight_cycles_bound_flux_weight {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (W : ℕ) (hlw : LowWeightCycleBasis G cycles W) (p : C) : (DeformedCode.fluxChecks G cycles p).weight ≤ W

Low-weight cycles imply bounded flux check weight: the weight of B_p equals the number of edges in cycle p, so it is at most W.

theorem DesiderataForGraphG.all_flux_checks_bounded {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (W : ℕ) (hlw : LowWeightCycleBasis G cycles W) (p : C) : (DeformedCode.fluxChecks G cycles p).weight ≤ W

All flux checks are uniformly bounded when the cycle basis is low-weight.

Constant Degree and Edge Overhead

A constant-degree graph has edge count linear in vertex count, giving constant overhead per qubit in the support of L.

def DesiderataForGraphG.ConstantDegree {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (Δ : ℕ) : Prop

A constant-degree graph has maximum degree at most Δ.

Equations

• DesiderataForGraphG.ConstantDegree G Δ = ∀ (v : V), G.degree v ≤ Δ

theorem DesiderataForGraphG.constant_degree_bounds_edges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (Δ : ℕ) (hΔ : ConstantDegree G Δ) : 2 * Fintype.card ↑G.edgeSet ≤ Δ * Fintype.card V

Constant degree bounds edge count via the handshaking lemma: 2|E| = Σ_v deg(v) ≤ Δ · |V|.

theorem DesiderataForGraphG.edge_overhead_per_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (Δ : ℕ) (hΔ : ConstantDegree G Δ) (hV : 0 < Fintype.card V) : ↑(Fintype.card ↑G.edgeSet) / ↑(Fintype.card V) ≤ ↑Δ / 2

Constant overhead per vertex: the ratio |E|/|V| ≤ Δ/2.

theorem DesiderataForGraphG.total_qubits_bounded {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (Δ : ℕ) (hΔ : ConstantDegree G Δ) : 2 * (Fintype.card V + Fintype.card ↑G.edgeSet) ≤ (2 + Δ) * Fintype.card V

The total qubit count of the deformed code is |V| + |E|, which is at most |V| · (1 + Δ/2). We state a clean integer bound: 2·(|V| + |E|) ≤ (2 + Δ)·|V|.

Gauss Check Weight Characterization

The weight of the Gauss check A_v on V ⊕ E equals 1 + |incident edges|. The support of A_v consists of vertex v (contributing 1) and all incident edges.

theorem DesiderataForGraphG.gaussLawOp_xVec_inl {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v w : V) : (GaussFlux.gaussLawOp G v).xVec (Sum.inl w) = if w = v then 1 else 0

theorem DesiderataForGraphG.gaussLawOp_xVec_inr {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) (e : ↑G.edgeSet) : (GaussFlux.gaussLawOp G v).xVec (Sum.inr e) = if v ∈ ↑e then 1 else 0

theorem DesiderataForGraphG.gaussLaw_support_inl {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v w : V) : Sum.inl w ∈ (GaussFlux.gaussLawOp G v).support ↔ w = v

A_v acts nontrivially at vertex w iff w = v.

theorem DesiderataForGraphG.gaussLaw_support_inr {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) (e : ↑G.edgeSet) : Sum.inr e ∈ (GaussFlux.gaussLawOp G v).support ↔ v ∈ ↑e

A_v acts nontrivially at edge e iff v ∈ e.

theorem DesiderataForGraphG.gaussLaw_support_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : (GaussFlux.gaussLawOp G v).support = {Sum.inl v} ∪ Finset.map { toFun := Sum.inr, inj' := ⋯ } {e : ↑G.edgeSet | v ∈ ↑e}

The support of A_v is {Sum.inl v} ∪ {Sum.inr e | v ∈ e}.

theorem DesiderataForGraphG.gaussLaw_weight_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : (GaussFlux.gaussLawOp G v).weight = 1 + {e : ↑G.edgeSet | v ∈ ↑e}.card

The weight of A_v equals 1 + |incident edges of v|.

theorem DesiderataForGraphG.incident_edges_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : {e : ↑G.edgeSet | v ∈ ↑e}.card = (GaussFlux.incidentEdges G v).card

The incident edges count equals the incidentEdges cardinality.

theorem DesiderataForGraphG.gaussLaw_weight_eq_incident {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : (GaussFlux.gaussLawOp G v).weight = 1 + (GaussFlux.incidentEdges G v).card

The weight of A_v equals 1 + |incidentEdges|.

theorem DesiderataForGraphG.incidentEdges_card_eq_degree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : (GaussFlux.incidentEdges G v).card = G.degree v

The incident edge count equals the graph degree.

theorem DesiderataForGraphG.gaussLaw_weight_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) (Δ : ℕ) (hΔ : ConstantDegree G Δ) : (GaussFlux.gaussLawOp G v).weight ≤ 1 + Δ

On a constant-degree graph, A_v has weight at most 1 + Δ.

All Desiderata Satisfied

When all three conditions hold with constants independent of n, the deformed code has bounded check weight and bounded qubit degree (LDPC property preserved), with no distance reduction.

structure DesiderataForGraphG.AllDesiderataSatisfied {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} (checks : J → PauliOp V) (D W : ℕ) : Prop

All three desiderata satisfied with given constants.

• short_paths : ShortPathsForDeformation G checks D
• expansion : SufficientExpansion G
• low_weight_cycles : LowWeightCycleBasis G cycles W

theorem DesiderataForGraphG.desiderata_imply_bounded_flux_weight {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (D W : ℕ) (hall : AllDesiderataSatisfied G cycles checks D W) (p : C) : (DeformedCode.fluxChecks G cycles p).weight ≤ W

When all desiderata are satisfied, the flux checks have bounded weight.

theorem DesiderataForGraphG.desiderata_imply_expander {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (D W : ℕ) (hall : AllDesiderataSatisfied G cycles checks D W) : QEC1.SimpleGraph.IsExpander G 1

When all desiderata are satisfied, the graph is an expander.

theorem DesiderataForGraphG.desiderata_imply_no_distance_loss {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (D W : ℕ) (hall : AllDesiderataSatisfied G cycles checks D W) (S : Finset V) (hne : S.Nonempty) (hsize : 2 * S.card ≤ Fintype.card V) : ↑S.card ≤ ↑(QEC1.SimpleGraph.edgeBoundary G S).card

When all desiderata are satisfied, every valid vertex subset has boundary at least as large as itself — preventing distance loss.

LDPC Preservation Characterization

The deformed code has three families of checks:

• Gauss checks A_v: weight = 1 + deg(v) (bounded by 1 + Δ on a degree-Δ graph)
• Flux checks B_p: weight = |cycle p| (bounded by W)
• Deformed checks s̃_j: vertex weight from original + edge weight from path γ_j All are bounded when the desiderata hold with constant bounds.

def DesiderataForGraphG.DeformedCodeIsLDPC {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (w_bound c_bound : ℕ) : Prop

The LDPC property of the deformed code, using the existing IsQLDPC predicate.

Equations

• DesiderataForGraphG.DeformedCodeIsLDPC G cycles checks data hcyc hcomm w_bound c_bound = IsQLDPC (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm) w_bound c_bound

theorem DesiderataForGraphG.gaussLaw_checks_weight_bounded {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (Δ : ℕ) (hΔ : ConstantDegree G Δ) (v : V) : (DeformedCode.gaussLawChecks G v).weight ≤ 1 + Δ

Gauss check weights are bounded on constant-degree graphs.

theorem DesiderataForGraphG.flux_checks_weight_bounded {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (W : ℕ) (hlw : LowWeightCycleBasis G cycles W) (p : C) : (DeformedCode.fluxChecks G cycles p).weight ≤ W

Flux check weights are bounded by the cycle basis weight bound.

Summary: All Three Conditions Together

The three desiderata together ensure the deformed code is a good qLDPC code:

1. Flux checks have bounded weight (from low-weight cycle basis)
2. G is an expander with h(G) ≥ 1 (from sufficient expansion) — no distance loss
3. Edge overhead is linear in |V| (from constant degree) — constant overhead per qubit
4. Short paths ensure deformed checks have bounded weight

theorem DesiderataForGraphG.desiderata_consequences {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (D W Δ : ℕ) (_hsp : ShortPathsForDeformation G checks D) (hexp : SufficientExpansion G) (hlw : LowWeightCycleBasis G cycles W) (hΔ : ConstantDegree G Δ) : (∀ (p : C), (DeformedCode.fluxChecks G cycles p).weight ≤ W) ∧ QEC1.SimpleGraph.IsExpander G 1 ∧ 2 * Fintype.card ↑G.edgeSet ≤ Δ * Fintype.card V ∧ ∀ (v : V), (DeformedCode.gaussLawChecks G v).weight ≤ 1 + Δ

Summary theorem: when all three desiderata and constant degree are satisfied, the key consequences hold simultaneously.

theorem DesiderataForGraphG.overhead_per_vertex_bounded {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] {J : Type u_3} [Fintype J] [DecidableEq J] (checks : J → PauliOp V) (D W Δ : ℕ) (_hsp : ShortPathsForDeformation G checks D) (_hexp : SufficientExpansion G) (_hlw : LowWeightCycleBasis G cycles W) (hΔ : ConstantDegree G Δ) (hV : 0 < Fintype.card V) : ↑(Fintype.card ↑G.edgeSet) / ↑(Fintype.card V) ≤ ↑Δ / 2

The additional qubit overhead (edge count) per vertex of L is bounded.