Def_9: Syndrome

Statement

The syndrome of a spacetime fault F is the set of detectors violated by F. Formally: $$\text{syndrome}(F) = \{D : D \text{ is a detector and } D \text{ reports } -1 \text{ in the presence of } F\}$$

Equivalently, the syndrome is the binary vector over the set of all detectors, where entry D is 1 if detector D is violated and 0 otherwise.

Key properties:

1. The syndrome function is Z₂-linear: syndrome(F₁ · F₂) = syndrome(F₁) + syndrome(F₂) (symmetric difference).
2. A spacetime stabilizer (trivial fault) has empty syndrome.
3. A logical fault is a non-trivial fault with empty syndrome.

Main Definitions

• Syndrome : The syndrome of a spacetime fault (set of violated detectors)
• syndrome : Function computing the syndrome of a fault
• syndromeVector : Binary vector representation of the syndrome
• hasEmptySyndrome : Predicate for faults with no violated detectors

Key Properties

• syndrome_identity : Identity fault has empty syndrome
• syndrome_mul : Syndrome is Z₂-linear (symmetric difference under composition)
• syndrome_inv : Syndrome of inverse equals syndrome of original
• isLogicalFault_iff : A logical fault is non-trivial with empty syndrome

Syndrome Definition

The syndrome of a spacetime fault is the set of detectors it violates. We use Finset directly rather than a wrapper type.

@[reducible, inline]

abbrev Syndrome (V : Type u_4) (E : Type u_5) (M : Type u_6) [DecidableEq V] [DecidableEq E] [DecidableEq M] : Type (max (max u_6 u_5) u_4)

The syndrome of a spacetime fault: the set of detectors violated by the fault. A detector is violated if the observed parity differs from expected parity.

Equations

• Syndrome V E M = Finset (Detector V E M)

def Syndrome.empty {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] : Syndrome V E M

The empty syndrome (no detectors violated)

Equations

• Syndrome.empty = ∅

