Lemma 3: Space Distance #
Statement #
Let G be the graph used in the gauging measurement procedure for a logical operator L in an [[n,k,d]] stabilizer code. Let d* denote the distance of the deformed code. Then: d* ≥ min(h(G), 1) · d where h(G) is the Cheeger constant of G and d is the distance of the original code.
In particular, if h(G) ≥ 1, then d* ≥ d.
Main Results #
restrictToV: restriction of a Pauli operator on V ⊕ E to VgaussSubsetProduct_mem_stabilizerGroup: gaussSubsetProduct is in deformed stabilizer groupedgeXSupport_in_ker_secondCoboundary: edge X-support of logical is a cocycle (Step 2)cleaned_restriction_logical_disjunction: at least one cleaned restriction is a logicalconstruct_wlog: derives WLOG cleaning vector from exactness + cocycle + Step 4 hypothesisdistance_ge_min_cheeger_one_mul_d: d* ≥ min(h(G), 1) · ddeformed_distance_ge_d_sufficient_expansion: if h(G) ≥ 1 then d* ≥ d
Corollaries #
deformed_distance_ge_min_cheeger_d: d* ≥ min(h(G), 1) · d (at code distance level)
Step 1: Restriction to Vertex Qubits #
def
SpaceDistance.restrictToV
{V : Type u_1}
(G : SimpleGraph V)
(P : PauliOp (GaussFlux.ExtQubit G))
:
PauliOp V
Restriction of a Pauli operator on V ⊕ E to vertex qubits V.
Equations
Instances For
@[simp]
theorem
SpaceDistance.restrictToV_xVec
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
(v : V)
:
@[simp]
theorem
SpaceDistance.restrictToV_zVec
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
(v : V)
:
@[simp]
theorem
SpaceDistance.restrictToV_one
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
:
@[simp]
theorem
SpaceDistance.restrictToV_mul
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P Q : PauliOp (GaussFlux.ExtQubit G))
:
Step 2: Cleaning a Logical Operator #
def
SpaceDistance.edgeXSupport
{V : Type u_1}
(G : SimpleGraph V)
(P : PauliOp (GaussFlux.ExtQubit G))
:
The X-support vector of P on edge qubits.
Equations
- SpaceDistance.edgeXSupport G P e = P.xVec (Sum.inr e)
Instances For
def
SpaceDistance.cleanedOp
{V : Type u_1}
(G : SimpleGraph V)
[Fintype ↑G.edgeSet]
(L' : PauliOp (GaussFlux.ExtQubit G))
(c : V → ZMod 2)
:
The cleaned operator: L' multiplied by gaussSubsetProduct(c).
Equations
Instances For
theorem
SpaceDistance.cleanedOp_xVec_edge
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(L' : PauliOp (GaussFlux.ExtQubit G))
(c : V → ZMod 2)
(e : ↑G.edgeSet)
:
The cleaned operator has X-vector on edges equal to original plus coboundary of c.
theorem
SpaceDistance.cleanedOp_xVec_vertex
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(L' : PauliOp (GaussFlux.ExtQubit G))
(c : V → ZMod 2)
(v : V)
:
The cleaned operator has X-vector on vertices equal to original plus c.
theorem
SpaceDistance.cleanedOp_zVec
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(L' : PauliOp (GaussFlux.ExtQubit G))
(c : V → ZMod 2)
:
The cleaned operator preserves Z-vector (gaussSubsetProduct is pure X).
theorem
SpaceDistance.cleaned_has_no_xSupport_on_edges
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(L' : PauliOp (GaussFlux.ExtQubit G))
(c : V → ZMod 2)
(hcob : ∀ (e : ↑G.edgeSet), (GraphMaps.coboundaryMap G) c e = L'.xVec (Sum.inr e))
(e : ↑G.edgeSet)
:
If coboundary of c equals the edge X-support of L', then cleaned op has zero X-support on edges.
Step 3: Cleaned operator restricted to V commutes with original checks #
theorem
SpaceDistance.symplecticInner_noXEdge_deformed
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
(checks : J → PauliOp V)
(Lbar : PauliOp (GaussFlux.ExtQubit G))
(data : DeformedCode.DeformedCodeData G checks)
(hnoX : ∀ (e : ↑G.edgeSet), Lbar.xVec (Sum.inr e) = 0)
(j : J)
:
Lbar.symplecticInner (DeformedCode.deformedOriginalChecks G checks data j) = (restrictToV G Lbar).symplecticInner (checks j)
The symplectic inner product of Lbar with a deformed check equals the symplectic inner product of Lbar|_V with the original check, when Lbar has no X on edges.
theorem
SpaceDistance.cleaned_commutes_with_original_check
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
(checks : J → PauliOp V)
(Lbar : PauliOp (GaussFlux.ExtQubit G))
(data : DeformedCode.DeformedCodeData G checks)
(hnoX : ∀ (e : ↑G.edgeSet), Lbar.xVec (Sum.inr e) = 0)
(j : J)
(hcomm : Lbar.PauliCommute (DeformedCode.deformedOriginalChecks G checks data j))
:
(restrictToV G Lbar).PauliCommute (checks j)
If Lbar commutes with deformed check s̃_j and has no X on edges, then Lbar|_V commutes with s_j.
theorem
SpaceDistance.cleaned_commutes_with_all_original_checks
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
(checks : J → PauliOp V)
(Lbar : PauliOp (GaussFlux.ExtQubit G))
(data : DeformedCode.DeformedCodeData G checks)
(hnoX : ∀ (e : ↑G.edgeSet), Lbar.xVec (Sum.inr e) = 0)
(hcomm_all : ∀ (j : J), Lbar.PauliCommute (DeformedCode.deformedOriginalChecks G checks data j))
(j : J)
:
(restrictToV G Lbar).PauliCommute (checks j)
If Lbar commutes with all deformed checks and has no X on edges, then Lbar|_V commutes with all original checks.
Step 4: gaussSubsetProduct commutes with all deformed code checks #
theorem
SpaceDistance.gaussSubsetProduct_comm_deformedCheck
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
(checks : J → PauliOp V)
(data : DeformedCode.DeformedCodeData G checks)
(c : V → ZMod 2)
(j : J)
:
(GaugingMeasurementCorrectness.gaussSubsetProduct G c).PauliCommute
(DeformedCode.deformedOriginalChecks G checks data j)
The gaussSubsetProduct commutes with deformed checks. Proof: gaussSubsetProduct(c) = ∏_{v : c v = 1} A_v, and each A_v commutes with the deformed check by the boundary condition.
theorem
SpaceDistance.gaussSubsetProduct_comm_gaussLaw
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(c : V → ZMod 2)
(v : V)
:
The gaussSubsetProduct commutes with gaussLaw checks (both pure X).
theorem
SpaceDistance.gaussSubsetProduct_comm_flux
{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]
(hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card)
(c : V → ZMod 2)
(p : C)
:
(GaugingMeasurementCorrectness.gaussSubsetProduct G c).PauliCommute (DeformedCode.fluxChecks G cycles p)
The gaussSubsetProduct commutes with flux checks.
theorem
SpaceDistance.gaussSubsetProduct_comm_allChecks
{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)
(c : V → ZMod 2)
(a : DeformedCode.CheckIndex V C J)
:
(GaugingMeasurementCorrectness.gaussSubsetProduct G c).PauliCommute
(DeformedCode.deformedCodeChecks G cycles checks data a)
The gaussSubsetProduct commutes with all checks of the deformed code.
theorem
SpaceDistance.gaussSubsetProduct_inCentralizer
{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))
(c : V → ZMod 2)
:
(DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).inCentralizer
(GaugingMeasurementCorrectness.gaussSubsetProduct G c)
gaussSubsetProduct is in the centralizer of the deformed code.
gaussSubsetProduct is in the Stabilizer Group #
theorem
SpaceDistance.gaussSubsetProduct_mem_stabilizerGroup
{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))
(c : V → ZMod 2)
:
GaugingMeasurementCorrectness.gaussSubsetProduct G c ∈ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup
gaussSubsetProduct is in the stabilizer group of the deformed code. This follows because gaussSubsetProduct(c) = ∏_{v : c v = 1} A_v, and each A_v is a check of the deformed code.
Weight Decomposition #
theorem
SpaceDistance.weight_eq_vertex_plus_edge
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
:
Weight of a Pauli on V ⊕ E decomposes as vertex + edge contributions.
theorem
SpaceDistance.weight_decomposition
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
:
The weight of P on V ⊕ E equals the weight of its restriction plus edge support.
Step 4 (Paper): Restriction to original qubits is a logical of the original code #
The key insight: the two cleaned operators (with c and c + 1) differ by the logical L on vertices. If both restrictions were in the original stabilizer group, their product (= L|_V) would be too, contradicting L being a logical of the original code.
theorem
SpaceDistance.restrictToV_logicalOp
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
:
The restriction of the logical operator L to V is the all-X operator.
theorem
SpaceDistance.cleanedOp_complement_eq_mul_logical
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(L' : PauliOp (GaussFlux.ExtQubit G))
(c : V → ZMod 2)
:
The two cleaned operators (with c and c + allOnes) differ by L on the extended system.
theorem
SpaceDistance.restrictToV_cleanedOp_complement
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(L' : PauliOp (GaussFlux.ExtQubit G))
(c : V → ZMod 2)
:
restrictToV G (cleanedOp G L' (c + fun (x : V) => 1)) = restrictToV G (cleanedOp G L' c) * GaugingMeasurementCorrectness.logicalOpV
The restrictions of the two cleaned operators differ by logicalOpV.
theorem
SpaceDistance.cleanedOp_not_in_stabilizerGroup
{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))
(L' : PauliOp (GaussFlux.ExtQubit G))
(hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L')
(c : V → ZMod 2)
:
cleanedOp G L' c ∉ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup
If L' is a logical of the deformed code and gaussSubsetProduct(c) is a stabilizer, then cleanedOp = L' * gaussSubsetProduct(c) is not in the deformed stabilizer group.
theorem
SpaceDistance.cleanedOp_ne_one
{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))
(L' : PauliOp (GaussFlux.ExtQubit G))
(hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L')
(c : V → ZMod 2)
:
If L' is a logical of the deformed code, then cleanedOp is not identity.
theorem
SpaceDistance.cleanedOp_isLogical
{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))
(L' : PauliOp (GaussFlux.ExtQubit G))
(hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L')
(c : V → ZMod 2)
:
(DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp (cleanedOp G L' c)
The cleaned operator is a logical of the deformed code.
theorem
SpaceDistance.cleaned_restriction_logical_disjunction
{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)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j)
(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))
(hL_logical : origCode.isLogicalOp GaugingMeasurementCorrectness.logicalOpV)
(L' : PauliOp (GaussFlux.ExtQubit G))
(hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L')
(c : V → ZMod 2)
(hc : (GraphMaps.coboundaryMap G) c = edgeXSupport G L')
:
origCode.isLogicalOp (restrictToV G (cleanedOp G L' c)) ∨ origCode.isLogicalOp (restrictToV G (cleanedOp G L' (c + fun (x : V) => 1)))
Key theorem (Step 4): At least one of the two cleaned restrictions is a logical of the original code.
Step 2: Edge X-support is a cocycle #
The edge X-support of a logical operator L' of the deformed code lies in ker(δ₂), i.e., it is a 1-cocycle. This follows because L' commutes with all flux checks B_p, and the symplectic inner product ⟨L', B_p⟩ equals δ₂(edgeXSupport(L'))(p).
theorem
SpaceDistance.symplecticInner_flux_eq_secondCoboundary
{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]
(L' : PauliOp (GaussFlux.ExtQubit G))
(p : C)
:
L'.symplecticInner (DeformedCode.fluxChecks G cycles p) = (GraphMaps.secondCoboundaryMap G cycles) (edgeXSupport G L') p
The symplectic inner product of L' with a flux check equals the second coboundary of the edge X-support applied to that cycle.
theorem
SpaceDistance.edgeXSupport_in_ker_secondCoboundary
{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))
(L' : PauliOp (GaussFlux.ExtQubit G))
(hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L')
:
Step 2 (Paper): The edge X-support of a logical operator of the deformed code is a cocycle (lies in ker δ₂). This follows from L' commuting with all flux checks.
Coboundary Support equals Edge Boundary #
theorem
SpaceDistance.coboundary_support_card_eq_edgeBoundary_card
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(c : V → ZMod 2)
:
{e : ↑G.edgeSet | (GraphMaps.coboundaryMap G) c e ≠ 0}.card = (QEC1.SimpleGraph.edgeBoundary G {v : V | c v ≠ 0}).card
The coboundary support of c (edges where δc ≠ 0) has the same cardinality as the edge boundary of the support of c.
theorem
SpaceDistance.edge_support_ge_coboundary_support
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(L' : PauliOp (GaussFlux.ExtQubit G))
(c : V → ZMod 2)
(hc : (GraphMaps.coboundaryMap G) c = edgeXSupport G L')
:
The edge support of L' is at least the coboundary support of c₀.
theorem
SpaceDistance.support_add_complement_card
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(c : V → ZMod 2)
:
The supports of c and c+1 partition V: |supp(c)| + |supp(c+1)| = |V|.
theorem
SpaceDistance.coboundary_add_ones_eq
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(c : V → ZMod 2)
:
The coboundary of c and c+1 are the same (since δ(1) = 0).
Step 4 (Paper): Any cleaning gives a logical of the original code #
The key structural argument: given boundary exactness (ker(∂) = im(∂₂)), we show that for ANY cleaning vector c with δc = edgeXSupport(L'), the restriction restrictToV(cleanedOp(L', c)) is a logical of the original code.
The proof proceeds by contradiction:
- Case (b): If the restriction is identity on V, the cleaned operator is a pure-Z edge operator. Its Z-support on edges lies in ker(∂), hence in im(∂₂) by boundary exactness, making it a product of flux operators ∈ stabilizer group. Contradiction.
- Case (a): If the restriction is in origCode.stabilizerGroup, we lift it to a deformed stabilizer using closure induction. The quotient is again a pure-Z edge operator in the centralizer, and the same argument applies. Contradiction.
theorem
SpaceDistance.restrictToV_deformedOriginalCheck
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
(checks : J → PauliOp V)
(data : DeformedCode.DeformedCodeData G checks)
(j : J)
:
The restriction of a deformed original check to V equals the original check.
theorem
SpaceDistance.restrictToV_fluxChecks
{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]
(p : C)
:
The restriction of a flux check to V is identity.
theorem
SpaceDistance.restrictToV_gaussLawChecks_xVec
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(w v : V)
:
The restriction of a gaussLaw check to V has X at v and no Z.
theorem
SpaceDistance.restrictToV_gaussLawChecks_zVec
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(w v : V)
:
theorem
SpaceDistance.pureZEdgeOp_mul
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(δ₁ δ₂ : ↑G.edgeSet → ZMod 2)
:
Multiplication of pure-Z edge operators adds their edge vectors.
theorem
SpaceDistance.pureZEdgeOp_single_cycle_eq_fluxChecks
{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]
(c : C)
:
(FreedomInDeformedChecks.pureZEdgeOp G fun (e : ↑G.edgeSet) => if e ∈ cycles c then 1 else 0) = DeformedCode.fluxChecks G cycles c
The pure-Z edge operator for a single cycle indicator equals the flux check.
@[simp]
theorem
SpaceDistance.pureZEdgeOp_zero
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
:
An operator equal to a pure-Z edge operator with δ = 0 is identity.
theorem
SpaceDistance.pureZEdgeOp_mem_stabilizerGroup_of_range
{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))
(δ : ↑G.edgeSet → ZMod 2)
(hδ : δ ∈ (GraphMaps.secondBoundaryMap G cycles).range)
:
FreedomInDeformedChecks.pureZEdgeOp G δ ∈ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup
If δ is in the image of ∂₂, then pureZEdgeOp(δ) is a product of flux checks, hence in the deformed stabilizer group.
theorem
SpaceDistance.cleaned_not_identity_on_V
{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))
(hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range)
(L' : PauliOp (GaussFlux.ExtQubit G))
(hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L')
(c : V → ZMod 2)
(hc : (GraphMaps.coboundaryMap G) c = edgeXSupport G L')
(hrestrict : restrictToV G (cleanedOp G L' c) = 1)
:
If Lbar is a logical of the deformed code, has no X on edges, and restrictToV(Lbar) = 1, then with boundary exactness, Lbar is in the deformed stabilizer group (contradiction).
theorem
SpaceDistance.lift_originalStabilizer_to_deformed
{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)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j)
(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))
(S : PauliOp V)
(hS : S ∈ origCode.stabilizerGroup)
:
∃ S_tilde ∈ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup,
restrictToV G S_tilde = S ∧ ∀ (e : ↑G.edgeSet), S_tilde.xVec (Sum.inr e) = 0
Lifting: for any element S of the original stabilizer group, there exists S̃ in the deformed stabilizer group with restrictToV(S̃) = S and no X on edges.
theorem
SpaceDistance.cleaned_not_stabilizer_on_V
{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)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j)
(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))
(hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range)
(L' : PauliOp (GaussFlux.ExtQubit G))
(hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L')
(c : V → ZMod 2)
(hc : (GraphMaps.coboundaryMap G) c = edgeXSupport G L')
(hrestrict : restrictToV G (cleanedOp G L' c) ∈ origCode.stabilizerGroup)
:
If Lbar is a logical of the deformed code, has no X on edges, and restrictToV(Lbar) is in the original stabilizer group, then with boundary exactness, Lbar is in the deformed stabilizer group (contradiction).
theorem
SpaceDistance.any_cleaning_gives_logical
{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)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j)
(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))
(hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range)
(_hL_logical : origCode.isLogicalOp GaugingMeasurementCorrectness.logicalOpV)
(L' : PauliOp (GaussFlux.ExtQubit G))
(hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L')
(c : V → ZMod 2)
(hc_cob : (GraphMaps.coboundaryMap G) c = edgeXSupport G L')
:
origCode.isLogicalOp (restrictToV G (cleanedOp G L' c))
Step 4 (Paper): Any cleaning of L' restricted to V is a logical of the original code. Given boundary exactness (ker(∂) ⊆ im(∂₂)), for any c with δc = edgeXSupport(L'), the restriction restrictToV(cleanedOp(L', c)) is a logical of the original code.
Constructing the WLOG hypothesis #
From the cocycle condition and exactness, we obtain a cleaning vector c. From the disjunction and support partition, we show there exists a c with small support that gives a logical restriction.
theorem
SpaceDistance.construct_wlog
{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)
(origCode : StabilizerCode V)
(_hJ : origCode.I = J)
(_hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j)
(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))
(hexact : ∀ γ ∈ (GraphMaps.secondCoboundaryMap G cycles).ker, ∃ (c : V → ZMod 2), (GraphMaps.coboundaryMap G) c = γ)
(hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range)
(_hL_logical : origCode.isLogicalOp GaugingMeasurementCorrectness.logicalOpV)
(L' : PauliOp (GaussFlux.ExtQubit G))
(hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L')
:
∃ (c : V → ZMod 2),
(GraphMaps.coboundaryMap G) c = edgeXSupport G L' ∧ origCode.isLogicalOp (restrictToV G (cleanedOp G L' c)) ∧ 2 * {v : V | c v ≠ 0}.card ≤ Fintype.card V
Construction of the WLOG cleaning vector. Given exactness of both sequences and that any cleaning gives a logical (derived from boundary exactness), we find c with δc = edgeXSupport(L'), the restriction is a logical, and |supp(c)| ≤ |V|/2.
Arithmetic Core of the Distance Bound #
theorem
SpaceDistance.weight_lower_bound_arithmetic
(w d suppC_card coboundary_card : ℕ)
(h_cheeger : ℝ)
(h_cheeger_nn : 0 ≤ h_cheeger)
(hw_ge_vertex_minus_plus_edge : w + suppC_card ≥ d + coboundary_card)
(h_coboundary_ge : h_cheeger * ↑suppC_card ≤ ↑coboundary_card)
(hw_ge_coboundary : coboundary_card ≤ w)
:
Core arithmetic lemma for the distance bound.
Vertex Weight Bound #
theorem
SpaceDistance.vertex_weight_plus_c_ge_cleaned_weight
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(L' : PauliOp (GaussFlux.ExtQubit G))
(c : V → ZMod 2)
:
The vertex weight of L' plus the size of c's support is at least the vertex weight of the cleaned operator restricted to V.
Cheeger bound for a specific cleaning vector #
Main Distance Bound Theorem #
theorem
SpaceDistance.distance_ge_min_cheeger_one_mul_d
{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)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j)
(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))
(_hconn : G.Connected)
(_hcard : 2 ≤ Fintype.card V)
(hexact : ∀ γ ∈ (GraphMaps.secondCoboundaryMap G cycles).ker, ∃ (c : V → ZMod 2), (GraphMaps.coboundaryMap G) c = γ)
(hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range)
(hL_logical : origCode.isLogicalOp GaugingMeasurementCorrectness.logicalOpV)
(L' : PauliOp (GaussFlux.ExtQubit G))
(hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L')
:
Lemma 3 (Space Distance): Per-operator bound. d* ≥ min(h(G), 1) · d
If L' is logical and gaussSubsetProduct is a stabilizer, the product is equivalent #
theorem
SpaceDistance.logical_mul_stabilizer
{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))
(L' : PauliOp (GaussFlux.ExtQubit G))
(hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L')
(s : PauliOp (GaussFlux.ExtQubit G))
(hs : s ∈ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup)
(hne : L' * s ≠ 1)
:
(DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp (L' * s) ∨ L' * s ∈ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup
If L' is logical and s is a stabilizer, then L' * s is logical or a stabilizer.
Sufficient Expansion Corollary #
theorem
SpaceDistance.distance_ge_d_of_sufficient_expansion
{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)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j)
(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))
(hconn : G.Connected)
(hcard : 2 ≤ Fintype.card V)
(hexact : ∀ γ ∈ (GraphMaps.secondCoboundaryMap G cycles).ker, ∃ (c : V → ZMod 2), (GraphMaps.coboundaryMap G) c = γ)
(hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range)
(hexp : DesiderataForGraphG.SufficientExpansion G)
(hL_logical : origCode.isLogicalOp GaugingMeasurementCorrectness.logicalOpV)
(L' : PauliOp (GaussFlux.ExtQubit G))
(hlog : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp L')
:
Corollary: if h(G) ≥ 1, then d ≥ d for each logical operator.*
Deformed Code Distance #
theorem
SpaceDistance.deformed_distance_ge_min_cheeger_d
{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)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j)
(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))
(hconn : G.Connected)
(hcard : 2 ≤ Fintype.card V)
(hexact : ∀ γ ∈ (GraphMaps.secondCoboundaryMap G cycles).ker, ∃ (c : V → ZMod 2), (GraphMaps.coboundaryMap G) c = γ)
(hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range)
(hL_logical : origCode.isLogicalOp GaugingMeasurementCorrectness.logicalOpV)
(hDeformedHasLogicals :
∃ (P : PauliOp (GaussFlux.ExtQubit G)),
(DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp P)
:
min (QEC1.cheegerConstant G) 1 * ↑origCode.distance ≤ ↑(DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).distance
Main theorem: deformed code distance bound. d* ≥ min(h(G), 1) · d.
theorem
SpaceDistance.deformed_distance_ge_d_sufficient_expansion
{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)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j)
(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))
(hconn : G.Connected)
(hcard : 2 ≤ Fintype.card V)
(hexact : ∀ γ ∈ (GraphMaps.secondCoboundaryMap G cycles).ker, ∃ (c : V → ZMod 2), (GraphMaps.coboundaryMap G) c = γ)
(hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range)
(hexp : DesiderataForGraphG.SufficientExpansion G)
(hL_logical : origCode.isLogicalOp GaugingMeasurementCorrectness.logicalOpV)
(hDeformedHasLogicals :
∃ (P : PauliOp (GaussFlux.ExtQubit G)),
(DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp P)
:
origCode.distance ≤ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).distance
Corollary: sufficient expansion preserves distance. If h(G) ≥ 1, then the deformed code distance d* ≥ d.