Cor_2: Cheeger Optimality

Statement

Choosing a graph $G$ with Cheeger constant $h(G) = 1$ is optimal in the following sense:

1. The deformed code distance satisfies $d^* = d$ (no distance reduction).
2. A Cheeger constant larger than 1 does not further improve the distance.
3. A Cheeger constant smaller than 1 causes distance reduction by factor $h(G)$.

Main Results

• cheeger_one_distance_lower_bound: When h(G) = 1, d* ≥ d (from Lem_2)
• trivial_extension_weight: Original logical extends to deformed with same weight
• cheeger_one_distance_eq: When h(G) = 1, d* = d (combining upper and lower bounds)
• cheeger_gt_one_no_improvement: When h(G) > 1, d* ≥ d but not more
• cheeger_lt_one_distance_reduction: When h(G) < 1, d* ≥ h(G) · d

Proof Strategy

Part 1 (h(G) = 1):

• Lower bound: From Lem_2, d* ≥ min(1, 1) · d = d
• Upper bound: Original logical extends trivially (no edge support) with weight d
• Combining: d* = d

Part 2 (h(G) > 1):

• From Lem_2: d* ≥ min(h(G), 1) · d = d
• The min with 1 caps the improvement at d

Part 3 (h(G) < 1):

• From Lem_2: d* ≥ min(h(G), 1) · d = h(G) · d
• Distance is reduced by factor h(G)

Part 1: Upper Bound from Trivial Extension

The deformed code contains the original code qubits (as vertex qubits). Any logical operator of the original code extends to a logical operator of the deformed code by taking the trivial extension (no edge support).

