Def_10: Spacetime Logical Fault

Statement

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

1. Does not violate any detector (has empty syndrome), AND
2. Causes a logical error, i.e., changes the outcome of the gauging measurement or introduces a logical Pauli error on the encoded quantum information.

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

1. Does not violate any detector (has empty syndrome), AND
2. Does NOT affect the logical information or measurement outcome.

Every fault with empty syndrome is either a spacetime stabilizer (trivial) or a spacetime logical fault (non-trivial). The set of spacetime stabilizers forms a group, and two faults are equivalent if they differ by a spacetime stabilizer.

Main Definitions

• Syndrome : The set of detectors violated by a spacetime fault
• hasEmptySyndrome : Whether a fault has empty syndrome (violates no detectors)
• IsSpacetimeStabilizer : Faults with empty syndrome that don't affect logical information
• IsSpacetimeLogicalFault : Faults with empty syndrome that DO affect logical information
• FaultEquivalent : Equivalence relation where faults differ by a stabilizer

Key Properties

• spacetimeStabilizerSubgroup : Spacetime stabilizers form a subgroup
• emptySyndrome_partition : Empty-syndrome faults partition into stabilizers and logical faults
• faultEquivalent_equivalence : Fault equivalence is an equivalence relation

Syndrome

The syndrome of a spacetime fault is the set of detectors it violates.

def applyFaultToOutcomes {V : Type u_1} {E : Type u_2} {M : Type u_3} (baseOutcomes : OutcomeAssignment M) (fault : SpacetimeFault V E M) : OutcomeAssignment M

Apply a spacetime fault to measurement outcomes. Time-faults flip outcomes.

Equations

• applyFaultToOutcomes baseOutcomes fault m t = if fault.timeErrors m t = true then baseOutcomes m t + 1 else baseOutcomes m t

def computeSyndrome {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) (fault : SpacetimeFault V E M) : Finset (Detector V E M)

Compute the syndrome of a spacetime fault given a detector collection. The syndrome is the set of detectors violated by the fault.

Equations

• computeSyndrome DC baseOutcomes fault = {D ∈ DC.detectors | D.isViolated (applyFaultToOutcomes baseOutcomes fault)}

def inSyndrome {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) (fault : SpacetimeFault V E M) (D : Detector V E M) : Prop

The syndrome as a predicate on detectors

Equations

• inSyndrome DC baseOutcomes fault D = (D ∈ computeSyndrome DC baseOutcomes fault)

def hasEmptySyndrome {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) (fault : SpacetimeFault V E M) : Prop

A fault has empty syndrome if it violates no detectors

Equations

• hasEmptySyndrome DC baseOutcomes fault = (computeSyndrome DC baseOutcomes fault = ∅)

instance decHasEmptySyndrome {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) (fault : SpacetimeFault V E M) : Decidable (hasEmptySyndrome DC baseOutcomes fault)

Equations

• decHasEmptySyndrome DC baseOutcomes fault = inferInstanceAs (Decidable (computeSyndrome DC baseOutcomes fault = ∅))

@[simp]

theorem hasEmptySyndrome_iff {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) (fault : SpacetimeFault V E M) : hasEmptySyndrome DC baseOutcomes fault ↔ ∀ D ∈ DC.detectors, D.isSatisfied (applyFaultToOutcomes baseOutcomes fault)

Identity fault has empty syndrome

theorem identity_hasEmptySyndrome {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) (h_base : DC.allSatisfied baseOutcomes) : hasEmptySyndrome DC baseOutcomes 1

The identity fault has empty syndrome (in any fault-free base outcome setting)

Logical Effect Predicate

To distinguish spacetime stabilizers from logical faults, we need a notion of "affecting logical information". We model this abstractly.

def affectsLogicalInfo {V : Type u_1} {E : Type u_2} {M : Type u_3} (logicalEffect : SpacetimeFault V E M → Prop) (fault : SpacetimeFault V E M) : Prop

Abstract predicate: whether a fault affects the logical information. This captures:

• Changes to the gauging measurement outcome
• Introduction of logical Pauli errors on encoded qubits

In practice, this is determined by the code structure and logical operators.

Equations

• affectsLogicalInfo logicalEffect fault = logicalEffect fault

def preservesLogicalInfo {V : Type u_1} {E : Type u_2} {M : Type u_3} (logicalEffect : SpacetimeFault V E M → Prop) (fault : SpacetimeFault V E M) : Prop

