Definition 11: Spacetime Logical Fault

Statement

A spacetime logical fault is a collection of space-faults and time-faults (Def 7) that:

1. Does not violate any detector (i.e., the syndrome (Def 9) is empty), AND
2. Changes the outcome of the fault-tolerant gauging measurement procedure (Def 10).

A spacetime stabilizer is a collection of space-faults and time-faults that:

1. Does not violate any detector, AND
2. Does NOT change the outcome of the procedure.

Every syndrome-free fault collection is either a spacetime logical fault or a spacetime stabilizer.

Main Results

• IsSyndromeFree: A fault has empty syndrome (no detectors violated)
• IsSpacetimeLogicalFault: Syndrome-free AND changes the measurement outcome
• IsSpacetimeStabilizer: Syndrome-free AND does NOT change the measurement outcome
• syndromeFree_dichotomy: Every syndrome-free fault is either logical or stabilizer

Corollaries

• logicalFault_not_stabilizer: The dichotomy is exclusive
• empty_isSpacetimeStabilizer: The empty fault is a stabilizer
• IsSpacetimeLogicalFault.weight_pos: A logical fault has positive weight
• syndromeFree_logicalFault_iff_not_stabilizer: Characterization via negation

Syndrome-Free Faults

We work with an arbitrary collection of detectors indexed by a fintype I. In the context of the fault-tolerant gauging procedure (Def 10), I is instantiated with DetectorIndex V C J G.edgeSet d from Lemma 4.

def SpacetimeLogicalFault.IsSyndromeFree {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} (detectors : I → Detector M) (F : SpacetimeFault Q T M) : Prop

A spacetime fault is syndrome-free if the syndrome is empty, i.e., no detector is violated. This is the first condition for both spacetime logical faults and spacetime stabilizers.

Equations

• SpacetimeLogicalFault.IsSyndromeFree detectors F = (syndromeFault detectors F = ∅)

theorem SpacetimeLogicalFault.isSyndromeFree_iff {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} (detectors : I → Detector M) (F : SpacetimeFault Q T M) : IsSyndromeFree detectors F ↔ ∀ (idx : I), ¬(detectors idx).isViolated F.timeFaults

Equivalently, a fault is syndrome-free iff every detector is not violated.

theorem SpacetimeLogicalFault.isSyndromeFree_iff_syndromeVec {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} (detectors : I → Detector M) (F : SpacetimeFault Q T M) : IsSyndromeFree detectors F ↔ syndromeVec detectors F = 0

Equivalently, syndrome-free means the syndrome vector is identically zero.

Outcome-Changing Faults

The gauging procedure produces a classical outcome σ ∈ ZMod 2 (the measurement sign) and a post-measurement state. A fault "changes the outcome" if it either:

1. Flips the measurement sign σ (changing the classical bit), OR
2. Applies a non-trivial logical operator to the post-measurement code state.

We parametrize the outcome-preserving predicate abstractly, as the precise quantum state evolution requires Hilbert space formalism. The key structural content is the syndrome-free dichotomy: every syndrome-free fault is either outcome-changing (logical fault) or outcome-preserving (stabilizer).

def SpacetimeLogicalFault.IsOutcomePreserving {M : Type u_5} {Q : Type u_6} {T : Type u_7} (outcomePreserving : SpacetimeFault Q T M → Prop) (F : SpacetimeFault Q T M) : Prop

A spacetime fault is outcome-preserving if its net effect on the procedure is trivial: it preserves both the measurement sign and the logical information in the post-measurement state. We parametrize by a predicate classifying outcome-preserving faults.

Equations

• SpacetimeLogicalFault.IsOutcomePreserving outcomePreserving F = outcomePreserving F

def SpacetimeLogicalFault.IsOutcomeChanging {M : Type u_5} {Q : Type u_6} {T : Type u_7} (outcomePreserving : SpacetimeFault Q T M → Prop) (F : SpacetimeFault Q T M) : Prop

A fault changes the outcome if it is not outcome-preserving.

Equations

• SpacetimeLogicalFault.IsOutcomeChanging outcomePreserving F = ¬outcomePreserving F

Main Definitions

def SpacetimeLogicalFault.IsSpacetimeLogicalFault {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} (detectors : I → Detector M) (outcomePreserving : SpacetimeFault Q T M → Prop) (F : SpacetimeFault Q T M) : Prop

A spacetime logical fault is a syndrome-free fault that changes the outcome of the fault-tolerant gauging measurement procedure. Condition 1: No detector is violated (syndrome is empty). Condition 2: The fault changes the measurement result or applies a non-trivial logical to the post-measurement state.

