Definition 8: Detectors

Statement

A detector is a collection of state initializations and measurements whose outcomes satisfy a deterministic constraint in the absence of faults (Definition 7).

A detector is specified by a set of measurement labels such that the product of all outcomes (in {+1, -1}) equals +1 when there are no faults. In ZMod 2 encoding (0 ↔ +1, 1 ↔ -1), this means the sum of ideal outcomes over the detector's measurements equals 0.

Main Results

• Detector: A detector on measurement type M with ideal outcomes
• Detector.detectorConstraint: The sum of ideal outcomes over detector measurements is 0
• Detector.isViolated: Whether a set of time-faults causes the detector to fire
• Detector.observedParity: The observed parity of detector measurements under faults
• repeatedMeasurementDetector: Two consecutive measurements of the same check form a detector
• initAndMeasureDetector: Initialization + later measurement forms a detector

Corollaries

• No-fault detectors have observed parity 0
• Violation depends only on which detector measurements are faulted
• Syndrome: the set of violated detectors

Detector Definition

structure Detector (M : Type u_4) : Type u_4

A detector is a finite collection of measurement labels together with ideal outcomes, such that the sum (in ZMod 2) of the ideal outcomes over the detector's measurements is 0. In {+1, -1} encoding, this means the product of ideal outcomes equals +1.

The type parameter M labels all measurements and state initializations in the procedure (per Definition 7, initializations are treated as measurements).

• measurements : Finset M

  The finset of measurement labels comprising this detector.

• idealOutcome : M → ZMod 2

  The ideal outcome of each measurement (0 ↔ +1, 1 ↔ -1 in ZMod 2).

• detectorConstraint : ∑ m ∈ self.measurements, self.idealOutcome m = 0

  The detector constraint: in the absence of faults, the sum of ideal outcomes over the detector's measurements is 0 in ZMod 2. Equivalently, the product of {+1, -1} outcomes equals +1.

Observed parity and violation

