Theorem 2: Fault-Tolerant Gauging Distance #
Statement #
The spacetime fault-distance (Def_12) of the fault-tolerant gauging measurement procedure (Def_10) is d, the distance of the original [[n,k,d]] stabilizer code (Rem_3), provided that:
- The graph G has Cheeger constant h(G) ≥ 1 (Rem_4), and
- The number of deformed code rounds satisfies t_o - t_i ≥ d.
Formally: d_spacetime = d.
Main Results #
spacetimeFaultDistance_eq_d: The spacetime fault-distance equals dspacetimeFaultDistance_ge_d: Lower bound: d_spacetime ≥ dspacetimeFaultDistance_le_d: Upper bound: d_spacetime ≤ d (via space-fault witness)fullLogicalFault_weight_ge_d: Any full gauging logical fault has weight ≥ d
Proof Outline #
Lower bound: Any spacetime logical fault F decomposes as F = F_S · F_T · S (Lem 7). Case (a): If F_T flips σ (requires odd d), then |F_T| ≥ d by Lem 6, hence |F| ≥ d. Case (b): If F_S is a nontrivial space logical, then d ≤ d* ≤ |F_S.pauliErrorAt| ≤ |F| by Lem 3 with h(G) ≥ 1. When d is even, case (a) is vacuous (no syndrome-free pure-time fault can flip σ), so only case (b) applies.
Upper bound: A minimum-weight logical L₀ of the original code, placed as a space-fault at time t_i, gives a spacetime logical fault of weight d.
Part I: Space-Fault Witness Construction #
The paper's upper bound uses a minimum-weight logical operator L₀ of the original code, placed as a space-fault at time t_i. This construction builds a spacetime fault from a deformed code logical operator.
For each qubit q in P.support, we create a SpaceFault at qubit q, time t_i, with the appropriate X and Z components from P. The resulting spacetime fault has no time-faults (pure-space), so it is syndrome-free.
def
FaultTolerantGaugingDistance.mkSpaceFault
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
(t : ℕ)
(q : GaussFlux.ExtQubit G)
(hq : q ∈ P.support)
:
Build a SpaceFault from a qubit in the support of P.
Equations
Instances For
def
FaultTolerantGaugingDistance.spaceFaultsOfPauliOp
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
(t : ℕ)
:
Finset (SpaceFault (GaussFlux.ExtQubit G) ℕ)
The finset of space-faults corresponding to a Pauli operator at a given time.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
FaultTolerantGaugingDistance.mkSpaceFault_injective
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
(t : ℕ)
:
Function.Injective fun (x : { q : GaussFlux.ExtQubit G // q ∈ P.support }) => mkSpaceFault P t ↑x ⋯
The map from P.support to SpaceFault is injective (different qubits give different space faults).
theorem
FaultTolerantGaugingDistance.spaceFaultsOfPauliOp_card
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
(t : ℕ)
:
The space-fault finset has the same cardinality as P.support.
def
FaultTolerantGaugingDistance.spacetimeFaultOfDeformedLogical
{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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(P : PauliOp (GaussFlux.ExtQubit G))
(_hlog : (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
:
SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel
Given a logical operator P of the deformed code, placing it as a collection of space-faults at time t_i produces a spacetime fault.
Concretely: for each qubit q in P.support, we create a SpaceFault at qubit q, time t_i, with the appropriate X and Z components from P.
Equations
- FaultTolerantGaugingDistance.spacetimeFaultOfDeformedLogical proc P _hlog = { spaceFaults := FaultTolerantGaugingDistance.spaceFaultsOfPauliOp P proc.phase2Start, timeFaults := ∅ }
Instances For
theorem
FaultTolerantGaugingDistance.spacetimeFaultOfDeformedLogical_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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(P : PauliOp (GaussFlux.ExtQubit G))
(hlog : (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
:
The space-fault witness has the same weight as the Pauli operator.
theorem
FaultTolerantGaugingDistance.spacetimeFaultOfDeformedLogical_isPureSpace
{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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(P : PauliOp (GaussFlux.ExtQubit G))
(hlog : (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
:
(spacetimeFaultOfDeformedLogical proc P hlog).isPureSpace
The space-fault witness is pure-space (no time-faults).
theorem
FaultTolerantGaugingDistance.spacetimeFaultOfDeformedLogical_syndromeFree
{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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(P : PauliOp (GaussFlux.ExtQubit G))
(hlog : (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
:
SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex (spacetimeFaultOfDeformedLogical proc P hlog)
The space-fault witness is syndrome-free: it has no time-faults, so every detector checks against ∅ which is never violated.
theorem
FaultTolerantGaugingDistance.spaceFaultsOfPauliOp_time
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
(t : ℕ)
(f : SpaceFault (GaussFlux.ExtQubit G) ℕ)
(hf : f ∈ spaceFaultsOfPauliOp P t)
:
Helper: a space fault in spaceFaultsOfPauliOp has the correct time.
theorem
FaultTolerantGaugingDistance.spaceFaultsOfPauliOp_qubit_mem
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
(t : ℕ)
(f : SpaceFault (GaussFlux.ExtQubit G) ℕ)
(hf : f ∈ spaceFaultsOfPauliOp P t)
:
Helper: a space fault in spaceFaultsOfPauliOp has qubit in P.support.
theorem
FaultTolerantGaugingDistance.spaceFaultsOfPauliOp_mem
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
(t : ℕ)
(q : GaussFlux.ExtQubit G)
(hq : q ∈ P.support)
:
Helper: for each qubit in P.support, there exists a space fault.
theorem
FaultTolerantGaugingDistance.spaceFaultsOfPauliOp_xComponent
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
(t : ℕ)
(f : SpaceFault (GaussFlux.ExtQubit G) ℕ)
(hf : f ∈ spaceFaultsOfPauliOp P t)
:
Helper: each space fault in spaceFaultsOfPauliOp has xComponent = P.xVec f.qubit
theorem
FaultTolerantGaugingDistance.spaceFaultsOfPauliOp_zComponent
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
(t : ℕ)
(f : SpaceFault (GaussFlux.ExtQubit G) ℕ)
(hf : f ∈ spaceFaultsOfPauliOp P t)
:
Helper: each space fault in spaceFaultsOfPauliOp has zComponent = P.zVec f.qubit
theorem
FaultTolerantGaugingDistance.spaceFaultsOfPauliOp_unique
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(P : PauliOp (GaussFlux.ExtQubit G))
(t : ℕ)
(f₁ f₂ : SpaceFault (GaussFlux.ExtQubit G) ℕ)
(hf₁ : f₁ ∈ spaceFaultsOfPauliOp P t)
(hf₂ : f₂ ∈ spaceFaultsOfPauliOp P t)
(hq : f₁.qubit = f₂.qubit)
:
Helper: at most one space fault per qubit in spaceFaultsOfPauliOp.
theorem
FaultTolerantGaugingDistance.spacetimeFaultOfDeformedLogical_pauliErrorAt
{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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(P : PauliOp (GaussFlux.ExtQubit G))
(hlog : (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
:
The Pauli error at t_i of the space-fault witness equals P.
theorem
FaultTolerantGaugingDistance.spaceFaultWitness_isFullLogicalFault
{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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(P : PauliOp (GaussFlux.ExtQubit G))
(hlog : (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
:
SpaceTimeDecoupling.IsFullGaugingLogicalFault proc (spacetimeFaultOfDeformedLogical proc P hlog)
The space-fault witness is a full gauging logical fault: it is syndrome-free and NOT outcome-preserving. The sign is preserved (pure-space → gaussSignFlip = 0), but the Pauli error at t_i is P, which is NOT in the stabilizer group (since P is a logical).
Part II: Upper Bound d_spacetime ≤ d #
A deformed code logical of minimum weight gives a space-fault witness. By Rem 13 (d* = d when h(G) ≥ 1), the deformed code has a logical of weight d.
theorem
FaultTolerantGaugingDistance.spacetimeFaultDistance_le_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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = 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)), (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
(hd_eq : origCode.distance = proc.d)
(P : PauliOp V)
(hPlog : origCode.isLogicalOp P)
(hPpureX : P.zVec = 0)
(hPweight : P.weight = origCode.distance)
(hnotDeformedStab :
OptimalCheegerConstant.liftToExtended G P ∉ (SpaceTimeDecoupling.theDeformedCode proc).stabilizerGroup)
:
Upper bound: d_spacetime ≤ d (via the space-fault witness).
Place a minimum-weight deformed code logical at time t_i as a collection of space-faults. This has weight d* ≤ d and is a full gauging logical fault.
Part III: Lower Bound d_spacetime ≥ d #
Any full logical fault has weight ≥ d. We use the decomposition from Lem 7:
- Case (a): F_T flips σ → |F| ≥ d via time component weight bound (requires odd d)
- Case (b): F_S is a nontrivial deformed code logical → d ≤ d* ≤ |F.pauliErrorAt| ≤ |F|
When d is even, case (a) is vacuous: no syndrome-free pure-time fault can flip σ (each vertex has 0 or d faults by all-or-none, so total count is k·d ≡ 0 mod 2).
theorem
FaultTolerantGaugingDistance.even_d_no_time_sign_flip
{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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(F_T : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(_hpT : F_T.isPureTime)
(hfreeT : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F_T)
(heven : Even proc.d)
:
When d is even, no syndrome-free pure-time fault can flip the gauging sign σ. This is because the all-or-none property (from Lem 6's detector structure) forces each vertex's A_v fault count to be 0 or d. When d is even, the total gaussSignFlip = Σ (0 or d) = k·d ≡ 0 (mod 2) for all k.
theorem
FaultTolerantGaugingDistance.inCentralizer_mul_stabilizerGroup
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(code : StabilizerCode (GaussFlux.ExtQubit G))
(P s : PauliOp (GaussFlux.ExtQubit G))
(hP : code.inCentralizer P)
(hs : s ∈ code.stabilizerGroup)
:
code.inCentralizer (P * s)
Helper: the product of a centralizer element and a stabilizer group element is in the centralizer.
theorem
FaultTolerantGaugingDistance.distance_le_weight_of_isLogicalOp
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
(code : StabilizerCode (GaussFlux.ExtQubit G))
(P : PauliOp (GaussFlux.ExtQubit G))
(hlog : code.isLogicalOp P)
:
Helper: distance ≤ weight of any logical operator (directly from sInf).
theorem
FaultTolerantGaugingDistance.pauliErrorAt_support_subset_image
{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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(t : ℕ)
:
Helper: the support of pauliErrorAt t is a subset of the qubit image of spaceFaultsAt t.
theorem
FaultTolerantGaugingDistance.pauliErrorAt_weight_le_spaceWeight
{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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(t : ℕ)
:
Helper: the weight of the Pauli error at a time is ≤ the total space weight. Each qubit in the support of pauliErrorAt t corresponds to at least one space-fault at time t, and space-faults at time t are a subset of all space-faults.
theorem
FaultTolerantGaugingDistance.fullLogicalFault_weight_ge_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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = 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)), (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
(hd_eq : origCode.distance = proc.d)
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(hlog : SpaceTimeDecoupling.IsFullGaugingLogicalFault proc F)
:
Any full gauging logical fault has weight ≥ d.
This is the core content of the lower bound. We use the space-time decoupling (Lem 7) to decompose F into space and time components, then bound each case using Lem 3 (space distance) and Lem 6 (time distance).
Part IV: Lower Bound via sInf #
theorem
FaultTolerantGaugingDistance.spacetimeFaultDistance_ge_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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = 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)), (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
(hd_eq : origCode.distance = proc.d)
(P : PauliOp V)
(hPlog : origCode.isLogicalOp P)
(hPpureX : P.zVec = 0)
(_hPweight : P.weight = origCode.distance)
(hnotDeformedStab :
OptimalCheegerConstant.liftToExtended G P ∉ (SpaceTimeDecoupling.theDeformedCode proc).stabilizerGroup)
:
Lower bound: d_spacetime ≥ d.
Part V: Main Theorem #
theorem
FaultTolerantGaugingDistance.spacetimeFaultDistance_eq_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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = 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)), (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
(hd_eq : origCode.distance = proc.d)
(P : PauliOp V)
(hPlog : origCode.isLogicalOp P)
(hPpureX : P.zVec = 0)
(hPweight : P.weight = origCode.distance)
(hnotDeformedStab :
OptimalCheegerConstant.liftToExtended G P ∉ (SpaceTimeDecoupling.theDeformedCode proc).stabilizerGroup)
:
Theorem 2 (Fault-Tolerant Gauging Distance): The spacetime fault-distance of the fault-tolerant gauging measurement procedure equals d, the distance of the original code, when h(G) ≥ 1.
No parity assumption on d is needed: when d is even, the lower bound still holds because case (a) (time-logical) is vacuous, and case (b) (space-logical) provides |F| ≥ d* ≥ d.
Corollaries #
theorem
FaultTolerantGaugingDistance.spacetimeFaultDistance_pos
{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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = 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)), (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
(hd_eq : origCode.distance = proc.d)
(P : PauliOp V)
(hPlog : origCode.isLogicalOp P)
(hPpureX : P.zVec = 0)
(hPweight : P.weight = origCode.distance)
(hnotDeformedStab :
OptimalCheegerConstant.liftToExtended G P ∉ (SpaceTimeDecoupling.theDeformedCode proc).stabilizerGroup)
:
The spacetime fault-distance is positive.
theorem
FaultTolerantGaugingDistance.weight_lt_d_is_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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = 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)), (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
(hd_eq : origCode.distance = proc.d)
(P : PauliOp V)
(hPlog : origCode.isLogicalOp P)
(hPpureX : P.zVec = 0)
(hPweight : P.weight = origCode.distance)
(hnotDeformedStab :
OptimalCheegerConstant.liftToExtended G P ∉ (SpaceTimeDecoupling.theDeformedCode proc).stabilizerGroup)
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F)
(hw : F.weight < proc.d)
:
Any full gauging fault of weight < d is a gauging stabilizer.
theorem
FaultTolerantGaugingDistance.spacetimeFaultDistance_eq_phase2_duration
{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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = 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)), (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
(hd_eq : origCode.distance = proc.d)
(P : PauliOp V)
(hPlog : origCode.isLogicalOp P)
(hPpureX : P.zVec = 0)
(hPweight : P.weight = origCode.distance)
(hnotDeformedStab :
OptimalCheegerConstant.liftToExtended G P ∉ (SpaceTimeDecoupling.theDeformedCode proc).stabilizerGroup)
:
SpacetimeFaultDistance.gaugingSpacetimeFaultDistance proc proc.detectorOfIndex
(SpaceTimeDecoupling.FullOutcomePreserving proc) = proc.phase3Start - proc.phase2Start
The spacetime fault-distance equals the Phase 2 duration.
theorem
FaultTolerantGaugingDistance.deformed_distance_ge_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}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(origCode : StabilizerCode V)
(hJ : origCode.I = J)
(hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = 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)), (SpaceTimeDecoupling.theDeformedCode proc).isLogicalOp P)
:
origCode.distance ≤ (DeformedCodeChecks.deformedStabilizerCode G cycles checks proc.deformedData ⋯ ⋯).distance
Space code distance d* ≥ d when h(G) ≥ 1.