Lemma 6: Time Fault-Distance #
Statement #
The fault-distance for pure measurement and initialization errors (time-faults only, no space-faults) in the fault-tolerant gauging measurement procedure (Def 10) is $t_o - t_i = d$, the number of rounds in the deformed code phase.
Main Results #
timeFaultDistance: The time fault-distance (minimum weight of pure-time logical fault)gaussStringFault: The A_v measurement string of weight d (upper bound witness)gaussStringFault_weight_eq_d: The A_v string has weight dgaussStringFault_syndromeFree: The A_v string is syndrome-freetimeFaultDistance_le_d: d_time ≤ d (upper bound)timeFaultDistance_ge_d: d_time ≥ d (lower bound)timeFaultDistance_eq_d: d_time = d (main theorem)
Proof Outline #
Upper bound: A string of A_v measurement faults for a single vertex v at all d rounds of Phase 2 has weight d, is syndrome-free (repeated detectors see two flips that cancel), and flips σ (since d is odd).
Lower bound: Any pure time-fault that changes the logical outcome must flip σ. By the all-or-none constraint from repeated Gauss detectors, each vertex's A_v faults span either all d rounds or none. A sign flip requires an odd number of full A_v strings, each contributing d to weight.
Part I: Pure-Time Logical Fault Definition #
def
TimeFaultDistance.IsPureTimeFault
{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)
:
A pure-time spacetime fault: no space-faults, only time-faults.
Equations
- TimeFaultDistance.IsPureTimeFault proc F = F.isPureTime
Instances For
def
TimeFaultDistance.IsPureTimeLogicalFault
{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)
(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)
:
A pure-time gauging logical fault: pure-time AND a gauging logical fault.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
TimeFaultDistance.pureTimeLogicalFaultWeights
{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)
(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 pure-time gauging logical faults.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
TimeFaultDistance.timeFaultDistance
{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)
(detectors : FaultTolerantGaugingProcedure.DetectorIndex V C J (↑G.edgeSet) proc.d → Detector proc.MeasLabel)
(outcomePreserving : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel → Prop)
:
The time fault-distance: minimum weight of a pure-time gauging logical fault.
Equations
- TimeFaultDistance.timeFaultDistance proc detectors outcomePreserving = sInf (TimeFaultDistance.pureTimeLogicalFaultWeights proc detectors outcomePreserving)
Instances For
Part II: The A_v Measurement String (Upper Bound Witness) #
def
TimeFaultDistance.gaussMeasFaults
{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)
(v : V)
:
The A_v measurement string: time-faults on A_v at all d rounds of Phase 2.
Equations
- TimeFaultDistance.gaussMeasFaults proc v = Finset.image (fun (r : Fin proc.d) => { measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r) }) Finset.univ
Instances For
def
TimeFaultDistance.gaussStringFault
{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)
(v : V)
:
SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel
The A_v measurement string as a spacetime fault.
Equations
- TimeFaultDistance.gaussStringFault proc v = { spaceFaults := ∅, timeFaults := TimeFaultDistance.gaussMeasFaults proc v }
Instances For
theorem
TimeFaultDistance.gaussStringFault_isPureTime
{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)
(v : V)
:
(gaussStringFault proc v).isPureTime
The A_v string is pure-time.
theorem
TimeFaultDistance.gaussMeasFaults_injective
{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)
(v : V)
:
Function.Injective fun (r : Fin proc.d) =>
{ measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r) }
The image map for A_v faults is injective.
theorem
TimeFaultDistance.gaussMeasFaults_card
{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)
(v : V)
:
The A_v string has exactly d time-faults.
theorem
TimeFaultDistance.gaussStringFault_weight_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)
(v : V)
:
The A_v string has weight d.
Membership lemmas #
theorem
TimeFaultDistance.mem_gaussMeasFaults
{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)
(v : V)
(tf : TimeFault proc.MeasLabel)
:
tf ∈ gaussMeasFaults proc v ↔ ∃ (r : Fin proc.d), tf = { measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r) }
A time-fault is in the A_v string iff it's a Gauss A_v measurement at some round.
theorem
TimeFaultDistance.gaussStringFault_timeFaults_eq
{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)
(v : V)
:
theorem
TimeFaultDistance.gaussStringFault_mem_gauss
{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)
(v : V)
(r : Fin proc.d)
:
{ measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r) } ∈ (gaussStringFault proc v).timeFaults
A Gauss A_v measurement at round r is in the A_v string.
theorem
TimeFaultDistance.gaussStringFault_no_other_gauss
{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)
(v w : V)
(r : Fin proc.d)
(hvw : v ≠ w)
:
{ measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw w r) } ∉
(gaussStringFault proc v).timeFaults
A Gauss A_w measurement (w ≠ v) is not in the A_v string.
The A_v string flips the gauging sign #
theorem
TimeFaultDistance.gaussStringFault_signFlip
{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)
(v : V)
:
The gaussSignFlip for the A_v string equals d (mod 2).
theorem
TimeFaultDistance.gaussStringFault_flipsSign_of_odd
{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)
(v : V)
(hodd : Odd proc.d)
:
SpacetimeLogicalFault.FlipsGaugingSign proc (gaussStringFault proc v)
When d is odd, the A_v string flips the gauging sign.
Syndrome-freeness of the A_v string #
theorem
TimeFaultDistance.gaussStringFault_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)
(v : V)
:
SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex (gaussStringFault proc v)
The A_v string is syndrome-free with respect to all detectors from Lemma 4.
Part III: Upper Bound #
theorem
TimeFaultDistance.gaussStringFault_isLogicalFault
{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)
(v : V)
(hodd : Odd proc.d)
:
SpacetimeLogicalFault.IsGaugingLogicalFault proc proc.detectorOfIndex (SpacetimeLogicalFault.PreservesGaugingSign proc)
(gaussStringFault proc v)
The A_v string is a gauging logical fault when d is odd.
theorem
TimeFaultDistance.timeFaultDistance_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)
(v : V)
(hodd : Odd proc.d)
:
timeFaultDistance proc proc.detectorOfIndex (SpacetimeLogicalFault.PreservesGaugingSign proc) ≤ proc.d
Upper bound: timeFaultDistance ≤ d when d is odd and V is nonempty.
Part IV: Lower Bound #
theorem
TimeFaultDistance.pureTime_weight_eq_card
{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)
(hpure : F.isPureTime)
:
For a pure-time fault, weight = timeFaults.card.
noncomputable def
TimeFaultDistance.gaussFaultCount
{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)
(v : V)
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
:
Gauss fault count for vertex v: number of A_v measurement faults across all rounds.
Equations
- TimeFaultDistance.gaussFaultCount proc v F = {r : Fin proc.d | { measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r) } ∈ F.timeFaults}.card
Instances For
theorem
TimeFaultDistance.gaussSignFlip_eq_sum_parities
{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)
:
The gaussSignFlip equals the sum of Gauss fault count parities.
Consecutive round constraint #
theorem
TimeFaultDistance.syndromeFree_gauss_consecutive
{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)
(v : V)
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F)
(r r' : Fin proc.d)
(hr : ↑r + 1 = ↑r')
:
{ measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r) } ∈ F.timeFaults ↔ { measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r') } ∈ F.timeFaults
For a syndrome-free fault, consecutive Gauss A_v rounds have the same fault status.
theorem
TimeFaultDistance.syndromeFree_gauss_all_or_none
{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)
(v : V)
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F)
(r r' : Fin proc.d)
:
{ measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r) } ∈ F.timeFaults ↔ { measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r') } ∈ F.timeFaults
All-or-none: for a syndrome-free fault, either all rounds of A_v are faulted or none are.
theorem
TimeFaultDistance.gaussFaultCount_zero_or_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)
(v : V)
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F)
:
The Gauss fault count for each vertex is either 0 or d.
theorem
TimeFaultDistance.gaussFaultParity_zero_or_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)
(v : V)
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F)
:
Gauss fault parity for each vertex is either 0 or d (mod 2).
theorem
TimeFaultDistance.sign_flip_implies_odd_full_strings
{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)
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F)
(hflip : SpacetimeLogicalFault.FlipsGaugingSign proc F)
(hodd : Odd proc.d)
:
Odd {v : V | gaussFaultCount proc v F = proc.d}.card
For a syndrome-free fault that flips the sign with odd d: odd number of full A_v strings.
theorem
TimeFaultDistance.pureTime_weight_ge_gauss_sum
{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)
(hpure : F.isPureTime)
:
The total Gauss fault count ≤ weight for a pure-time fault.
theorem
TimeFaultDistance.pureTime_weight_ge_d_of_full_string
{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)
(hpure : F.isPureTime)
(v : V)
(hv : gaussFaultCount proc v F = proc.d)
:
A pure-time fault with a full A_v string has weight ≥ d.
theorem
TimeFaultDistance.pureTime_logicalFault_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)
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(hpure : IsPureTimeFault proc F)
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F)
(hflip : SpacetimeLogicalFault.FlipsGaugingSign proc F)
(hodd : Odd proc.d)
:
Lower bound: Any pure-time logical fault has weight ≥ d (when d is odd).
Part V: Main Theorem #
theorem
TimeFaultDistance.timeFaultDistance_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)
(hodd : Odd proc.d)
(hV : Nonempty V)
:
proc.d ≤ timeFaultDistance proc proc.detectorOfIndex (SpacetimeLogicalFault.PreservesGaugingSign proc)
Lower bound for time fault-distance: timeFaultDistance ≥ d.
theorem
TimeFaultDistance.timeFaultDistance_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)
(v : V)
(hodd : Odd proc.d)
(hV : Nonempty V)
:
timeFaultDistance proc proc.detectorOfIndex (SpacetimeLogicalFault.PreservesGaugingSign proc) = proc.d
Lemma 6 (Time Fault-Distance): timeFaultDistance = d.
Part V-b: Justification of the Outcome Predicate (Paper Step 5, second bullet) #
The paper's proof (Step 5) shows that for pure-time faults, PreservesGaugingSign is the
correct outcome predicate. Specifically: every syndrome-free pure-time fault that does NOT
flip σ decomposes into the spacetime stabilizer generators from Lemma 5 (B_p measurement
pairs, s̃_j measurement pairs, and boundary initialization/readout faults). Since these
generators preserve the gauging outcome by listedGenerator_isGaugingStabilizer (Lem 5),
they are trivial logical faults.
This section proves this equivalence, connecting our use of PreservesGaugingSign proc
to the paper's full argument.
theorem
TimeFaultDistance.pureTime_preservesSign_decomposes_into_generators
{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)
(_hpure : IsPureTimeFault proc F)
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F)
(hpres : SpacetimeLogicalFault.PreservesGaugingSign proc F)
:
∃ (gens : List (SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)),
(∀ g ∈ gens, SpacetimeStabilizers.IsListedGenerator proc g) ∧ F = List.foldl SpacetimeFault.compose SpacetimeFault.empty gens
Every syndrome-free pure-time fault that preserves the Gauss sign is a gauging stabilizer that decomposes into Lemma 5's listed generators. This is the mathematical content of Step 5 (second bullet) of the paper's proof: non-σ-flipping syndrome-free pure-time faults are products of spacetime stabilizers (B_p/s̃_j measurement pairs and boundary faults), hence trivial.
theorem
TimeFaultDistance.pureTime_syndromeFree_logical_or_stabilizer_generators
{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)
(hpure : IsPureTimeFault proc F)
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F)
:
SpacetimeLogicalFault.FlipsGaugingSign proc F ∨ SpacetimeLogicalFault.PreservesGaugingSign proc F ∧ ∃ (gens : List (SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)),
(∀ g ∈ gens, SpacetimeStabilizers.IsListedGenerator proc g) ∧ F = List.foldl SpacetimeFault.compose SpacetimeFault.empty gens
For syndrome-free pure-time faults, the dichotomy from Def 11 specializes to:
either the fault flips σ (logical fault), or it decomposes into Lemma 5's
stabilizer generators (trivial fault). This justifies using PreservesGaugingSign
as the outcomePreserving predicate in the time fault-distance definition.
Part VI: Corollaries #
theorem
TimeFaultDistance.pureTime_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)
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(hpure : IsPureTimeFault proc F)
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F)
(hw : F.weight < proc.d)
(hodd : Odd proc.d)
:
Any pure-time fault of weight < d is a gauging stabilizer (when d is odd).
theorem
TimeFaultDistance.gaussFaultCount_dichotomy
{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)
(v : V)
(F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel)
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F)
:
The Gauss fault count dichotomy (rephrased).
theorem
TimeFaultDistance.timeFaultDistance_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)
(v : V)
(hodd : Odd proc.d)
(hV : Nonempty V)
:
timeFaultDistance proc proc.detectorOfIndex (SpacetimeLogicalFault.PreservesGaugingSign proc) = proc.phase3Start - proc.phase2Start
The time fault-distance equals the Phase 2 duration t_o - t_i.
theorem
TimeFaultDistance.minimum_weight_is_single_string
{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)
(hpure : IsPureTimeFault proc F)
(hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F)
(hflip : SpacetimeLogicalFault.FlipsGaugingSign proc F)
(hw : F.weight = proc.d)
(hodd : Odd proc.d)
:
Minimum-weight pure-time logical faults have exactly one full A_v string.