Equations

• SpacetimeLogicalFault.IsSpacetimeLogicalFault detectors outcomePreserving F = (SpacetimeLogicalFault.IsSyndromeFree detectors F ∧ SpacetimeLogicalFault.IsOutcomeChanging outcomePreserving F)

def SpacetimeLogicalFault.IsSpacetimeStabilizer {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} (detectors : I → Detector M) (outcomePreserving : SpacetimeFault Q T M → Prop) (F : SpacetimeFault Q T M) : Prop

A spacetime stabilizer is a syndrome-free fault that does NOT change the outcome of the procedure. Condition 1: No detector is violated (syndrome is empty). Condition 2: The fault preserves both the measurement result and the logical information in the post-measurement state.

Equations

• SpacetimeLogicalFault.IsSpacetimeStabilizer detectors outcomePreserving F = (SpacetimeLogicalFault.IsSyndromeFree detectors F ∧ SpacetimeLogicalFault.IsOutcomePreserving outcomePreserving F)

Dichotomy

theorem SpacetimeLogicalFault.syndromeFree_dichotomy {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} (detectors : I → Detector M) (outcomePreserving : SpacetimeFault Q T M → Prop) (F : SpacetimeFault Q T M) (hfree : IsSyndromeFree detectors F) : IsSpacetimeLogicalFault detectors outcomePreserving F ∨ IsSpacetimeStabilizer detectors outcomePreserving F

Every syndrome-free fault is either a spacetime logical fault or a spacetime stabilizer. This is a tautological consequence of the definitions: a syndrome-free fault either changes the outcome (logical fault) or does not (stabilizer).

theorem SpacetimeLogicalFault.logicalFault_not_stabilizer {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} (detectors : I → Detector M) (outcomePreserving : SpacetimeFault Q T M → Prop) (F : SpacetimeFault Q T M) (hlog : IsSpacetimeLogicalFault detectors outcomePreserving F) : ¬IsSpacetimeStabilizer detectors outcomePreserving F

The dichotomy is exclusive: a fault cannot be both a logical fault and a stabilizer.

theorem SpacetimeLogicalFault.stabilizer_not_logicalFault {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} (detectors : I → Detector M) (outcomePreserving : SpacetimeFault Q T M → Prop) (F : SpacetimeFault Q T M) (hstab : IsSpacetimeStabilizer detectors outcomePreserving F) : ¬IsSpacetimeLogicalFault detectors outcomePreserving F

Conversely, a stabilizer is not a logical fault.

Accessor Lemmas

theorem SpacetimeLogicalFault.IsSpacetimeLogicalFault.syndromeFree {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} {detectors : I → Detector M} {outcomePreserving : SpacetimeFault Q T M → Prop} {F : SpacetimeFault Q T M} (h : IsSpacetimeLogicalFault detectors outcomePreserving F) : IsSyndromeFree detectors F

A spacetime logical fault is syndrome-free.

theorem SpacetimeLogicalFault.IsSpacetimeLogicalFault.changesOutcome {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} {detectors : I → Detector M} {outcomePreserving : SpacetimeFault Q T M → Prop} {F : SpacetimeFault Q T M} (h : IsSpacetimeLogicalFault detectors outcomePreserving F) : IsOutcomeChanging outcomePreserving F

A spacetime logical fault changes the outcome.

theorem SpacetimeLogicalFault.IsSpacetimeStabilizer.syndromeFree {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} {detectors : I → Detector M} {outcomePreserving : SpacetimeFault Q T M → Prop} {F : SpacetimeFault Q T M} (h : IsSpacetimeStabilizer detectors outcomePreserving F) : IsSyndromeFree detectors F

A spacetime stabilizer is syndrome-free.

theorem SpacetimeLogicalFault.IsSpacetimeStabilizer.preservesOutcome {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} {detectors : I → Detector M} {outcomePreserving : SpacetimeFault Q T M → Prop} {F : SpacetimeFault Q T M} (h : IsSpacetimeStabilizer detectors outcomePreserving F) : IsOutcomePreserving outcomePreserving F

A spacetime stabilizer preserves the outcome.

Empty Fault is a Stabilizer

theorem SpacetimeLogicalFault.empty_isSyndromeFree {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} [DecidableEq Q] [DecidableEq T] [DecidableEq (SpaceFault Q T)] (detectors : I → Detector M) : IsSyndromeFree detectors SpacetimeFault.empty

The empty fault has empty syndrome: no faults means no detector violations.