The negation: fault does NOT affect logical info

Equations

• preservesLogicalInfo logicalEffect fault = ¬logicalEffect fault

Spacetime Stabilizers

Spacetime stabilizers are faults with empty syndrome that preserve logical information.

structure IsSpacetimeStabilizer {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) (fault : SpacetimeFault V E M) : Prop

A spacetime stabilizer: empty syndrome AND preserves logical information

• emptySyndrome : hasEmptySyndrome DC baseOutcomes fault

  The fault has empty syndrome (violates no detectors)

• preservesLogical : preservesLogicalInfo logicalEffect fault

  The fault preserves logical information

def spacetimeStabilizerSet {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) : Set (SpacetimeFault V E M)

The set of spacetime stabilizers as a set

Equations

• spacetimeStabilizerSet DC baseOutcomes logicalEffect = {f : SpacetimeFault V E M | IsSpacetimeStabilizer DC baseOutcomes logicalEffect f}

Spacetime Logical Faults

Spacetime logical faults are faults with empty syndrome that DO affect logical information.

structure IsSpacetimeLogicalFault {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) (fault : SpacetimeFault V E M) : Prop

A spacetime logical fault: empty syndrome AND affects logical information

• emptySyndrome : hasEmptySyndrome DC baseOutcomes fault

  The fault has empty syndrome (violates no detectors)

• affectsLogical : affectsLogicalInfo logicalEffect fault

  The fault DOES affect logical information

def spacetimeLogicalFaultSet {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) : Set (SpacetimeFault V E M)

The set of spacetime logical faults as a set

Equations

• spacetimeLogicalFaultSet DC baseOutcomes logicalEffect = {f : SpacetimeFault V E M | IsSpacetimeLogicalFault DC baseOutcomes logicalEffect f}

Partition of Empty-Syndrome Faults

Every fault with empty syndrome is either a stabilizer or a logical fault.

def emptySyndromeSet {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) : Set (SpacetimeFault V E M)

The set of faults with empty syndrome

Equations

• emptySyndromeSet DC baseOutcomes = {f : SpacetimeFault V E M | hasEmptySyndrome DC baseOutcomes f}

theorem emptySyndrome_partition {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) (f : SpacetimeFault V E M) (h_empty : hasEmptySyndrome DC baseOutcomes f) : IsSpacetimeStabilizer DC baseOutcomes logicalEffect f ∨ IsSpacetimeLogicalFault DC baseOutcomes logicalEffect f

Stabilizers and logical faults partition the empty-syndrome faults

theorem stabilizer_logicalFault_disjoint {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) (f : SpacetimeFault V E M) : ¬(IsSpacetimeStabilizer DC baseOutcomes logicalEffect f ∧ IsSpacetimeLogicalFault DC baseOutcomes logicalEffect f)

Stabilizers and logical faults are disjoint

theorem stabilizer_logicalFault_union {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) : spacetimeStabilizerSet DC baseOutcomes logicalEffect ∪ spacetimeLogicalFaultSet DC baseOutcomes logicalEffect = emptySyndromeSet DC baseOutcomes

Union of stabilizers and logical faults equals empty-syndrome set

Spacetime Stabilizers Form a Subgroup

Under appropriate conditions on the logical effect predicate, spacetime stabilizers form a subgroup of all spacetime faults.

structure LogicalEffectIsGroupLike {V : Type u_1} {E : Type u_2} {M : Type u_3} (logicalEffect : SpacetimeFault V E M → Prop) : Prop

Condition: logical effect is preserved under product (group-like)

• identity_preserves : ¬logicalEffect 1

  Identity preserves logical info

• mul_preserves (f g : SpacetimeFault V E M) : ¬logicalEffect f → ¬logicalEffect g → ¬logicalEffect (f * g)

  Product of two stabilizers is a stabilizer (closure under multiplication)

• inv_preserves (f : SpacetimeFault V E M) : ¬logicalEffect f → ¬logicalEffect f⁻¹

  Inverse of a stabilizer is a stabilizer

structure SyndromeIsGroupHomomorphism {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) : Prop

Condition: syndrome computation respects the group structure

• identity_empty : hasEmptySyndrome DC baseOutcomes 1

  Identity has empty syndrome

• mul_respects (f g : SpacetimeFault V E M) : hasEmptySyndrome DC baseOutcomes f → hasEmptySyndrome DC baseOutcomes g → hasEmptySyndrome DC baseOutcomes (f * g)

  Product respects syndrome