def Detector.observedParity {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (D : Detector M) (faults : Finset (TimeFault M)) : ZMod 2

The observed parity of a detector under a set of time-faults. This is the sum (in ZMod 2) of observed outcomes over the detector's measurements. In {+1, -1} encoding, 0 means the product is +1, 1 means the product is -1.

Equations

• D.observedParity faults = ∑ m ∈ D.measurements, observedOutcome D.idealOutcome faults m

def Detector.isViolated {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (D : Detector M) (faults : Finset (TimeFault M)) : Prop

A detector is violated by a set of time-faults if the observed parity is 1 (i.e., the product of observed outcomes is -1 instead of +1).

Equations

• D.isViolated faults = (D.observedParity faults = 1)

def Detector.flipParity {M : Type u_3} [DecidableEq (TimeFault M)] (D : Detector M) (faults : Finset (TimeFault M)) : ZMod 2

The flip parity: the sum in ZMod 2 of the indicator of faulted measurements in this detector. This equals the observed parity.

Equations

• D.flipParity faults = ∑ m ∈ D.measurements, if { measurement := m } ∈ faults then 1 else 0

Basic Properties

@[simp]

theorem Detector.observedParity_no_faults {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (D : Detector M) : D.observedParity ∅ = 0

In the absence of faults, the observed parity equals 0 (detector is not violated).

theorem Detector.not_isViolated_no_faults {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (D : Detector M) : ¬D.isViolated ∅

In the absence of faults, no detector is violated.

theorem Detector.observedParity_eq_flipParity {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (D : Detector M) (faults : Finset (TimeFault M)) : D.observedParity faults = D.flipParity faults

The observed parity equals the flip parity (number of faulted measurements mod 2). This is because the ideal outcomes cancel by the detector constraint.

theorem Detector.isViolated_iff_flipParity {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (D : Detector M) (faults : Finset (TimeFault M)) : D.isViolated faults ↔ D.flipParity faults = 1

A detector is violated iff the flip parity is 1.

@[simp]

theorem Detector.flipParity_no_faults {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (D : Detector M) : D.flipParity ∅ = 0

The flip parity with no faults is 0.

Violation depends only on fault-detector intersection

theorem Detector.isViolated_depends_on_intersection {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (D : Detector M) (faults₁ faults₂ : Finset (TimeFault M)) (h : ∀ m ∈ D.measurements, { measurement := m } ∈ faults₁ ↔ { measurement := m } ∈ faults₂) : D.isViolated faults₁ ↔ D.isViolated faults₂

The violation of a detector depends only on which of the detector's measurements appear in the fault set.

theorem Detector.isViolated_of_superset_disjoint {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (D : Detector M) (faults extra : Finset (TimeFault M)) (hdisj : ∀ m ∈ D.measurements, { measurement := m } ∉ extra) : D.isViolated (faults ∪ extra) ↔ D.isViolated faults

Violation is invariant if we add faults outside the detector.

Detector from a single measurement repeated twice

Example 1: Two consecutive measurements of the same stabilizer check s at times t and t+1 form a detector. If no faults occur, both give the same outcome, so their product is +1.

def repeatedMeasurementDetector {M : Type u_3} [DecidableEq M] (m₁ m₂ : M) (hne : m₁ ≠ m₂) (outcome : ZMod 2) : Detector M

A repeated measurement detector: measuring the same check at two different times. Both measurements have the same ideal outcome, so in ZMod 2 they sum to 0.

Equations

• repeatedMeasurementDetector m₁ m₂ hne outcome = { measurements := {m₁, m₂}, idealOutcome := fun (m : M) => if m = m₁ ∨ m = m₂ then outcome else 0, detectorConstraint := ⋯ }

def initAndMeasureDetector {M : Type u_3} [DecidableEq M] (m_init m_meas : M) (hne : m_init ≠ m_meas) (outcome : ZMod 2) : Detector M

An initialization-measurement detector: initializing a qubit and later measuring it in the same basis. Both give the same outcome (+1 for |0⟩ → Z-measurement), so the product is +1. The two labels m_init and m_meas represent the initialization (treated as a measurement per Def 7) and the actual measurement.

Equations

• initAndMeasureDetector m_init m_meas hne outcome = { measurements := {m_init, m_meas}, idealOutcome := fun (m : M) => if m = m_init ∨ m = m_meas then outcome else 0, detectorConstraint := ⋯ }

Properties of example detectors

theorem Detector.repeatedMeasurement_violated_iff {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (m₁ m₂ : M) (hne : m₁ ≠ m₂) (outcome : ZMod 2) (faults : Finset (TimeFault M)) : (repeatedMeasurementDetector m₁ m₂ hne outcome).isViolated faults ↔ Xor' ({ measurement := m₁ } ∈ faults) ({ measurement := m₂ } ∈ faults)

A repeated measurement detector is violated iff exactly one of the two measurements is faulted (i.e., the two outcomes disagree).

Syndrome: the set of violated detectors

def Detector.syndrome {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] {I : Type u_4} [DecidableEq I] [Fintype I] (detectors : I → Detector M) (faults : Finset (TimeFault M)) : Finset I

The syndrome of a set of time-faults with respect to a collection of detectors: the set of detector indices that are violated.

Equations

• Detector.syndrome detectors faults = {i : I | (detectors i).observedParity faults = 1}

@[simp]

theorem Detector.mem_syndrome_iff {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] {I : Type u_4} [DecidableEq I] [Fintype I] (detectors : I → Detector M) (faults : Finset (TimeFault M)) (i : I) : i ∈ syndrome detectors faults ↔ (detectors i).isViolated faults

A detector index is in the syndrome iff the detector is violated.

@[simp]

theorem Detector.syndrome_empty_no_faults {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] {I : Type u_4} [DecidableEq I] [Fintype I] (detectors : I → Detector M) : syndrome detectors ∅ = ∅

The syndrome is empty when there are no faults.

Disjoint union of detectors

def Detector.disjointUnion {M : Type u_3} [DecidableEq M] (D₁ D₂ : Detector M) (hdisj : Disjoint D₁.measurements D₂.measurements) (hsame : ∀ (m : M), D₁.idealOutcome m = D₂.idealOutcome m) : Detector M

The union of two detectors with disjoint measurement sets forms a new detector, provided the ideal outcomes agree on any common measurements.

Equations

• D₁.disjointUnion D₂ hdisj hsame = { measurements := D₁.measurements ∪ D₂.measurements, idealOutcome := D₁.idealOutcome, detectorConstraint := ⋯ }

Empty and single-measurement detectors

def Detector.emptyDetector {M : Type u_3} (idealOutcome : M → ZMod 2) : Detector M

The empty detector (no measurements) is trivially satisfied.

Equations

• Detector.emptyDetector idealOutcome = { measurements := ∅, idealOutcome := idealOutcome, detectorConstraint := Detector.emptyDetector._proof_1 }

@[simp]

theorem Detector.emptyDetector_not_violated {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (idealOutcome : M → ZMod 2) (faults : Finset (TimeFault M)) : ¬(emptyDetector idealOutcome).isViolated faults

The empty detector is never violated.

def Detector.singleMeasurementDetector {M : Type u_3} (m : M) : Detector M

A single-measurement detector requires the ideal outcome to be 0 (i.e., the measurement gives +1 in the absence of faults).

Equations

• Detector.singleMeasurementDetector m = { measurements := {m}, idealOutcome := fun (x : M) => 0, detectorConstraint := ⋯ }

theorem Detector.singleMeasurement_violated_iff {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (m : M) (faults : Finset (TimeFault M)) : (singleMeasurementDetector m).isViolated faults ↔ { measurement := m } ∈ faults

A single-measurement detector with outcome 0 is violated iff the measurement is faulted.

Detector violation from spacetime faults

theorem Detector.isViolated_spacetimeFault {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] [DecidableEq Q] [DecidableEq T] [DecidableEq (SpaceFault Q T)] (D : Detector M) (F : SpacetimeFault Q T M) : D.isViolated F.timeFaults ↔ D.observedParity F.timeFaults = 1

The violation status of a detector under a spacetime fault is determined by the time-fault component. Space-faults change the quantum state but the detector constraint is purely about measurement outcome flips.

Detector weight

def Detector.detectorWeight {M : Type u_3} (D : Detector M) : ℕ

The weight (number of measurements) in a detector.

Equations

• D.detectorWeight = D.measurements.card

theorem Detector.repeatedMeasurement_weight {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (m₁ m₂ : M) (hne : m₁ ≠ m₂) (outcome : ZMod 2) : (repeatedMeasurementDetector m₁ m₂ hne outcome).detectorWeight = 2

The repeated measurement detector has weight 2.

theorem Detector.initAndMeasure_weight {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (m_init m_meas : M) (hne : m_init ≠ m_meas) (outcome : ZMod 2) : (initAndMeasureDetector m_init m_meas hne outcome).detectorWeight = 2

The init-and-measure detector has weight 2.

@[simp]

theorem Detector.emptyDetector_weight {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (idealOutcome : M → ZMod 2) : (emptyDetector idealOutcome).detectorWeight = 0

The empty detector has weight 0.

theorem Detector.singleMeasurement_weight {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (m : M) : (singleMeasurementDetector m).detectorWeight = 1

The single-measurement detector has weight 1.