Def_11: Spacetime Fault-Distance

Statement

The spacetime fault-distance of the fault-tolerant gauging measurement procedure is defined as: $$d_{\text{spacetime}} = \min\{|F| : F \text{ is a spacetime logical fault}\}$$ where $|F|$ denotes the weight of $F$, counted as the total number of:

• Single-qubit Pauli errors (each $X$, $Y$, or $Z$ error on one qubit at one time counts as weight 1), plus
• Single measurement errors (each incorrectly reported measurement counts as weight 1), plus
• Single initialization errors (each faulty initialization counts as weight 1).

Intuitively, $d_{\text{spacetime}}$ is the minimum number of independent faults required to cause a logical error without being detected.

Main Definitions

• logicalFaultWeights : The set of weights of all spacetime logical faults
• hasLogicalFault : Predicate that there exists at least one spacetime logical fault
• spacetimeFaultDistance : The minimum weight d_ST of any spacetime logical fault

Key Properties

• spacetimeFaultDistance_le_weight : d_ST ≤ weight of any logical fault
• spacetimeFaultDistance_is_min : d_ST is achieved by some logical fault
• not_logical_of_weight_lt : Faults with weight < d_ST cannot be logical faults
• spacetimeFaultDistance_pos_iff : Characterization of when d_ST > 0

Section 1: Set of Logical Fault Weights

We define the set of weights of all spacetime logical faults. The spacetime fault-distance is the minimum of this set.

def logicalFaultWeights {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) : Set ℕ

The set of weights of spacetime logical faults. W = {|F| : F is a spacetime logical fault}

Equations

• logicalFaultWeights DC baseOutcomes logicalEffect times = {w : ℕ | ∃ (F : SpacetimeFault V E M), IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F ∧ F.weight times = w}

def undetectableNonStabilizerWeights {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) : Set ℕ

The set of weights of all empty-syndrome (undetectable) non-stabilizer faults

Equations

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

theorem logicalFaultWeights_eq_undetectableNonStabilizer {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) : logicalFaultWeights DC baseOutcomes logicalEffect times = undetectableNonStabilizerWeights DC baseOutcomes logicalEffect times

The two weight sets are equal by definition of logical fault

Section 2: Predicate for Existence of Logical Faults

def hasLogicalFault {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) : Prop

Predicate: there exists at least one spacetime logical fault

Equations

• hasLogicalFault DC baseOutcomes logicalEffect = ∃ (F : SpacetimeFault V E M), IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F