theorem SpacetimeLogicalFault.empty_isSpacetimeStabilizer {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} [DecidableEq Q] [DecidableEq T] [DecidableEq (SpaceFault Q T)] (detectors : I → Detector M) (outcomePreserving : SpacetimeFault Q T M → Prop) (hempty : outcomePreserving SpacetimeFault.empty) : IsSpacetimeStabilizer detectors outcomePreserving SpacetimeFault.empty

The empty fault is a spacetime stabilizer, provided it is outcome-preserving (the natural requirement: no fault means no change).

Weight Properties

theorem SpacetimeLogicalFault.syndromeFree_weight_zero_eq_empty {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} [DecidableEq Q] [DecidableEq T] [DecidableEq (SpaceFault Q T)] {detectors : I → Detector M} {F : SpacetimeFault Q T M} (_hfree : IsSyndromeFree detectors F) (hw : F.weight = 0) : F = SpacetimeFault.empty

A syndrome-free fault of weight 0 is the empty fault.

theorem SpacetimeLogicalFault.IsSpacetimeLogicalFault.weight_pos {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} [DecidableEq Q] [DecidableEq T] [DecidableEq (SpaceFault Q T)] {detectors : I → Detector M} {outcomePreserving : SpacetimeFault Q T M → Prop} {F : SpacetimeFault Q T M} (hlog : IsSpacetimeLogicalFault detectors outcomePreserving F) (hempty : outcomePreserving SpacetimeFault.empty) : 0 < F.weight

A spacetime logical fault must have positive weight (it cannot be empty).

Characterization via Syndrome Vector

theorem SpacetimeLogicalFault.IsSpacetimeLogicalFault.syndromeVec_eq_zero {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} {detectors : I → Detector M} {outcomePreserving : SpacetimeFault Q T M → Prop} {F : SpacetimeFault Q T M} (h : IsSpacetimeLogicalFault detectors outcomePreserving F) : syndromeVec detectors F = 0

A spacetime logical fault has zero syndrome vector.

theorem SpacetimeLogicalFault.IsSpacetimeStabilizer.syndromeVec_eq_zero {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} {detectors : I → Detector M} {outcomePreserving : SpacetimeFault Q T M → Prop} {F : SpacetimeFault Q T M} (h : IsSpacetimeStabilizer detectors outcomePreserving F) : syndromeVec detectors F = 0

A spacetime stabilizer has zero syndrome vector.

Classification of Syndrome-Free Faults

theorem SpacetimeLogicalFault.syndromeFree_iff_logicalFault_or_stabilizer {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} (detectors : I → Detector M) (outcomePreserving : SpacetimeFault Q T M → Prop) (F : SpacetimeFault Q T M) : IsSyndromeFree detectors F ↔ IsSpacetimeLogicalFault detectors outcomePreserving F ∨ IsSpacetimeStabilizer detectors outcomePreserving F

The set of all syndrome-free faults partitions into logical faults and stabilizers.

theorem SpacetimeLogicalFault.syndromeFree_logicalFault_iff_not_stabilizer {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} (detectors : I → Detector M) (outcomePreserving : SpacetimeFault Q T M → Prop) (F : SpacetimeFault Q T M) (hfree : IsSyndromeFree detectors F) : IsSpacetimeLogicalFault detectors outcomePreserving F ↔ ¬IsSpacetimeStabilizer detectors outcomePreserving F

A syndrome-free fault is a logical fault iff it is not a stabilizer.

theorem SpacetimeLogicalFault.syndromeFree_stabilizer_iff_not_logicalFault {I : Type u_4} [Fintype I] [DecidableEq I] {M : Type u_5} [DecidableEq M] [DecidableEq (TimeFault M)] {Q : Type u_6} {T : Type u_7} (detectors : I → Detector M) (outcomePreserving : SpacetimeFault Q T M → Prop) (F : SpacetimeFault Q T M) (hfree : IsSyndromeFree detectors F) : IsSpacetimeStabilizer detectors outcomePreserving F ↔ ¬IsSpacetimeLogicalFault detectors outcomePreserving F

A syndrome-free fault is a stabilizer iff it is not a logical fault.

Gauging Sign Flip

For the fault-tolerant gauging procedure specifically, we can define the sign flip indicator that tracks whether time-faults flip the measurement sign σ.

noncomputable def SpacetimeLogicalFault.gaussSignFlip {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) : ZMod 2

The sign flip indicator: the parity of time-faults that affect Gauss's law measurements. A fault changes the gauging sign σ iff this is 1 (mod 2). σ = ∑_v ε_v, and a time-fault on a Gauss measurement flips one ε_v.

Equations

• One or more equations did not get rendered due to their size.

def SpacetimeLogicalFault.FlipsGaugingSign {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) : Prop

