Def_8: Detector

Statement

A detector is a collection of state initializations and measurement events that yield a deterministic result in the absence of faults. Specifically, a detector is a subset D of initialization events and measurement events such that:

1. In a fault-free execution, the product of all measurement outcomes in D (treating +1 outcomes as 0 and −1 outcomes as 1 modulo 2) combined with initialization parities equals a fixed value (conventionally +1 or equivalently 0 mod 2).

2. This determinism holds regardless of the quantum state being processed (for measurements of stabilizer generators) or is guaranteed by the initialization (for measurements immediately following initialization).

Intuitively, a detector is a parity check on measurement outcomes that should always yield +1 if no errors occurred. A fault that causes a detector to report −1 instead is said to violate that detector.

Main Definitions

• MeasurementOutcome : The outcome of a quantum measurement (+1 or -1, represented as ZMod 2)
• InitializationEvent : A state initialization event (qubit and time)
• MeasurementEvent : A measurement event (measurement index and time)
• DetectorEvent : Either an initialization or measurement event
• Detector : A set of events with deterministic fault-free parity
• Detector.expectedParity : The expected parity (0 for +1 outcome, 1 for -1)
• Detector.observedParity : The observed parity given measurement outcomes
• Detector.isViolated : Whether a detector reports an unexpected value

Key Properties

• Detector.satisfied_or_violated : A detector is either satisfied or violated
• Detector.satisfied_iff_not_violated : A detector is satisfied iff not violated
• Detector.empty_isSatisfied : Empty detector always has parity 0

Measurement Outcomes

Measurement outcomes in quantum mechanics are typically ±1 eigenvalues. We represent these mod 2: +1 → 0, -1 → 1. This convention means XOR (addition mod 2) computes product parity correctly:

• +1 × +1 = +1 → 0 + 0 = 0
• +1 × -1 = -1 → 0 + 1 = 1
• -1 × +1 = -1 → 1 + 0 = 1
• -1 × -1 = +1 → 1 + 1 = 0

@[reducible, inline]

abbrev MeasurementOutcome : Type

A measurement outcome represented mod 2: 0 for +1, 1 for -1

Equations

• MeasurementOutcome = ZMod 2

def MeasurementOutcome.plusOne : MeasurementOutcome

The +1 outcome (no error detected)

Equations

• MeasurementOutcome.plusOne = 0

def MeasurementOutcome.minusOne : MeasurementOutcome

The -1 outcome (error detected)

Equations

• MeasurementOutcome.minusOne = 1

@[simp]

theorem MeasurementOutcome.plusOne_val : plusOne = 0

@[simp]

theorem MeasurementOutcome.minusOne_val : minusOne = 1

def MeasurementOutcome.fromBool : Bool → MeasurementOutcome

Convert from Bool: false → +1 (0), true → -1 (1)

Equations

• MeasurementOutcome.fromBool false = MeasurementOutcome.plusOne
• MeasurementOutcome.fromBool true = MeasurementOutcome.minusOne

def MeasurementOutcome.toBool (m : MeasurementOutcome) : Bool

Convert to Bool: 0 → false (+1), 1 → true (-1)

Equations

• m.toBool = decide (m ≠ 0)

@[simp]

theorem MeasurementOutcome.fromBool_false : fromBool false = plusOne

@[simp]

theorem MeasurementOutcome.fromBool_true : fromBool true = minusOne

@[simp]

theorem MeasurementOutcome.toBool_plusOne : plusOne.toBool = false

@[simp]

theorem MeasurementOutcome.toBool_minusOne : minusOne.toBool = true

def MeasurementOutcome.product (m₁ m₂ : MeasurementOutcome) : MeasurementOutcome

Product of outcomes is addition mod 2

Equations

• m₁.product m₂ = m₁ + m₂

@[simp]

theorem MeasurementOutcome.product_plusOne_plusOne : plusOne.product plusOne = plusOne

@[simp]

theorem MeasurementOutcome.product_plusOne_minusOne : plusOne.product minusOne = minusOne

@[simp]

theorem MeasurementOutcome.product_minusOne_plusOne : minusOne.product plusOne = minusOne

@[simp]