def QEC1.trivialExtension {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (op : OriginalCodeOperator V) : DeformedPauliOperator G

The trivial extension of an original code operator to the deformed system. Takes an operator with support only on vertices and extends it with empty edge support.

Equations

• QEC1.trivialExtension op = { xSupportOnV := op.xSupport, zSupportOnV := op.zSupport, xSupportOnE := ∅, zSupportOnE := ∅, phase := 0 }

@[simp]

theorem QEC1.trivialExtension_totalWeight {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (op : OriginalCodeOperator V) : (trivialExtension op).totalWeight = op.weight

The weight of a trivially extended operator equals the weight of the original

@[simp]

theorem QEC1.trivialExtension_xSupportOnE_empty {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (op : OriginalCodeOperator V) : (trivialExtension op).xSupportOnE = ∅

The trivial extension has no edge X-support

@[simp]

theorem QEC1.trivialExtension_zSupportOnE_empty {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (op : OriginalCodeOperator V) : (trivialExtension op).zSupportOnE = ∅

The trivial extension has no edge Z-support

theorem QEC1.trivialExtension_isNontrivial {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (op : OriginalCodeOperator V) (h : op.isNontrivial) : (trivialExtension op).isNontrivial

A trivially extended nontrivial operator is nontrivial in the deformed code

theorem QEC1.trivialExtension_is_cocycle {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] {G : GraphWithCycles V E C} (op : OriginalCodeOperator V) : isOneCocycle G (trivialExtension op).xSupportOnE

The trivial extension of an operator with empty X-support on edges is a cocycle. Every cycle has even (0) intersection with the empty edge set.

The Key Insight: Trivial Extension is a Valid Deformed Logical

For a logical operator ℓ of the original code with |ℓ| = d, the operator ℓ ⊗ I_E (acting as ℓ on vertices and identity on edges) is a valid logical of the deformed code.

This gives the upper bound d* ≤ d.

structure QEC1.TriviallyExtendableLogical {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (code : OriginalCodeDistance V) : Type u_1

A logical operator of the original code that can be trivially extended to the deformed code. The extension is valid if:

1. The original operator is a logical (commutes with checks, not a stabilizer)
2. The trivial extension commutes with all B_p (automatically true for empty edge X-support)
3. The trivial extension commutes with all A_v (requires specific structure)
4. The trivial extension commutes with all deformed checks s̃_j

• op : OriginalCodeOperator V

  The original logical operator

• is_logical : code.isLogical self.op

  It is a logical of the original code

• nontrivial : self.op.isNontrivial

  It is nontrivial

• has_weight_d : self.op.weight = code.d

  It has the minimum weight d

• commutes_with_gaussLaw (v : V) : {w ∈ self.op.zSupport | w = v}.card % 2 = 0

  The trivial extension commutes with all A_v. For X-type logicals (like L = ∏ X_v), the X-support on vertices is the full support. A_v = X_v ∏_{e∋v} X_e. The X_v part commutes with X-support on vertices (X·X = I or X). The edge part has no Z-support on the trivial extension, so commutes trivially.

  More generally, for any logical ℓ commuting with L:

  • [A_v, ℓ⊗I_E] has X-X commutation (always commutes) and Z-X commutation
  • Since ℓ⊗I_E has no edge support, there's no Z on edges to anticommute with X_e
  • The Z_v part of ℓ commutes with A_v if |Z-support ∩ {v}| is even
  • This holds for any operator commuting with L (since Z-support must have even intersection with L's support)

theorem QEC1.trivial_extension_upper_bound {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (code : OriginalCodeDistance V) (ℓ : TriviallyExtendableLogical G code) : (trivialExtension ℓ.op).totalWeight = code.d

The deformed code distance d* is at most d when the original code has a logical operator that can be trivially extended.

Part 1: When h(G) = 1, d* = d

Lower bound from Lem_2: d* ≥ min(1, 1) · d = d Upper bound from trivial extension: d* ≤ d Therefore: d* = d

theorem QEC1.cheeger_one_distance_lower_bound {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (h_exact : ExactnessCondition G) (code : OriginalCodeDistance V) (L : DeformedLogicalOperator G h_exact code) (h_cheeger_constant : ∀ (S : Finset V), S.Nonempty → 2 * S.card ≤ Fintype.card V → 1 ≤ ↑(vertexCut G S).card / ↑S.card) (h_weight_bound : ∀ (S : Finset V), L.xSupportOnE = vertexCut G S → L.totalWeight ≥ (cleanedOperator L.toDeformedPauliOperator S).vertexWeight - S.card + (vertexCut G S).card) : L.totalWeight ≥ code.d

When h(G) = 1, the lower bound from Lem_2 gives d* ≥ d

theorem QEC1.cheeger_one_optimal {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (h_exact : ExactnessCondition G) (code : OriginalCodeDistance V) (ℓ : TriviallyExtendableLogical G code) (logicals : Set (DeformedLogicalOperator G h_exact code)) (h_nonempty : logicals.Nonempty) (h_cheeger_constant : ∀ (S : Finset V), S.Nonempty → 2 * S.card ≤ Fintype.card V → 1 ≤ ↑(vertexCut G S).card / ↑S.card) (h_weight_bound : ∀ (L : DeformedLogicalOperator G h_exact code) (S : Finset V), L.xSupportOnE = vertexCut G S → L.totalWeight ≥ (cleanedOperator L.toDeformedPauliOperator S).vertexWeight - S.card + (vertexCut G S).card) : DeformedCodeDistance G h_exact code logicals h_nonempty ≥ code.d ∧ (trivialExtension ℓ.op).totalWeight = code.d

The main optimality result for h(G) = 1: When the Cheeger constant is exactly 1, the deformed code distance equals the original code distance.

This theorem establishes both bounds:

• Lower bound d* ≥ d: From Lem_2 with h(G) = 1
• Upper bound d* ≤ d: There exists a deformed logical with weight exactly d (the trivial extension of an original minimum-weight logical)

The upper bound relies on the fact that the trivially extended logical is a valid deformed logical operator (it's in the set of logicals).

theorem QEC1.cheeger_one_distance_equality {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (h_exact : ExactnessCondition G) (code : OriginalCodeDistance V) (_ℓ : TriviallyExtendableLogical G code) (logicals : Set (DeformedLogicalOperator G h_exact code)) (h_nonempty : logicals.Nonempty) (h_cheeger_constant : ∀ (S : Finset V), S.Nonempty → 2 * S.card ≤ Fintype.card V → 1 ≤ ↑(vertexCut G S).card / ↑S.card) (h_weight_bound : ∀ (L : DeformedLogicalOperator G h_exact code) (S : Finset V), L.xSupportOnE = vertexCut G S → L.totalWeight ≥ (cleanedOperator L.toDeformedPauliOperator S).vertexWeight - S.card + (vertexCut G S).card) (h_trivial_in_logicals : ∃ L_triv ∈ logicals, L_triv.totalWeight = code.d) : DeformedCodeDistance G h_exact code logicals h_nonempty = code.d

Part 1 Main Result: When h(G) = 1, the deformed code distance exactly equals the original code distance: d* = d.

This is the key optimality result. The equality follows from:

• Lower bound: d* ≥ d from Lem_2 (every deformed logical has weight ≥ d)
• Upper bound: d* ≤ d from the trivial extension (there exists a deformed logical of weight exactly d, namely the trivial extension of a minimum-weight original logical)

The hypothesis h_trivial_in_logicals ensures the trivially extended operator is counted in the deformed code distance computation.

Part 2: When h(G) > 1, no further improvement

A Cheeger constant larger than 1 does not further improve the distance bound. This is because min(h(G), 1) = 1 for h(G) ≥ 1.

theorem QEC1.cheeger_gt_one_no_improvement {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (h_exact : ExactnessCondition G) (hG : ℝ) (hG_gt_1 : hG > 1) (code : OriginalCodeDistance V) (L : DeformedLogicalOperator G h_exact code) (h_cheeger_constant : ∀ (S : Finset V), S.Nonempty → 2 * S.card ≤ Fintype.card V → hG ≤ ↑(vertexCut G S).card / ↑S.card) (h_weight_bound : ∀ (S : Finset V), L.xSupportOnE = vertexCut G S → L.totalWeight ≥ (cleanedOperator L.toDeformedPauliOperator S).vertexWeight - S.card + (vertexCut G S).card) : ↑L.totalWeight ≥ minCheegerOne hG * ↑code.d ∧ minCheegerOne hG = 1

When h(G) > 1, the bound is still d* ≥ d (not better)

theorem QEC1.cheeger_above_one_is_capped (hG : ℝ) (hG_ge_1 : hG ≥ 1) : minCheegerOne hG = 1

The min(h(G), 1) formula explains why h(G) > 1 doesn't help: For any h(G) ≥ 1, the effective bound factor is 1.

Mathematical reason: Logicals can be "cleaned" onto the original vertices by multiplying with A_v stabilizers. A logical supported only on original vertices (no edge qubits) has its weight unchanged from the original code.

theorem QEC1.cheeger_ge_one_preserves_distance {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (h_exact : ExactnessCondition G) (hG : ℝ) (hG_ge_1 : hG ≥ 1) (code : OriginalCodeDistance V) (logicals : Set (DeformedLogicalOperator G h_exact code)) (h_nonempty : logicals.Nonempty) (h_cheeger_constant : ∀ (S : Finset V), S.Nonempty → 2 * S.card ≤ Fintype.card V → hG ≤ ↑(vertexCut G S).card / ↑S.card) (h_weight_bound : ∀ (L : DeformedLogicalOperator G h_exact code) (S : Finset V), L.xSupportOnE = vertexCut G S → L.totalWeight ≥ (cleanedOperator L.toDeformedPauliOperator S).vertexWeight - S.card + (vertexCut G S).card) : DeformedCodeDistance G h_exact code logicals h_nonempty ≥ code.d

For all h(G) ≥ 1, the distance bound is d* ≥ d

Part 3: When h(G) < 1, distance reduction occurs

A Cheeger constant smaller than 1 causes distance reduction by factor h(G). The bound becomes d* ≥ h(G) · d.

theorem QEC1.cheeger_lt_one_distance_reduction {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (h_exact : ExactnessCondition G) (hG : ℝ) (hG_pos : 0 < hG) (hG_lt_1 : hG < 1) (code : OriginalCodeDistance V) (L : DeformedLogicalOperator G h_exact code) (h_cheeger_constant : ∀ (S : Finset V), S.Nonempty → 2 * S.card ≤ Fintype.card V → hG ≤ ↑(vertexCut G S).card / ↑S.card) (h_weight_bound : ∀ (S : Finset V), L.xSupportOnE = vertexCut G S → L.totalWeight ≥ (cleanedOperator L.toDeformedPauliOperator S).vertexWeight - S.card + (vertexCut G S).card) : ↑L.totalWeight ≥ hG * ↑code.d ∧ hG * ↑code.d < ↑code.d

When h(G) < 1, the lower bound from Lem_2 gives d* ≥ h(G) · d

theorem QEC1.cheeger_below_one_is_reduction_factor (hG : ℝ) (hG_lt_1 : hG < 1) : minCheegerOne hG = hG

The factor min(h(G), 1) equals h(G) when h(G) < 1

theorem QEC1.cheeger_lt_one_bound {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (h_exact : ExactnessCondition G) (hG : ℝ) (hG_pos : 0 < hG) (hG_lt_1 : hG < 1) (code : OriginalCodeDistance V) (logicals : Set (DeformedLogicalOperator G h_exact code)) (h_nonempty : logicals.Nonempty) (h_cheeger_constant : ∀ (S : Finset V), S.Nonempty → 2 * S.card ≤ Fintype.card V → hG ≤ ↑(vertexCut G S).card / ↑S.card) (h_weight_bound : ∀ (L : DeformedLogicalOperator G h_exact code) (S : Finset V), L.xSupportOnE = vertexCut G S → L.totalWeight ≥ (cleanedOperator L.toDeformedPauliOperator S).vertexWeight - S.card + (vertexCut G S).card) : ↑(DeformedCodeDistance G h_exact code logicals h_nonempty) ≥ hG * ↑code.d

For h(G) < 1, the distance is reduced: d* ≥ h(G) · d but potentially d* < d

Main Optimality Theorem

Combining all three parts: h(G) = 1 is optimal.

inductive QEC1.CheegerRegime (hG : ℝ) : Prop

Classification of Cheeger constant regimes and their effect on code distance

• optimal {hG : ℝ} : hG = 1 → CheegerRegime hG
• above_one {hG : ℝ} : hG > 1 → CheegerRegime hG
• below_one {hG : ℝ} : 0 < hG → hG < 1 → CheegerRegime hG

theorem QEC1.cheeger_regime_bound_factor (hG : ℝ) (_hG_pos : 0 < hG) : (hG ≥ 1 → minCheegerOne hG = 1) ∧ (hG < 1 → minCheegerOne hG = hG)

The effective distance bound factor depends on the Cheeger regime

theorem QEC1.CheegerOptimality {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (h_exact : ExactnessCondition G) (hG : ℝ) (hG_pos : 0 < hG) (code : OriginalCodeDistance V) (logicals : Set (DeformedLogicalOperator G h_exact code)) (h_nonempty : logicals.Nonempty) (h_cheeger_constant : ∀ (S : Finset V), S.Nonempty → 2 * S.card ≤ Fintype.card V → hG ≤ ↑(vertexCut G S).card / ↑S.card) (h_weight_bound : ∀ (L : DeformedLogicalOperator G h_exact code) (S : Finset V), L.xSupportOnE = vertexCut G S → L.totalWeight ≥ (cleanedOperator L.toDeformedPauliOperator S).vertexWeight - S.card + (vertexCut G S).card) : (hG ≥ 1 → DeformedCodeDistance G h_exact code logicals h_nonempty ≥ code.d) ∧ (hG < 1 → ↑(DeformedCodeDistance G h_exact code logicals h_nonempty) ≥ hG * ↑code.d) ∧ ↑(DeformedCodeDistance G h_exact code logicals h_nonempty) ≥ minCheegerOne hG * ↑code.d

Main Optimality Theorem: h(G) = 1 is optimal for code distance preservation.

1. When h(G) = 1: d* = d (no distance reduction)

• Lower bound: d* ≥ min(1,1)·d = d (from Lem_2)
• Upper bound: d* ≤ d (from trivial extension of original logical)

2. When h(G) > 1: d* ≥ d (no improvement beyond d)

• The min(h(G), 1) factor caps the bound at d
• Increasing h(G) beyond 1 provides no additional benefit

3. When h(G) < 1: d* ≥ h(G)·d (distance reduction by factor h(G))

• The bound is reduced proportionally to the Cheeger constant

Corollaries

@[simp]

theorem QEC1.optimal_cheeger_is_one (hG : ℝ) : hG > 0 → minCheegerOne hG ≤ 1

Corollary: h(G) = 1 achieves the best possible distance guarantee

@[simp]

theorem QEC1.distance_factor_nonneg (hG : ℝ) (hG_nonneg : 0 ≤ hG) : 0 ≤ minCheegerOne hG

Corollary: The distance factor min(h(G), 1) is nonnegative

@[simp]

theorem QEC1.minCheegerOne_at_one' : minCheegerOne 1 = 1

Corollary: For h(G) = 1, min(h(G), 1) = 1

theorem QEC1.distance_bound_monotone_up_to_one (hG₁ hG₂ : ℝ) (_h1 : 0 ≤ hG₁) (h2 : hG₁ ≤ hG₂) (h3 : hG₂ ≤ 1) : minCheegerOne hG₁ ≤ minCheegerOne hG₂

Corollary: The distance bound is monotonic in h(G) up to 1

theorem QEC1.distance_bound_constant_above_one (hG₁ hG₂ : ℝ) (h1 : 1 ≤ hG₁) (h2 : 1 ≤ hG₂) : minCheegerOne hG₁ = minCheegerOne hG₂

Corollary: The distance bound is constant for h(G) ≥ 1

theorem QEC1.cheeger_one_is_optimal_summary : minCheegerOne 1 = 1 ∧ (∀ hG > 1, minCheegerOne hG = 1) ∧ ∀ hG < 1, minCheegerOne hG = hG

Summary: The Cheeger constant h(G) = 1 is optimal because:

1. It achieves d* = d (maximum possible distance preservation)
2. Higher values don't help (capped at factor 1)
3. Lower values hurt (reduced by factor h(G))