theorem hasLogicalFault_of_weights_nonempty {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (h : (logicalFaultWeights DC baseOutcomes logicalEffect times).Nonempty) : hasLogicalFault DC baseOutcomes logicalEffect

Nonemptiness of logical fault weights implies existence of logical faults

theorem weights_nonempty_of_hasLogicalFault {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (h : hasLogicalFault DC baseOutcomes logicalEffect) : (logicalFaultWeights DC baseOutcomes logicalEffect times).Nonempty

Existence of logical faults implies nonemptiness of weights

Section 3: Spacetime Fault Distance Definition

The spacetime fault-distance is the minimum weight of any spacetime logical fault.

noncomputable def spacetimeFaultDistance {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) : ℕ

The spacetime fault-distance d_ST as a natural number. d_ST = min{|F| : F is a spacetime logical fault}

If no logical faults exist (which would mean perfect error correction), we return 0 as a sentinel value. In practice, interesting codes always have logical faults, so d_ST > 0.

We define this using WellFounded.min on the set of logical fault weights.

Equations

• spacetimeFaultDistance DC baseOutcomes logicalEffect times = if h : hasLogicalFault DC baseOutcomes logicalEffect then ⋯.min (logicalFaultWeights DC baseOutcomes logicalEffect times) ⋯ else 0

Section 4: Main Properties

theorem spacetimeFaultDistance_le_weight {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (F : SpacetimeFault V E M) (hF : IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F) : spacetimeFaultDistance DC baseOutcomes logicalEffect times ≤ F.weight times

The spacetime fault distance is at most the weight of any logical fault

theorem weight_ge_spacetimeFaultDistance {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (F : SpacetimeFault V E M) (hF : IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F) : F.weight times ≥ spacetimeFaultDistance DC baseOutcomes logicalEffect times

The spacetime fault distance is a lower bound: all logical faults have weight ≥ d_ST

theorem spacetimeFaultDistance_is_min {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (h : hasLogicalFault DC baseOutcomes logicalEffect) : ∃ (F : SpacetimeFault V E M), IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F ∧ F.weight times = spacetimeFaultDistance DC baseOutcomes logicalEffect times

If logical faults exist, the minimum is achieved

theorem spacetimeFaultDistance_zero_of_no_logical {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (h : ¬hasLogicalFault DC baseOutcomes logicalEffect) : spacetimeFaultDistance DC baseOutcomes logicalEffect times = 0

If no logical faults exist, d_ST = 0

Section 5: Faults Below Distance Cannot Be Logical

theorem not_logical_of_weight_lt {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (F : SpacetimeFault V E M) (hF : F.weight times < spacetimeFaultDistance DC baseOutcomes logicalEffect times) : ¬IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F

A fault with weight < d_ST cannot be a logical fault

theorem detectable_or_stabilizer_if_weight_lt {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (F : SpacetimeFault V E M) (hF : F.weight times < spacetimeFaultDistance DC baseOutcomes logicalEffect times) : ¬hasEmptySyndrome DC baseOutcomes F ∨ ¬affectsLogicalInfo logicalEffect F

A fault with weight < d_ST is either detectable or a stabilizer

Section 6: Characterization of Positive Distance

theorem spacetimeFaultDistance_pos_iff {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) : 0 < spacetimeFaultDistance DC baseOutcomes logicalEffect times ↔ hasLogicalFault DC baseOutcomes logicalEffect ∧ ∀ (F : SpacetimeFault V E M), IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F → 0 < F.weight times

d_ST > 0 iff there exist logical faults and all have positive weight

Section 7: Helper Lemmas

@[simp]

theorem spacetimeFaultDistance_nonneg {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) : 0 ≤ spacetimeFaultDistance DC baseOutcomes logicalEffect times

The spacetime fault distance is non-negative

theorem logicalFaultWeights_bounded_below {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (w : ℕ) : w ∈ logicalFaultWeights DC baseOutcomes logicalEffect times → spacetimeFaultDistance DC baseOutcomes logicalEffect times ≤ w

Logical fault weights are bounded below by d_ST

theorem spacetimeFaultDistance_mem_weights {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (h : hasLogicalFault DC baseOutcomes logicalEffect) : spacetimeFaultDistance DC baseOutcomes logicalEffect times ∈ logicalFaultWeights DC baseOutcomes logicalEffect times

d_ST ∈ logicalFaultWeights when logical faults exist

theorem exists_logical_of_exact_distance {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (h : hasLogicalFault DC baseOutcomes logicalEffect) : ∃ (F : SpacetimeFault V E M), IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F ∧ F.weight times = spacetimeFaultDistance DC baseOutcomes logicalEffect times

A fault of weight exactly d_ST exists when logical faults exist

Section 8: Fault Tolerance Threshold

A code can tolerate faults of weight t if t < d_ST. This section establishes the relationship between fault tolerance and d_ST.

def canTolerateFaults {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (t : ℕ) : Prop

A code can tolerate weight-t faults if t < d_ST

Equations

• canTolerateFaults DC baseOutcomes logicalEffect times t = (t < spacetimeFaultDistance DC baseOutcomes logicalEffect times)

theorem tolerable_implies_correctable {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (t : ℕ) (htol : canTolerateFaults DC baseOutcomes logicalEffect times t) (F : SpacetimeFault V E M) (hF : F.weight times ≤ t) : ¬hasEmptySyndrome DC baseOutcomes F ∨ ¬affectsLogicalInfo logicalEffect F

If the code can tolerate weight t, any fault of weight ≤ t is correctable or stabilizer

theorem max_tolerable_weight {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (hpos : 0 < spacetimeFaultDistance DC baseOutcomes logicalEffect times) : canTolerateFaults DC baseOutcomes logicalEffect times (spacetimeFaultDistance DC baseOutcomes logicalEffect times - 1)

The maximum tolerable fault weight is d_ST - 1 (when d_ST > 0)

Section 9: Intuitive Interpretation

The spacetime fault-distance d_ST is the minimum number of independent faults required to cause a logical error without being detected.

theorem distance_pos_means_nontrivial {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (hpos : 0 < spacetimeFaultDistance DC baseOutcomes logicalEffect times) (F : SpacetimeFault V E M) : F.weight times = 0 → hasEmptySyndrome DC baseOutcomes F → ¬affectsLogicalInfo logicalEffect F

If d_ST > 0, weight-0 undetectable faults must be stabilizers

theorem identity_not_logical {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (h_logical : LogicalEffectIsGroupLike logicalEffect) (_h_base : DC.allSatisfied baseOutcomes) : ¬IsSpacetimeLogicalFault DC baseOutcomes logicalEffect 1

The identity fault has weight 0 and empty syndrome, so it's a stabilizer

Section 10: Distance as Infimum Characterization

Alternative characterization of spacetime fault distance using infimum.

theorem spacetimeFaultDistance_is_glb {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] [Fintype V] [Fintype E] [Fintype M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (times : Finset TimeStep) (h : hasLogicalFault DC baseOutcomes logicalEffect) : IsGLB (logicalFaultWeights DC baseOutcomes logicalEffect times) (spacetimeFaultDistance DC baseOutcomes logicalEffect times)

The spacetime fault distance satisfies the infimum property: it's the greatest lower bound of logical fault weights

Summary

This formalization captures the spacetime fault-distance from fault-tolerant quantum error correction:

1. Logical Fault Weights: The set W = {|F| : F is a spacetime logical fault} where weight counts single-qubit Pauli errors + measurement errors + initialization errors.

2. Spacetime Fault Distance: d_ST = min(W), the minimum weight of any logical fault. If no logical faults exist, d_ST = 0 as a sentinel value.

3. Fault Tolerance: Faults with weight < d_ST cannot be logical faults. They are either:

   • Detectable (non-empty syndrome), or
   • Stabilizers (don't affect logical information)

4. Intuition: d_ST is the minimum number of independent faults required to cause a logical error without being detected.

Key properties proven:

• d_ST ≤ weight of any logical fault (it's a lower bound)
• The minimum is achieved when logical faults exist
• Faults with weight < d_ST cannot be logical faults
• d_ST > 0 iff logical faults exist and all have positive weight
• d_ST is the greatest lower bound (infimum) of logical fault weights