Definition 9: Syndrome

Statement

The syndrome of a spacetime fault (Def 7) is the set of detectors (Def 8) that are violated by the fault. A detector is violated if the product of its measurement outcomes is −1 instead of the expected +1.

Equivalently, working over Z₂, if detectors are indexed as D₁, …, Dₘ, the syndrome can be identified with a binary vector s ∈ Z₂^m where sⱼ = 1 iff detector Dⱼ is violated.

Main Results

• syndromeFault: The syndrome of a spacetime fault as a finset of detector indices
• syndromeVec: The syndrome as a binary vector s ∈ (I → ZMod 2)
• mem_syndromeFault_iff: Detector i is in the syndrome iff it is violated by the fault
• syndromeVec_eq_one_iff: s(i) = 1 iff detector i is violated

Corollaries

• syndromeFault_empty: The syndrome is empty for the fault-free configuration
• syndromeVec_zero: The syndrome vector is zero for no faults
• syndromeFault_eq_syndrome: The spacetime syndrome reduces to the time-fault syndrome
• syndromeVec_sum: The sum of the syndrome vector counts violated detectors (mod 2)

Decidability of isViolated

instance Detector.decidableIsViolated {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (D : Detector M) (faults : Finset (TimeFault M)) : Decidable (D.isViolated faults)

Detector.isViolated is decidable because it reduces to equality in ZMod 2, which has DecidableEq.

Equations

• D.decidableIsViolated faults = inferInstanceAs (Decidable (D.observedParity faults = 1))

Syndrome of a Spacetime Fault

def syndromeFault {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) : Finset I

The syndrome of a spacetime fault F with respect to a collection of detectors: the finset of detector indices that are violated by F. Since detectors depend only on measurement outcomes (time-faults flip outcomes), the syndrome is determined by the time-fault component of F.

Equations

• syndromeFault detectors F = {i : I | (detectors i).isViolated F.timeFaults}

def syndromeVec {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) : I → ZMod 2

The syndrome as a binary vector: s(i) = 1 if detector i is violated, 0 otherwise. This is the Z₂^m representation from the paper.

Equations

• syndromeVec detectors F i = if (detectors i).isViolated F.timeFaults then 1 else 0

Membership and characterization

@[simp]

theorem mem_syndromeFault_iff {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) (i : I) : i ∈ syndromeFault detectors F ↔ (detectors i).isViolated F.timeFaults

A detector index is in the syndrome iff the detector is violated by the spacetime fault.

@[simp]

theorem syndromeVec_eq_one_iff {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) (i : I) : syndromeVec detectors F i = 1 ↔ (detectors i).isViolated F.timeFaults

The syndrome vector is 1 at index i iff detector i is violated.

@[simp]

theorem syndromeVec_eq_zero_iff {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) (i : I) : syndromeVec detectors F i = 0 ↔ ¬(detectors i).isViolated F.timeFaults

The syndrome vector is 0 at index i iff detector i is not violated.

Consistency with Def_8 syndrome

theorem syndromeFault_eq_syndrome {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) : syndromeFault detectors F = Detector.syndrome detectors F.timeFaults

The spacetime syndrome equals the Def_8 syndrome applied to the time-fault component. This captures the key fact that detectors depend only on measurement outcomes, so only time-faults affect the syndrome.

Empty fault syndrome

@[simp]

theorem syndromeFault_empty {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq Q] [DecidableEq T] [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] [DecidableEq (SpaceFault Q T)] (detectors : I → Detector M) : syndromeFault detectors SpacetimeFault.empty = ∅

The syndrome is empty for the fault-free spacetime configuration.

@[simp]

theorem syndromeVec_zero {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq Q] [DecidableEq T] [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] [DecidableEq (SpaceFault Q T)] (detectors : I → Detector M) : syndromeVec detectors SpacetimeFault.empty = 0

The syndrome vector is zero for the fault-free configuration.

Syndrome vector and finset correspondence

theorem syndromeFault_eq_support {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) : syndromeFault detectors F = {i : I | syndromeVec detectors F i = 1}

The syndrome finset is exactly the support of the syndrome vector.

theorem mem_syndromeFault_iff_vec {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) (i : I) : i ∈ syndromeFault detectors F ↔ syndromeVec detectors F i = 1

Membership in syndrome finset iff the syndrome vector entry is 1.

theorem not_mem_syndromeFault_iff_vec {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) (i : I) : i ∉ syndromeFault detectors F ↔ syndromeVec detectors F i = 0

Not in syndrome finset iff the syndrome vector entry is 0.

Space-faults do not affect the syndrome

theorem syndromeFault_depends_on_timeFaults {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F₁ F₂ : SpacetimeFault Q T M) (h : F₁.timeFaults = F₂.timeFaults) : syndromeFault detectors F₁ = syndromeFault detectors F₂

Space-faults do not affect the syndrome: two spacetime faults with the same time-faults produce the same syndrome. This formalizes the key insight that the syndrome depends only on measurement outcome flips (time-faults).

theorem syndromeVec_depends_on_timeFaults {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F₁ F₂ : SpacetimeFault Q T M) (h : F₁.timeFaults = F₂.timeFaults) : syndromeVec detectors F₁ = syndromeVec detectors F₂

The syndrome vector is the same for faults with identical time-fault components.

Syndrome of pure space-faults and pure time-faults

theorem syndromeFault_pureSpace {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq Q] [DecidableEq T] [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] [DecidableEq (SpaceFault Q T)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) (hpure : F.isPureSpace) : syndromeFault detectors F = ∅

A pure space-fault (no time-faults) has empty syndrome.

theorem syndromeVec_pureSpace {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq Q] [DecidableEq T] [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] [DecidableEq (SpaceFault Q T)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) (hpure : F.isPureSpace) : syndromeVec detectors F = 0

A pure space-fault has zero syndrome vector.

Syndrome cardinality

theorem syndromeFault_card {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) : (syndromeFault detectors F).card = {i : I | (detectors i).isViolated F.timeFaults}.card

The number of violated detectors equals the cardinality of the syndrome.

Syndrome sum (mod 2)

theorem syndromeVec_sum {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) : ∑ i : I, syndromeVec detectors F i = ↑(syndromeFault detectors F).card

The sum of the syndrome vector counts the number of violated detectors mod 2.

Syndrome determined by flip parity

theorem syndromeFault_eq_flipParity_filter {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) : syndromeFault detectors F = {i : I | (detectors i).flipParity F.timeFaults = 1}

The syndrome is equivalently described using flip parities of detectors.

theorem syndromeVec_eq_flipParity {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F : SpacetimeFault Q T M) (i : I) : syndromeVec detectors F i = (detectors i).flipParity F.timeFaults

The syndrome vector can be computed via flip parities.

Single fault syndrome

theorem syndromeFault_ofSpaceFault {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq Q] [DecidableEq T] [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] [DecidableEq (SpaceFault Q T)] (detectors : I → Detector M) (f : SpaceFault Q T) : syndromeFault detectors (SpacetimeFault.ofSpaceFault f) = ∅

A pure space-fault has empty syndrome: space-faults don't violate detectors.

theorem not_isViolated_disjoint {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (D : Detector M) (faults : Finset (TimeFault M)) (h : ∀ m ∈ D.measurements, { measurement := m } ∉ faults) : ¬D.isViolated faults

A detector not containing any faulted measurement is not violated.

Syndrome determines information about errors

theorem syndromeFault_eq_iff {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F₁ F₂ : SpacetimeFault Q T M) : syndromeFault detectors F₁ = syndromeFault detectors F₂ ↔ ∀ (i : I), (detectors i).isViolated F₁.timeFaults ↔ (detectors i).isViolated F₂.timeFaults

The syndrome captures the error information revealed by detectors: two faults produce the same syndrome iff they violate the same detectors.

theorem syndromeVec_eq_iff {Q : Type u_1} {T : Type u_2} {M : Type u_3} {I : Type u_4} [DecidableEq I] [Fintype I] [DecidableEq M] [DecidableEq (TimeFault M)] (detectors : I → Detector M) (F₁ F₂ : SpacetimeFault Q T M) : syndromeVec detectors F₁ = syndromeVec detectors F₂ ↔ syndromeFault detectors F₁ = syndromeFault detectors F₂

Two faults with the same syndrome have identical syndrome vectors.