• inv_respects (f : SpacetimeFault V E M) : hasEmptySyndrome DC baseOutcomes f → hasEmptySyndrome DC baseOutcomes f⁻¹

  Inverse respects syndrome

def spacetimeStabilizerSubgroup {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_syndrome : SyndromeIsGroupHomomorphism DC baseOutcomes) : Subgroup (SpacetimeFault V E M)

Spacetime stabilizers form a subgroup under the right conditions

Equations

• spacetimeStabilizerSubgroup DC baseOutcomes logicalEffect h_logical h_syndrome = { carrier := spacetimeStabilizerSet DC baseOutcomes logicalEffect, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Fault Equivalence

Two faults are equivalent if they differ by a spacetime stabilizer. This forms an equivalence relation.

def FaultEquivalent {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) (f g : SpacetimeFault V E M) : Prop

Two faults are equivalent if they differ by a spacetime stabilizer

Equations

• FaultEquivalent DC baseOutcomes logicalEffect f g = IsSpacetimeStabilizer DC baseOutcomes logicalEffect (f⁻¹ * g)

theorem faultEquivalent_refl {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_syndrome : SyndromeIsGroupHomomorphism DC baseOutcomes) (f : SpacetimeFault V E M) : FaultEquivalent DC baseOutcomes logicalEffect f f

Fault equivalence is reflexive

theorem faultEquivalent_symm {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_syndrome : SyndromeIsGroupHomomorphism DC baseOutcomes) (f g : SpacetimeFault V E M) (h : FaultEquivalent DC baseOutcomes logicalEffect f g) : FaultEquivalent DC baseOutcomes logicalEffect g f

Fault equivalence is symmetric

theorem faultEquivalent_trans {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_syndrome : SyndromeIsGroupHomomorphism DC baseOutcomes) (f g k : SpacetimeFault V E M) (hfg : FaultEquivalent DC baseOutcomes logicalEffect f g) (hgk : FaultEquivalent DC baseOutcomes logicalEffect g k) : FaultEquivalent DC baseOutcomes logicalEffect f k

Fault equivalence is transitive

theorem faultEquivalent_equivalence {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_syndrome : SyndromeIsGroupHomomorphism DC baseOutcomes) : Equivalence (FaultEquivalent DC baseOutcomes logicalEffect)

Fault equivalence is an equivalence relation

def faultSetoid {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_syndrome : SyndromeIsGroupHomomorphism DC baseOutcomes) : Setoid (SpacetimeFault V E M)

Fault equivalence as a Setoid

Equations

• faultSetoid DC baseOutcomes logicalEffect h_logical h_syndrome = { r := FaultEquivalent DC baseOutcomes logicalEffect, iseqv := ⋯ }

Equivalence Classes as Cosets

Fault equivalence classes correspond to cosets of the stabilizer subgroup.

def FaultQuotient {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_syndrome : SyndromeIsGroupHomomorphism DC baseOutcomes) : Type (max (max u_3 u_2) u_1)

The quotient by fault equivalence is the quotient by the stabilizer subgroup

Equations

• FaultQuotient DC baseOutcomes logicalEffect h_logical h_syndrome = (SpacetimeFault V E M ⧸ spacetimeStabilizerSubgroup DC baseOutcomes logicalEffect h_logical h_syndrome)

Characterization: Logical Fault iff Non-trivial Coset

A fault is a logical fault iff it represents a non-trivial coset in the quotient.

theorem isLogicalFault_iff_not_stabilizer {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) (f : SpacetimeFault V E M) (h_empty : hasEmptySyndrome DC baseOutcomes f) : IsSpacetimeLogicalFault DC baseOutcomes logicalEffect f ↔ ¬IsSpacetimeStabilizer DC baseOutcomes logicalEffect f

A fault with empty syndrome is a spacetime logical fault iff it's NOT a stabilizer

Summary

This formalization captures:

1. Syndrome: The set of detectors violated by a fault.

2. Spacetime Stabilizers: Faults with empty syndrome that preserve logical information. These form a subgroup under appropriate conditions.

3. Spacetime Logical Faults: Faults with empty syndrome that DO affect logical information.

4. Partition: Every empty-syndrome fault is either a stabilizer or a logical fault.

5. Fault Equivalence: Two faults are equivalent if they differ by a stabilizer. This is an equivalence relation.