theorem MeasurementOutcome.product_minusOne_minusOne : minusOne.product minusOne = plusOne

Events: Initialization and Measurement

A detector monitors both initialization events (where qubits are prepared in known states) and measurement events (where observables are measured).

structure InitializationEvent (V : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

An initialization event: preparing a qubit at a specific time

• qubit : QubitLoc V E

  The qubit being initialized

• time : TimeStep

  The time of initialization

• expectedParity : ZMod 2

  The expected parity of this initialization (0 for standard basis state)

instance instDecidableEqInitializationEvent {V✝ : Type u_1} {E✝ : Type u_2} [DecidableEq V✝] [DecidableEq E✝] : DecidableEq (InitializationEvent V✝ E✝)

Equations

• instDecidableEqInitializationEvent = instDecidableEqInitializationEvent.decEq

def instDecidableEqInitializationEvent.decEq {V✝ : Type u_1} {E✝ : Type u_2} [DecidableEq V✝] [DecidableEq E✝] (x✝ x✝¹ : InitializationEvent V✝ E✝) : Decidable (x✝ = x✝¹)

Equations

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

structure MeasurementEvent (M : Type u_1) : Type u_1

A measurement event: measuring an observable at a specific time

• measurement : M

  The measurement index (which check/observable is measured)

• time : TimeStep

  The time of measurement

instance instDecidableEqMeasurementEvent {M✝ : Type u_1} [DecidableEq M✝] : DecidableEq (MeasurementEvent M✝)

Equations

• instDecidableEqMeasurementEvent = instDecidableEqMeasurementEvent.decEq

def instDecidableEqMeasurementEvent.decEq {M✝ : Type u_1} [DecidableEq M✝] (x✝ x✝¹ : MeasurementEvent M✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqMeasurementEvent.decEq { measurement := a, time := a_1 } { measurement := b, time := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def InitializationEvent.standard {V : Type u_1} {E : Type u_2} (q : QubitLoc V E) (t : TimeStep) : InitializationEvent V E

Create an initialization event with +1 expected outcome

Equations

• InitializationEvent.standard q t = { qubit := q, time := t, expectedParity := 0 }

@[simp]

theorem InitializationEvent.standard_qubit {V : Type u_1} {E : Type u_2} (q : QubitLoc V E) (t : TimeStep) : (standard q t).qubit = q

@[simp]

theorem InitializationEvent.standard_time {V : Type u_1} {E : Type u_2} (q : QubitLoc V E) (t : TimeStep) : (standard q t).time = t

@[simp]

theorem InitializationEvent.standard_expectedParity {V : Type u_1} {E : Type u_2} (q : QubitLoc V E) (t : TimeStep) : (standard q t).expectedParity = 0

@[simp]

theorem MeasurementEvent.measurement_accessor {M : Type u_1} (m : M) (t : TimeStep) : { measurement := m, time := t }.measurement = m

Get the time of a measurement event

@[simp]

theorem MeasurementEvent.time_accessor {M : Type u_1} (m : M) (t : TimeStep) : { measurement := m, time := t }.time = t

Detector Events

A detector event is either an initialization or a measurement.

inductive DetectorEvent (V : Type u_1) (E : Type u_2) (M : Type u_3) : Type (max (max u_1 u_2) u_3)

A detector event: either an initialization or a measurement

• init {V : Type u_1} {E : Type u_2} {M : Type u_3} : InitializationEvent V E → DetectorEvent V E M

  An initialization event

• meas {V : Type u_1} {E : Type u_2} {M : Type u_3} : MeasurementEvent M → DetectorEvent V E M

  A measurement event

instance instDecidableEqDetectorEvent {V✝ : Type u_1} {E✝ : Type u_2} {M✝ : Type u_3} [DecidableEq V✝] [DecidableEq E✝] [DecidableEq M✝] : DecidableEq (DetectorEvent V✝ E✝ M✝)

Equations

• instDecidableEqDetectorEvent = instDecidableEqDetectorEvent.decEq

def instDecidableEqDetectorEvent.decEq {V✝ : Type u_1} {E✝ : Type u_2} {M✝ : Type u_3} [DecidableEq V✝] [DecidableEq E✝] [DecidableEq M✝] (x✝ x✝¹ : DetectorEvent V✝ E✝ M✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqDetectorEvent.decEq (DetectorEvent.init a) (DetectorEvent.init b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqDetectorEvent.decEq (DetectorEvent.init a) (DetectorEvent.meas a_1) = isFalse ⋯
• instDecidableEqDetectorEvent.decEq (DetectorEvent.meas a) (DetectorEvent.init a_1) = isFalse ⋯
• instDecidableEqDetectorEvent.decEq (DetectorEvent.meas a) (DetectorEvent.meas b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def DetectorEvent.isInit {V : Type u_1} {E : Type u_2} {M : Type u_3} : DetectorEvent V E M → Bool

Check if this is an initialization event

Equations

• (DetectorEvent.init a).isInit = true
• (DetectorEvent.meas a).isInit = false

def DetectorEvent.isMeas {V : Type u_1} {E : Type u_2} {M : Type u_3} : DetectorEvent V E M → Bool

Check if this is a measurement event

Equations

• (DetectorEvent.init a).isMeas = false
• (DetectorEvent.meas a).isMeas = true

@[simp]

theorem DetectorEvent.isInit_init {V : Type u_1} {E : Type u_2} {M : Type u_3} (e : InitializationEvent V E) : (init e).isInit = true

@[simp]

theorem DetectorEvent.isInit_meas {V : Type u_1} {E : Type u_2} {M : Type u_3} (e : MeasurementEvent M) : (meas e).isInit = false

@[simp]

theorem DetectorEvent.isMeas_init {V : Type u_1} {E : Type u_2} {M : Type u_3} (e : InitializationEvent V E) : (init e).isMeas = false

@[simp]

theorem DetectorEvent.isMeas_meas {V : Type u_1} {E : Type u_2} {M : Type u_3} (e : MeasurementEvent M) : (meas e).isMeas = true

def DetectorEvent.time {V : Type u_1} {E : Type u_2} {M : Type u_3} : DetectorEvent V E M → TimeStep

Get the time of a detector event

Equations

• (DetectorEvent.init a).time = a.time
• (DetectorEvent.meas a).time = a.time

@[simp]

theorem DetectorEvent.time_init {V : Type u_1} {E : Type u_2} {M : Type u_3} (e : InitializationEvent V E) : (init e).time = e.time

@[simp]

theorem DetectorEvent.time_meas {V : Type u_1} {E : Type u_2} {M : Type u_3} (e : MeasurementEvent M) : (meas e).time = e.time

def DetectorEvent.getInit {V : Type u_1} {E : Type u_2} {M : Type u_3} : DetectorEvent V E M → Option (InitializationEvent V E)

Get the initialization event if this is one

Equations

• (DetectorEvent.init a).getInit = some a
• (DetectorEvent.meas a).getInit = none

def DetectorEvent.getMeas {V : Type u_1} {E : Type u_2} {M : Type u_3} : DetectorEvent V E M → Option (MeasurementEvent M)

Get the measurement event if this is one

Equations

• (DetectorEvent.init a).getMeas = none
• (DetectorEvent.meas a).getMeas = some a

theorem DetectorEvent.getInit_injective {V : Type u_1} {E : Type u_2} {M : Type u_3} (a b : DetectorEvent V E M) : a.getInit.isSome = true → b.getInit.isSome = true → a.getInit = b.getInit → a = b

getInit is injective on init events

theorem DetectorEvent.getMeas_injective {V : Type u_1} {E : Type u_2} {M : Type u_3} (a b : DetectorEvent V E M) : a.getMeas.isSome = true → b.getMeas.isSome = true → a.getMeas = b.getMeas → a = b

getMeas is injective on meas events

Detectors

A detector is a set of events that together form a parity check with deterministic outcome in fault-free execution.

@[reducible, inline]

abbrev OutcomeAssignment (M : Type u_1) : Type u_1

An outcome assignment: provides measurement outcomes for all measurements at all times

Equations

• OutcomeAssignment M = (M → TimeStep → MeasurementOutcome)

@[reducible, inline]

abbrev InitFaultRecord (V : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

An initialization fault record: whether each initialization is faulty

Equations

• InitFaultRecord V E = (QubitLoc V E → TimeStep → Bool)

structure Detector (V : Type u_1) (E : Type u_2) (M : Type u_3) [DecidableEq V] [DecidableEq E] [DecidableEq M] : Type (max (max u_1 u_2) u_3)

A detector: a set of events with an expected fault-free parity.

The key property is that in fault-free execution, the XOR of all measurement outcomes in the detector (combined with initialization parities) equals the expected value. When faults occur, the observed parity may differ from expected.

• events : Finset (DetectorEvent V E M)

  The set of events in this detector

• expectedParity : ZMod 2

  The expected parity in fault-free execution (0 for +1, 1 for -1)

instance instDecidableEqDetector {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] : DecidableEq (Detector V E M)

Equations

• instDecidableEqDetector d1 d2 = if h : d1.events = d2.events ∧ d1.expectedParity = d2.expectedParity then isTrue ⋯ else isFalse ⋯

def Detector.initEvents {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) : Finset (InitializationEvent V E)

Get all initialization events in a detector

Equations

• D.initEvents = Finset.filterMap DetectorEvent.getInit D.events ⋯

def Detector.measEvents {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) : Finset (MeasurementEvent M)

Get all measurement events in a detector

Equations

• D.measEvents = Finset.filterMap DetectorEvent.getMeas D.events ⋯

def Detector.initParity {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) : ZMod 2

The contribution from initialization events: sum of their expected parities

Equations

• D.initParity = ∑ e ∈ D.initEvents, e.expectedParity

def Detector.observedParity {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) (outcomes : OutcomeAssignment M) : ZMod 2

The observed parity: sum of measurement outcomes plus initialization parities

Equations

• D.observedParity outcomes = D.initParity + ∑ e ∈ D.measEvents, outcomes e.measurement e.time

def Detector.isViolated {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) (outcomes : OutcomeAssignment M) : Prop

A detector is violated if observed parity differs from expected

Equations

• D.isViolated outcomes = (D.observedParity outcomes ≠ D.expectedParity)

def Detector.isSatisfied {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) (outcomes : OutcomeAssignment M) : Prop

A detector is satisfied if observed parity equals expected

Equations

• D.isSatisfied outcomes = (D.observedParity outcomes = D.expectedParity)

instance Detector.decIsViolated {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) (outcomes : OutcomeAssignment M) : Decidable (D.isViolated outcomes)

Equations

• D.decIsViolated outcomes = inferInstanceAs (Decidable (D.observedParity outcomes ≠ D.expectedParity))

instance Detector.decIsSatisfied {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) (outcomes : OutcomeAssignment M) : Decidable (D.isSatisfied outcomes)

Equations

• D.decIsSatisfied outcomes = inferInstanceAs (Decidable (D.observedParity outcomes = D.expectedParity))

theorem Detector.satisfied_or_violated {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) (outcomes : OutcomeAssignment M) : D.isSatisfied outcomes ∨ D.isViolated outcomes

A detector is either satisfied or violated

theorem Detector.satisfied_iff_not_violated {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) (outcomes : OutcomeAssignment M) : D.isSatisfied outcomes ↔ ¬D.isViolated outcomes

Satisfied and violated are mutually exclusive

Empty Detector

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

The empty detector with expected parity 0

Equations

• Detector.empty = { events := ∅, expectedParity := 0 }

@[simp]

theorem Detector.empty_events {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] : empty.events = ∅

@[simp]

theorem Detector.empty_expectedParity {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] : empty.expectedParity = 0

@[simp]

theorem Detector.empty_initEvents {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] : empty.initEvents = ∅

@[simp]

theorem Detector.empty_measEvents {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] : empty.measEvents = ∅

@[simp]

theorem Detector.empty_initParity {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] : empty.initParity = 0

@[simp]

theorem Detector.empty_observedParity {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (outcomes : OutcomeAssignment M) : empty.observedParity outcomes = 0

@[simp]

theorem Detector.empty_isSatisfied {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (outcomes : OutcomeAssignment M) : empty.isSatisfied outcomes

The empty detector is always satisfied

@[simp]

theorem Detector.empty_not_isViolated {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (outcomes : OutcomeAssignment M) : ¬empty.isViolated outcomes

The empty detector is never violated

Single-Event Detectors

def Detector.singleInit {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (e : InitializationEvent V E) : Detector V E M

A detector consisting of a single initialization event

Equations

• Detector.singleInit e = { events := {DetectorEvent.init e}, expectedParity := e.expectedParity }

def Detector.singleMeas {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (e : MeasurementEvent M) (expectedOutcome : ZMod 2 := 0) : Detector V E M

A detector consisting of a single measurement event

Equations

• Detector.singleMeas e expectedOutcome = { events := {DetectorEvent.meas e}, expectedParity := expectedOutcome }

@[simp]

theorem Detector.singleInit_events {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (e : InitializationEvent V E) : (singleInit e).events = {DetectorEvent.init e}

@[simp]

theorem Detector.singleMeas_events {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (e : MeasurementEvent M) (p : ZMod 2) : (singleMeas e p).events = {DetectorEvent.meas e}

Combining Detectors

def Detector.combine {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D₁ D₂ : Detector V E M) : Detector V E M

Combine two detectors by taking symmetric difference of events and XOR of parities. This corresponds to multiplying the parity checks.

Equations

• D₁.combine D₂ = { events := symmDiff D₁.events D₂.events, expectedParity := D₁.expectedParity + D₂.expectedParity }

instance Detector.instAdd {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] : Add (Detector V E M)

Notation for detector combination

Equations

• Detector.instAdd = { add := Detector.combine }

@[simp]

theorem Detector.combine_events {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D₁ D₂ : Detector V E M) : (D₁.combine D₂).events = symmDiff D₁.events D₂.events

@[simp]

theorem Detector.combine_expectedParity {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D₁ D₂ : Detector V E M) : (D₁.combine D₂).expectedParity = D₁.expectedParity + D₂.expectedParity

theorem Detector.ext_iff {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] {D₁ D₂ : Detector V E M} : D₁ = D₂ ↔ D₁.events = D₂.events ∧ D₁.expectedParity = D₂.expectedParity

Two detectors are equal iff their components are equal

theorem Detector.empty_combine {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) : empty.combine D = D

Adding empty detector does nothing (from the left)

theorem Detector.combine_empty {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) : D.combine empty = D

Adding empty detector does nothing (from the right)

theorem Detector.combine_self {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) : D.combine D = empty

Combining a detector with itself gives empty

Fault-Free Execution

The key property of detectors is determinism in fault-free execution.

def Detector.faultFreeOutcomes {M : Type u_3} (expectedMeasOutcome : M → TimeStep → ZMod 2) : OutcomeAssignment M

Fault-free outcomes: all measurements return their expected values. For stabilizer measurements, this means +1 (represented as 0). This function represents the outcomes in an ideal fault-free execution.

Equations

• Detector.faultFreeOutcomes expectedMeasOutcome = expectedMeasOutcome

theorem Detector.faultFree_isSatisfied {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) (expectedMeasOutcome : M → TimeStep → ZMod 2) (h_consistent : D.initParity + ∑ e ∈ D.measEvents, expectedMeasOutcome e.measurement e.time = D.expectedParity) : D.isSatisfied (faultFreeOutcomes expectedMeasOutcome)

A detector with consistent expected outcomes is satisfied in fault-free execution. This captures the defining property of detectors: determinism without faults.

Effect of Faults on Detectors

Faults can flip measurement outcomes, causing detectors to be violated.

def Detector.applyTimeFault {M : Type u_3} [DecidableEq M] (outcomes : OutcomeAssignment M) (f : TimeFault M) : OutcomeAssignment M

Apply a time fault to outcomes: if the fault is active, flip the outcome

Equations

• Detector.applyTimeFault outcomes f m t = if m = f.measurement ∧ t = f.time ∧ f.isFlipped = true then outcomes m t + 1 else outcomes m t

theorem Detector.applyTimeFault_flips {M : Type u_3} [DecidableEq M] (outcomes : OutcomeAssignment M) (f : TimeFault M) (e : MeasurementEvent M) (hf : f.isFlipped = true) (he : e.measurement = f.measurement) (ht : e.time = f.time) : applyTimeFault outcomes f e.measurement e.time = outcomes e.measurement e.time + 1

A single time fault at a measurement in the detector flips its contribution

theorem Detector.applyTimeFault_unchanged {M : Type u_3} [DecidableEq M] (outcomes : OutcomeAssignment M) (f : TimeFault M) (m : M) (t : TimeStep) (h : m ≠ f.measurement ∨ t ≠ f.time) : applyTimeFault outcomes f m t = outcomes m t

A time fault outside the detector doesn't affect outcomes for events not at that location

Detector Violation Analysis

We characterize when faults violate detectors.

def Detector.faultSyndrome {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) (faultedMeas : Finset (MeasurementEvent M)) : ZMod 2

The syndrome of a fault on a detector: how much the parity is shifted

Equations

• D.faultSyndrome faultedMeas = ↑(D.measEvents ∩ faultedMeas).card

theorem Detector.isViolated_iff_odd_syndrome {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (D : Detector V E M) (outcomes : OutcomeAssignment M) (faultedMeas : Finset (MeasurementEvent M)) (h_outcomes : ∀ e ∈ D.measEvents, e ∈ faultedMeas → outcomes e.measurement e.time = 1) (h_no_fault : ∀ e ∈ D.measEvents, e ∉ faultedMeas → outcomes e.measurement e.time = 0) (h_init : D.initParity = 0) (h_expected : D.expectedParity = 0) : D.isViolated outcomes ↔ D.faultSyndrome faultedMeas = 1

A fault violates a detector iff the syndrome is odd (1 mod 2)

Detector Collection

A fault-tolerant procedure typically has multiple detectors.

structure DetectorCollection (V : Type u_1) (E : Type u_2) (M : Type u_3) [DecidableEq V] [DecidableEq E] [DecidableEq M] : Type (max (max u_1 u_2) u_3)

A detector collection: a set of detectors for a fault-tolerant procedure

• detectors : Finset (Detector V E M)

  The set of detectors

def DetectorCollection.syndrome {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (DC : DetectorCollection V E M) (outcomes : OutcomeAssignment M) : Finset (Detector V E M)

The syndrome: which detectors are violated by given outcomes

Equations

• DC.syndrome outcomes = {D ∈ DC.detectors | D.isViolated outcomes}

def DetectorCollection.violatedCount {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (DC : DetectorCollection V E M) (outcomes : OutcomeAssignment M) : ℕ

Count of violated detectors

Equations

• DC.violatedCount outcomes = (DC.syndrome outcomes).card

def DetectorCollection.allSatisfied {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (DC : DetectorCollection V E M) (outcomes : OutcomeAssignment M) : Prop

All detectors are satisfied (syndrome is empty)

Equations

• DC.allSatisfied outcomes = (DC.syndrome outcomes = ∅)

@[simp]

theorem DetectorCollection.allSatisfied_iff {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (DC : DetectorCollection V E M) (outcomes : OutcomeAssignment M) : DC.allSatisfied outcomes ↔ ∀ D ∈ DC.detectors, D.isSatisfied outcomes

@[simp]

theorem DetectorCollection.empty_allSatisfied {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (outcomes : OutcomeAssignment M) : { detectors := ∅ }.allSatisfied outcomes

Empty collection has all detectors satisfied

Summary

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

1. Measurement Outcomes: Represented mod 2 (0 for +1, 1 for -1), with XOR computing product parity.

2. Events: Either initialization events (preparing qubits) or measurement events (measuring observables).

3. Detectors: Sets of events with an expected fault-free parity. The key property is that in fault-free execution, the XOR of all measurement outcomes (plus initialization parities) equals the expected value.

4. Violation: A detector is violated when the observed parity differs from expected. This indicates that a fault has occurred.

5. Fault Analysis: The syndrome of a fault on a detector counts (mod 2) how many faulted measurements are in the detector. A detector is violated iff this count is odd.

Key properties proven:

• Detectors are either satisfied or violated (exclusive)
• Empty detector is always satisfied
• Combining detectors XORs their events and parities
• Self-combination gives the empty detector
• Fault-free execution satisfies consistent detectors
• Violation occurs iff the fault syndrome is odd