A fault flips the gauging sign if the sign flip indicator is 1.

Equations

• SpacetimeLogicalFault.FlipsGaugingSign proc F = (SpacetimeLogicalFault.gaussSignFlip proc F = 1)

def SpacetimeLogicalFault.PreservesGaugingSign {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) : Prop

A fault preserves the gauging sign if the sign flip indicator is 0.

Equations

• SpacetimeLogicalFault.PreservesGaugingSign proc F = (SpacetimeLogicalFault.gaussSignFlip proc F = 0)

theorem SpacetimeLogicalFault.gaussSignFlip_zero_or_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} (proc : FaultTolerantGaugingProcedure G cycles checks) (F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) : gaussSignFlip proc F = 0 ∨ gaussSignFlip proc F = 1

The sign flip is always 0 or 1 in ZMod 2.

theorem SpacetimeLogicalFault.flipsOrPreserves {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) : FlipsGaugingSign proc F ∨ PreservesGaugingSign proc F

The sign flip dichotomy: a fault either flips or preserves the gauging sign.

theorem SpacetimeLogicalFault.flipsGaugingSign_not_preserves {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) (h : FlipsGaugingSign proc F) : ¬PreservesGaugingSign proc F

Flipping and preserving are mutually exclusive.

theorem SpacetimeLogicalFault.preservesGaugingSign_not_flips {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) (h : PreservesGaugingSign proc F) : ¬FlipsGaugingSign proc F

Preserving and flipping are mutually exclusive.

Instantiation for the Gauging Procedure

We provide specialized definitions for the fault-tolerant gauging procedure using its specific detector index type and measurement labels.

def SpacetimeLogicalFault.IsSyndromeFreeGauging {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) (F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) : Prop

A syndrome-free fault in the gauging procedure: no detector from the spacetime code (Lemma 4) is violated.

Equations

• SpacetimeLogicalFault.IsSyndromeFreeGauging proc detectors F = ∀ (idx : FaultTolerantGaugingProcedure.DetectorIndex V C J (↑G.edgeSet) proc.d), ¬(detectors idx).isViolated F.timeFaults

def SpacetimeLogicalFault.IsGaugingLogicalFault {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) : Prop

A spacetime logical fault in the gauging procedure: syndrome-free AND changes the outcome.

Equations

• SpacetimeLogicalFault.IsGaugingLogicalFault proc detectors outcomePreserving F = (SpacetimeLogicalFault.IsSyndromeFreeGauging proc detectors F ∧ ¬outcomePreserving F)

def SpacetimeLogicalFault.IsGaugingStabilizer {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) : Prop

A spacetime stabilizer in the gauging procedure: syndrome-free AND preserves the outcome.

Equations

• SpacetimeLogicalFault.IsGaugingStabilizer proc detectors outcomePreserving F = (SpacetimeLogicalFault.IsSyndromeFreeGauging proc detectors F ∧ outcomePreserving F)

theorem SpacetimeLogicalFault.gaugingSyndromeFree_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) (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 : IsSyndromeFreeGauging proc detectors F) : IsGaugingLogicalFault proc detectors outcomePreserving F ∨ IsGaugingStabilizer proc detectors outcomePreserving F

Every syndrome-free fault in the gauging procedure is either a logical fault or a stabilizer.

theorem SpacetimeLogicalFault.gaugingLogicalFault_not_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) (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 : IsGaugingLogicalFault proc detectors outcomePreserving F) : ¬IsGaugingStabilizer proc detectors outcomePreserving F

The gauging dichotomy is exclusive.

theorem SpacetimeLogicalFault.gaugingStabilizer_not_logicalFault {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) (hstab : IsGaugingStabilizer proc detectors outcomePreserving F) : ¬IsGaugingLogicalFault proc detectors outcomePreserving F

A gauging stabilizer is not a logical fault.

theorem SpacetimeLogicalFault.gaugingSyndromeFree_logicalFault_iff {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) (hfree : IsSyndromeFreeGauging proc detectors F) : IsGaugingLogicalFault proc detectors outcomePreserving F ↔ ¬IsGaugingStabilizer proc detectors outcomePreserving F

A syndrome-free gauging fault is a logical fault iff not a stabilizer.

theorem SpacetimeLogicalFault.gaugingSyndromeFree_stabilizer_iff {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) (hfree : IsSyndromeFreeGauging proc detectors F) : IsGaugingStabilizer proc detectors outcomePreserving F ↔ ¬IsGaugingLogicalFault proc detectors outcomePreserving F

A syndrome-free gauging fault is a stabilizer iff not a logical fault.