Definition 12: Spacetime Fault-Distance #
Statement #
The spacetime fault-distance of the fault-tolerant gauging measurement procedure (Def 10) is the minimum weight of a spacetime logical fault (Def 11).
The weight |F| of a spacetime fault F is the total number of elementary fault events:
- Each single-qubit Pauli error (space-fault) counts as weight 1
- Each measurement error (time-fault) counts as weight 1
- Each initialization error (time-fault) counts as weight 1
Formally: d_spacetime = min { |F| : F is a spacetime logical fault }
Returns 0 if no spacetime logical faults exist.
Main Results #
spacetimeFaultDistance: The spacetime fault-distance d_spacetimespacetimeFaultDistance_le_of_logicalFault: d_spacetime ≤ |F| for any logical fault FspacetimeFaultDistance_pos: d_spacetime > 0 when logical faults exist and empty is a stabilizer
Corollaries #
spacetimeFaultDistance_eq_zero_of_no_logicalFaults: d_spacetime = 0 if no logical faultsnot_logicalFault_of_weight_lt: Fault of weight < d_spacetime cannot be logicalsyndromeFree_weight_lt_is_stabilizer: Syndrome-free fault of weight < d_spacetime is stabilizer
Generic Spacetime Fault-Distance #
Defined for an arbitrary collection of detectors and an outcome-preserving predicate.
This follows the same sInf pattern as StabilizerCode.distance (Rem_3).
def
SpacetimeFaultDistance.logicalFaultWeights
{Q : Type u_1}
{T : Type u_2}
{I : Type u_3}
[Fintype I]
[DecidableEq I]
{M : Type u_4}
[DecidableEq M]
[DecidableEq (TimeFault M)]
(detectors : I → Detector M)
(outcomePreserving : SpacetimeFault Q T M → Prop)
:
The set of weights of spacetime logical faults.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
SpacetimeFaultDistance.spacetimeFaultDistance
{Q : Type u_1}
{T : Type u_2}
{I : Type u_3}
[Fintype I]
[DecidableEq I]
{M : Type u_4}
[DecidableEq M]
[DecidableEq (TimeFault M)]
(detectors : I → Detector M)
(outcomePreserving : SpacetimeFault Q T M → Prop)
:
The spacetime fault-distance: minimum weight of a spacetime logical fault. Returns 0 if no spacetime logical faults exist.
Equations
- SpacetimeFaultDistance.spacetimeFaultDistance detectors outcomePreserving = sInf (SpacetimeFaultDistance.logicalFaultWeights detectors outcomePreserving)
Instances For
Basic Properties #
theorem
SpacetimeFaultDistance.spacetimeFaultDistance_le_of_logicalFault
{Q : Type u_1}
{T : Type u_2}
{I : Type u_3}
[Fintype I]
[DecidableEq I]
{M : Type u_4}
[DecidableEq M]
[DecidableEq (TimeFault M)]
{detectors : I → Detector M}
{outcomePreserving : SpacetimeFault Q T M → Prop}
{F : SpacetimeFault Q T M}
(hlog : SpacetimeLogicalFault.IsSpacetimeLogicalFault detectors outcomePreserving F)
:
d_spacetime ≤ |F| for any spacetime logical fault F.
theorem
SpacetimeFaultDistance.spacetimeFaultDistance_eq_zero_of_no_logicalFaults
{Q : Type u_1}
{T : Type u_2}
{I : Type u_3}
[Fintype I]
[DecidableEq I]
{M : Type u_4}
[DecidableEq M]
[DecidableEq (TimeFault M)]
(detectors : I → Detector M)
(outcomePreserving : SpacetimeFault Q T M → Prop)
(hno : ∀ (F : SpacetimeFault Q T M), ¬SpacetimeLogicalFault.IsSpacetimeLogicalFault detectors outcomePreserving F)
:
If no spacetime logical faults exist, d_spacetime = 0.
theorem
SpacetimeFaultDistance.spacetimeFaultDistance_pos
{Q : Type u_1}
{T : Type u_2}
{I : Type u_3}
[Fintype I]
[DecidableEq I]
{M : Type u_4}
[DecidableEq M]
[DecidableEq (TimeFault M)]
[DecidableEq Q]
[DecidableEq T]
[DecidableEq (SpaceFault Q T)]
{detectors : I → Detector M}
{outcomePreserving : SpacetimeFault Q T M → Prop}
(hempty : outcomePreserving SpacetimeFault.empty)
(hexists : ∃ (F : SpacetimeFault Q T M), SpacetimeLogicalFault.IsSpacetimeLogicalFault detectors outcomePreserving F)
:
d_spacetime > 0 when logical faults exist and the empty fault is outcome-preserving.
Characterization Lemmas #
theorem
SpacetimeFaultDistance.not_logicalFault_of_weight_lt
{Q : Type u_1}
{T : Type u_2}
{I : Type u_3}
[Fintype I]
[DecidableEq I]
{M : Type u_4}
[DecidableEq M]
[DecidableEq (TimeFault M)]
{detectors : I → Detector M}
{outcomePreserving : SpacetimeFault Q T M → Prop}
{F : SpacetimeFault Q T M}
(hw : F.weight < spacetimeFaultDistance detectors outcomePreserving)
:
¬SpacetimeLogicalFault.IsSpacetimeLogicalFault detectors outcomePreserving F
A fault of weight < d_spacetime cannot be a logical fault.
theorem
SpacetimeFaultDistance.syndromeFree_weight_lt_is_stabilizer
{Q : Type u_1}
{T : Type u_2}
{I : Type u_3}
[Fintype I]
[DecidableEq I]
{M : Type u_4}
[DecidableEq M]
[DecidableEq (TimeFault M)]
{detectors : I → Detector M}
{outcomePreserving : SpacetimeFault Q T M → Prop}
{F : SpacetimeFault Q T M}
(hfree : SpacetimeLogicalFault.IsSyndromeFree detectors F)
(hw : F.weight < spacetimeFaultDistance detectors outcomePreserving)
:
SpacetimeLogicalFault.IsSpacetimeStabilizer detectors outcomePreserving F
Any syndrome-free fault of weight < d_spacetime is a spacetime stabilizer.
theorem
SpacetimeFaultDistance.spacetimeFaultDistance_le_space_plus_time
{Q : Type u_1}
{T : Type u_2}
{I : Type u_3}
[Fintype I]
[DecidableEq I]
{M : Type u_4}
[DecidableEq M]
[DecidableEq (TimeFault M)]
[DecidableEq Q]
[DecidableEq T]
[DecidableEq (SpaceFault Q T)]
{detectors : I → Detector M}
{outcomePreserving : SpacetimeFault Q T M → Prop}
{F : SpacetimeFault Q T M}
(hlog : SpacetimeLogicalFault.IsSpacetimeLogicalFault detectors outcomePreserving F)
:
d_spacetime ≤ spaceWeight + timeWeight for any logical fault.
Instantiation for the Gauging Procedure #
The spacetime fault-distance of the fault-tolerant gauging procedure (Def 10) uses the gauging-specific logical fault definition (IsGaugingLogicalFault from Def 11) and the detectors from Lemma 4.
def
SpacetimeFaultDistance.gaugingLogicalFaultWeights
{V : Type u_5}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_6}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_7}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(detectors : FaultTolerantGaugingProcedure.DetectorIndex V C J (↑G.edgeSet) proc.d → Detector proc.MeasLabel)
(outcomePreserving : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel → Prop)
:
The set of weights of gauging logical faults.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
SpacetimeFaultDistance.gaugingSpacetimeFaultDistance
{V : Type u_5}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_6}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_7}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(detectors : FaultTolerantGaugingProcedure.DetectorIndex V C J (↑G.edgeSet) proc.d → Detector proc.MeasLabel)
(outcomePreserving : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel → Prop)
:
The spacetime fault-distance of the gauging procedure: minimum weight of a gauging logical fault.
Equations
- SpacetimeFaultDistance.gaugingSpacetimeFaultDistance proc detectors outcomePreserving = sInf (SpacetimeFaultDistance.gaugingLogicalFaultWeights proc detectors outcomePreserving)
Instances For
theorem
SpacetimeFaultDistance.gaugingSpacetimeFaultDistance_le
{V : Type u_5}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_6}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_7}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
(proc : FaultTolerantGaugingProcedure G cycles checks)
{detectors : FaultTolerantGaugingProcedure.DetectorIndex V C J (↑G.edgeSet) proc.d → Detector proc.MeasLabel}
{outcomePreserving : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel → Prop}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(hlog : SpacetimeLogicalFault.IsGaugingLogicalFault proc detectors outcomePreserving F)
:
d_spacetime ≤ |F| for any gauging logical fault F.
theorem
SpacetimeFaultDistance.gaugingSpacetimeFaultDistance_eq_zero_of_no_faults
{V : Type u_5}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_6}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_7}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
(proc : FaultTolerantGaugingProcedure G cycles checks)
(detectors : FaultTolerantGaugingProcedure.DetectorIndex V C J (↑G.edgeSet) proc.d → Detector proc.MeasLabel)
(outcomePreserving : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel → Prop)
(hno :
∀ (F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel),
¬SpacetimeLogicalFault.IsGaugingLogicalFault proc detectors outcomePreserving F)
:
If no gauging logical faults exist, d_spacetime = 0.
theorem
SpacetimeFaultDistance.gaugingSpacetimeFaultDistance_pos
{V : Type u_5}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_6}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_7}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
(proc : FaultTolerantGaugingProcedure G cycles checks)
{detectors : FaultTolerantGaugingProcedure.DetectorIndex V C J (↑G.edgeSet) proc.d → Detector proc.MeasLabel}
{outcomePreserving : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel → Prop}
(hempty : outcomePreserving SpacetimeFault.empty)
(hexists :
∃ (F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel),
SpacetimeLogicalFault.IsGaugingLogicalFault proc detectors outcomePreserving F)
:
d_spacetime > 0 when gauging logical faults exist and empty is outcome-preserving.
theorem
SpacetimeFaultDistance.not_gaugingLogicalFault_of_weight_lt
{V : Type u_5}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_6}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_7}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
(proc : FaultTolerantGaugingProcedure G cycles checks)
{detectors : FaultTolerantGaugingProcedure.DetectorIndex V C J (↑G.edgeSet) proc.d → Detector proc.MeasLabel}
{outcomePreserving : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel → Prop}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(hw : F.weight < gaugingSpacetimeFaultDistance proc detectors outcomePreserving)
:
¬SpacetimeLogicalFault.IsGaugingLogicalFault proc detectors outcomePreserving F
Any gauging fault of weight < d_spacetime cannot be a gauging logical fault.
theorem
SpacetimeFaultDistance.syndromeFree_gauging_weight_lt_is_stabilizer
{V : Type u_5}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_6}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_7}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
(proc : FaultTolerantGaugingProcedure G cycles checks)
{detectors : FaultTolerantGaugingProcedure.DetectorIndex V C J (↑G.edgeSet) proc.d → Detector proc.MeasLabel}
{outcomePreserving : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel → Prop}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc detectors F)
(hw : F.weight < gaugingSpacetimeFaultDistance proc detectors outcomePreserving)
:
SpacetimeLogicalFault.IsGaugingStabilizer proc detectors outcomePreserving F
Any syndrome-free gauging fault of weight < d_spacetime is a gauging stabilizer.
theorem
SpacetimeFaultDistance.gaugingSpacetimeFaultDistance_le_weight
{V : Type u_5}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_6}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_7}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
(proc : FaultTolerantGaugingProcedure G cycles checks)
{detectors : FaultTolerantGaugingProcedure.DetectorIndex V C J (↑G.edgeSet) proc.d → Detector proc.MeasLabel}
{outcomePreserving : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel → Prop}
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(hlog : SpacetimeLogicalFault.IsGaugingLogicalFault proc detectors outcomePreserving F)
:
d_spacetime ≤ |F| for any specific gauging logical fault (explicit weight bound).
theorem
SpacetimeFaultDistance.gaugingSpacetimeFaultDistance_le_space_plus_time
{V : Type u_5}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_6}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_7}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
(proc : FaultTolerantGaugingProcedure G cycles checks)
{detectors : FaultTolerantGaugingProcedure.DetectorIndex V C J (↑G.edgeSet) proc.d → Detector proc.MeasLabel}
{outcomePreserving : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel → Prop}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(hlog : SpacetimeLogicalFault.IsGaugingLogicalFault proc detectors outcomePreserving F)
:
d_spacetime ≤ spaceWeight + timeWeight for any gauging logical fault.