def Syndrome.add {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (s₁ s₂ : Syndrome V E M) : Syndrome V E M

Combine two syndromes via symmetric difference (Z₂ addition)

Equations

• s₁.add s₂ = symmDiff s₁ s₂

@[simp]

theorem Syndrome.empty_eq {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] : empty = ∅

@[simp]

theorem Syndrome.add_eq {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (s₁ s₂ : Syndrome V E M) : s₁.add s₂ = symmDiff s₁ s₂

theorem Syndrome.add_comm' {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (s₁ s₂ : Syndrome V E M) : s₁.add s₂ = s₂.add s₁

Syndrome addition is commutative

theorem Syndrome.add_assoc' {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (s₁ s₂ s₃ : Syndrome V E M) : (s₁.add s₂).add s₃ = s₁.add (s₂.add s₃)

Syndrome addition is associative

@[simp]

theorem Syndrome.add_empty' {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (s : Syndrome V E M) : s.add empty = s

Empty syndrome is additive identity (right)

@[simp]

theorem Syndrome.empty_add' {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (s : Syndrome V E M) : empty.add s = s

Empty syndrome is additive identity (left)

@[simp]

theorem Syndrome.add_self' {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (s : Syndrome V E M) : s.add s = empty

Every syndrome is its own inverse (self-inverse in Z₂)

def Syndrome.card {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (s : Syndrome V E M) : ℕ

The cardinality of the syndrome (number of violated detectors)

Equations

• s.card = Finset.card s

@[simp]

theorem Syndrome.card_empty' {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] : empty.card = 0

theorem Syndrome.isEmpty_iff_card_zero {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (s : Syndrome V E M) : s = empty ↔ s.card = 0

A syndrome is empty iff its cardinality is 0

Computing the Syndrome

Given a detector collection and measurement outcomes, compute which detectors are violated.

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 the classical measurement outcome.

Equations

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

def syndrome {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) : Syndrome V E M

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

Equations

• syndrome DC baseOutcomes fault = {D ∈ DC.detectors | D.isViolated (applyFaultToOutcomes' 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 = (syndrome 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 (syndrome DC baseOutcomes fault = ∅))

Syndrome as Binary Vector

The syndrome can equivalently be viewed as a binary vector indexed by detectors.

def syndromeVector {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) : ZMod 2

The syndrome as a function to ZMod 2: 1 if violated, 0 if satisfied

Equations

• syndromeVector DC baseOutcomes fault D = if D ∈ syndrome DC baseOutcomes fault then 1 else 0

@[simp]

theorem syndromeVector_violated {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) (hD : D ∈ DC.detectors) (hviol : D.isViolated (applyFaultToOutcomes' baseOutcomes fault)) : syndromeVector DC baseOutcomes fault D = 1

@[simp]

theorem syndromeVector_satisfied {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) (hsat : ¬D.isViolated (applyFaultToOutcomes' baseOutcomes fault)) : syndromeVector DC baseOutcomes fault D = 0

theorem syndromeVector_eq_one_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) (D : Detector V E M) (hD : D ∈ DC.detectors) : syndromeVector DC baseOutcomes fault D = 1 ↔ D.isViolated (applyFaultToOutcomes' baseOutcomes fault)

Syndrome vector is 1 iff detector is violated

Key Properties

theorem syndrome_identity {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) : syndrome DC baseOutcomes 1 = ∅

The identity fault has empty syndrome when base outcomes satisfy all detectors

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)

Empty syndrome iff all detectors in the collection are satisfied

Z₂-Linearity of Syndrome

The key property: syndrome(F₁ · F₂) = syndrome(F₁) + syndrome(F₂) (symmetric difference).

This holds when faults only affect detectors through time-faults (measurement flips), and each detector monitors a fixed set of measurements.

theorem applyFaultToOutcomes_mul {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (baseOutcomes : OutcomeAssignment M) (f g : SpacetimeFault V E M) (m : M) (t : TimeStep) : applyFaultToOutcomes' baseOutcomes (f * g) m t = if (f.timeErrors m t ^^ g.timeErrors m t) = true then baseOutcomes m t + 1 else baseOutcomes m t

Helper: applying two faults in sequence

structure SyndromeLinearCondition {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 for Z₂-linearity: detectors depend only on time-faults in a simple way. Specifically, each detector's violation status depends on the XOR of time-faults over its measurement events.

• localDependence (f g : SpacetimeFault V E M) (D : Detector V E M) : D ∈ DC.detectors → (∀ e ∈ D.measEvents, f.timeErrors e.measurement e.time = g.timeErrors e.measurement e.time) → (D.isViolated (applyFaultToOutcomes' baseOutcomes f) ↔ D.isViolated (applyFaultToOutcomes' baseOutcomes g))

  Each detector's violation only depends on time-faults at its measurement events

• parityDetermines (f : SpacetimeFault V E M) (D : Detector V E M) : D ∈ DC.detectors → (D.isViolated (applyFaultToOutcomes' baseOutcomes f) ↔ {e ∈ D.measEvents | f.timeErrors e.measurement e.time = true}.card % 2 = 1)

  Violation is determined by parity of time-faults on measurement events

theorem syndrome_mul {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) (hlin : SyndromeLinearCondition DC baseOutcomes) (f g : SpacetimeFault V E M) : syndrome DC baseOutcomes (f * g) = symmDiff (syndrome DC baseOutcomes f) (syndrome DC baseOutcomes g)

Under linearity conditions, syndrome respects multiplication (symmetric difference)

theorem syndrome_inv {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) (hlin : SyndromeLinearCondition DC baseOutcomes) (f : SpacetimeFault V E M) : syndrome DC baseOutcomes f⁻¹ = syndrome DC baseOutcomes f

Syndrome of inverse equals syndrome of original (since XOR is self-inverse)

Spacetime Stabilizers and Logical Faults

Based on the syndrome definition, we can characterize:

• Spacetime stabilizers: trivial faults with empty syndrome
• Logical faults: non-trivial faults with empty syndrome

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

A spacetime stabilizer has empty syndrome by definition

Equations

• IsSpacetimeStabilizer' DC baseOutcomes isTrivial fault = (hasEmptySyndrome' DC baseOutcomes fault ∧ isTrivial fault)

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

A logical fault is non-trivial with empty syndrome

Equations

• IsLogicalFault DC baseOutcomes isTrivial fault = (hasEmptySyndrome' DC baseOutcomes fault ∧ ¬isTrivial fault)

theorem emptySyndrome_dichotomy {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) (isTrivial : SpacetimeFault V E M → Prop) (fault : SpacetimeFault V E M) (h_empty : hasEmptySyndrome' DC baseOutcomes fault) : IsSpacetimeStabilizer' DC baseOutcomes isTrivial fault ∨ IsLogicalFault DC baseOutcomes isTrivial fault

Stabilizers and logical faults partition empty-syndrome faults

theorem stabilizer_logicalFault_exclusive {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) (isTrivial : SpacetimeFault V E M → Prop) (fault : SpacetimeFault V E M) : ¬(IsSpacetimeStabilizer' DC baseOutcomes isTrivial fault ∧ IsLogicalFault DC baseOutcomes isTrivial fault)

Stabilizers and logical faults are mutually exclusive

theorem isLogicalFault_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) (isTrivial : SpacetimeFault V E M → Prop) (fault : SpacetimeFault V E M) : IsLogicalFault DC baseOutcomes isTrivial fault ↔ hasEmptySyndrome' DC baseOutcomes fault ∧ ¬isTrivial fault

A logical fault is characterized as non-trivial with empty syndrome

Syndrome Membership Characterization

theorem mem_syndrome_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) (D : Detector V E M) (hD : D ∈ DC.detectors) : D ∈ syndrome DC baseOutcomes fault ↔ D.isViolated (applyFaultToOutcomes' baseOutcomes fault)

A detector is in the syndrome iff it is violated by the fault

theorem syndrome_subset {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) : syndrome DC baseOutcomes fault ⊆ DC.detectors

Syndrome is a subset of the detector collection

Summary

This formalization captures the syndrome concept from fault-tolerant quantum error correction:

1. Syndrome Definition: The syndrome of a fault F is the set of detectors violated by F. Equivalently, it's a binary vector where entry D is 1 iff detector D is violated.

2. Z₂-Linearity: Under appropriate conditions, the syndrome function satisfies:

   • syndrome(F₁ · F₂) = syndrome(F₁) + syndrome(F₂) (symmetric difference)
   • syndrome(F⁻¹) = syndrome(F)
   • syndrome(1) = ∅

3. Partition of Empty-Syndrome Faults:

   • Spacetime stabilizers: trivial faults with empty syndrome
   • Logical faults: non-trivial faults with empty syndrome
   • These are mutually exclusive and exhaustive

Key properties proven:

• Syndrome addition (symmetric difference) is commutative, associative, has identity
• Every syndrome is self-inverse
• Identity fault has empty syndrome
• Syndrome respects fault composition (Z₂-linear)
• Empty-syndrome faults partition into stabilizers and logical faults