Definition 7: Space and Time Faults

Statement

In the context of fault-tolerant quantum error correction:

1. A space-fault (or space error) is a Pauli error operator that occurs on some qubit at a specific time during the procedure.

2. A time-fault (or measurement error) is an error where the result of a measurement is reported incorrectly (i.e., +1 is reported as -1 or vice versa).

3. A spacetime fault is a collection of space-faults and time-faults occurring at various locations and times during the procedure.

Convention: State mis-initialization faults are treated as time-faults that are equivalent to a perfect initialization followed by a space-fault.

Main Results

• SpaceFault: A Pauli error on a specific qubit at a specific time
• TimeFault: A measurement error (bit-flip of outcome) at a specific measurement location
• SpacetimeFault: A collection of space-faults and time-faults
• SpacetimeFault.weight: The total number of individual faults
• SpacetimeFault.empty: The fault-free configuration
• SpacetimeFault.compose: Composition (symmetric difference) of faults

Corollaries

• Weight properties: empty has weight 0, single faults have weight 1
• Composition is commutative and involutive
• Space-only and time-only fault embeddings

Space Faults

structure SpaceFault (Q : Type u_4) (T : Type u_5) : Type (max u_4 u_5)

A space-fault (space error) is a single-qubit Pauli error at a specific qubit and time. The error is described by which qubit is affected, when it occurs, and what Pauli error is applied (X, Y, or Z, encoded as a nonzero element of ZMod 2 x ZMod 2 for the x and z components).

• qubit : Q

  The qubit where the error occurs.

• time : T

  The time at which the error occurs.

• xComponent : ZMod 2

  The X-component of the Pauli error (1 if X or Y, 0 otherwise).

• zComponent : ZMod 2

  The Z-component of the Pauli error (1 if Z or Y, 0 otherwise).

• nontrivial : self.xComponent ≠ 0 ∨ self.zComponent ≠ 0

  The error is nontrivial: at least one component is nonzero.

Time Faults

structure TimeFault (M : Type u_4) : Type u_4

A time-fault (measurement error) is a single measurement whose outcome is reported incorrectly. In ZMod 2 encoding (0 -> +1, 1 -> -1), this corresponds to flipping the measurement outcome bit. The fault is identified by which measurement is affected.

Convention: State mis-initialization faults are also modeled as time-faults. For example, initializing |0> but getting |1> is equivalent to a perfect initialization followed by an X error. The initialization measurement (projecting onto |0>) is treated as a measurement that reported incorrectly.

• measurement : M

  The measurement whose outcome is flipped.

Spacetime Faults

structure SpacetimeFault (Q : Type u_4) (T : Type u_5) (M : Type u_6) : Type (max (max u_4 u_5) u_6)

A spacetime fault is a collection of space-faults and time-faults occurring at various locations and times during the procedure. We represent it as a pair of finsets: one of space-faults and one of time-faults.

The weight of a spacetime fault is the total number of individual faults (each single-qubit Pauli error counts as 1, each measurement error counts as 1).

• spaceFaults : Finset (SpaceFault Q T)

  The collection of space-faults (Pauli errors on qubits at specific times).

• timeFaults : Finset (TimeFault M)

  The collection of time-faults (measurement errors).

theorem SpacetimeFault.ext {Q : Type u_4} {T : Type u_5} {M : Type u_6} {x y : SpacetimeFault Q T M} (spaceFaults : x.spaceFaults = y.spaceFaults) (timeFaults : x.timeFaults = y.timeFaults) : x = y

theorem SpacetimeFault.ext_iff {Q : Type u_4} {T : Type u_5} {M : Type u_6} {x y : SpacetimeFault Q T M} : x = y ↔ x.spaceFaults = y.spaceFaults ∧ x.timeFaults = y.timeFaults

def SpacetimeFault.weight {Q : Type u_1} {T : Type u_2} {M : Type u_3} (F : SpacetimeFault Q T M) : ℕ

The weight of a spacetime fault: total number of individual faults.

Equations

• F.weight = F.spaceFaults.card + F.timeFaults.card

def SpacetimeFault.empty {Q : Type u_1} {T : Type u_2} {M : Type u_3} : SpacetimeFault Q T M

The empty spacetime fault: no errors at all.

Equations

• SpacetimeFault.empty = { spaceFaults := ∅, timeFaults := ∅ }

def SpacetimeFault.ofSpaceFault {Q : Type u_1} {T : Type u_2} {M : Type u_3} (f : SpaceFault Q T) : SpacetimeFault Q T M

A spacetime fault consisting of a single space-fault.

Equations

• SpacetimeFault.ofSpaceFault f = { spaceFaults := {f}, timeFaults := ∅ }

def SpacetimeFault.ofTimeFault {Q : Type u_1} {T : Type u_2} {M : Type u_3} (f : TimeFault M) : SpacetimeFault Q T M

A spacetime fault consisting of a single time-fault.

Equations

• SpacetimeFault.ofTimeFault f = { spaceFaults := ∅, timeFaults := {f} }

def SpacetimeFault.compose {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F₁ F₂ : SpacetimeFault Q T M) : SpacetimeFault Q T M

Composition of spacetime faults via symmetric difference. Applying the same error twice cancels it; flipping an outcome twice restores it.

Equations

• F₁.compose F₂ = { spaceFaults := symmDiff F₁.spaceFaults F₂.spaceFaults, timeFaults := symmDiff F₁.timeFaults F₂.timeFaults }

def SpacetimeFault.isPureSpace {Q : Type u_1} {T : Type u_2} {M : Type u_3} (F : SpacetimeFault Q T M) : Prop

A spacetime fault is pure-space if it has no time-faults.

Equations

• F.isPureSpace = (F.timeFaults = ∅)

def SpacetimeFault.isPureTime {Q : Type u_1} {T : Type u_2} {M : Type u_3} (F : SpacetimeFault Q T M) : Prop

A spacetime fault is pure-time if it has no space-faults.

Equations

• F.isPureTime = (F.spaceFaults = ∅)

def SpacetimeFault.spaceWeight {Q : Type u_1} {T : Type u_2} {M : Type u_3} (F : SpacetimeFault Q T M) : ℕ

The number of space-faults in the spacetime fault.

Equations

• F.spaceWeight = F.spaceFaults.card

def SpacetimeFault.timeWeight {Q : Type u_1} {T : Type u_2} {M : Type u_3} (F : SpacetimeFault Q T M) : ℕ

The number of time-faults in the spacetime fault.

Equations

• F.timeWeight = F.timeFaults.card

Basic Properties

@[simp]

theorem SpacetimeFault.weight_empty {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] : empty.weight = 0

@[simp]

theorem SpacetimeFault.weight_eq_space_plus_time {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : F.weight = F.spaceWeight + F.timeWeight

@[simp]

theorem SpacetimeFault.spaceWeight_empty {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] : empty.spaceWeight = 0

@[simp]

theorem SpacetimeFault.timeWeight_empty {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] : empty.timeWeight = 0

theorem SpacetimeFault.weight_ofSpaceFault {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (f : SpaceFault Q T) : (ofSpaceFault f).weight = 1

theorem SpacetimeFault.weight_ofTimeFault {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (f : TimeFault M) : (ofTimeFault f).weight = 1

@[simp]

theorem SpacetimeFault.isPureSpace_empty {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] : empty.isPureSpace

@[simp]

theorem SpacetimeFault.isPureTime_empty {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] : empty.isPureTime

theorem SpacetimeFault.isPureSpace_ofSpaceFault {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (f : SpaceFault Q T) : (ofSpaceFault f).isPureSpace

theorem SpacetimeFault.isPureTime_ofTimeFault {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (f : TimeFault M) : (ofTimeFault f).isPureTime

theorem SpacetimeFault.weight_pos_of_nonempty_space {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] {F : SpacetimeFault Q T M} (h : F.spaceFaults.Nonempty) : 0 < F.weight

theorem SpacetimeFault.weight_pos_of_nonempty_time {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] {F : SpacetimeFault Q T M} (h : F.timeFaults.Nonempty) : 0 < F.weight

Composition Properties

theorem SpacetimeFault.compose_comm {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F₁ F₂ : SpacetimeFault Q T M) : F₁.compose F₂ = F₂.compose F₁

theorem SpacetimeFault.compose_self {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : F.compose F = empty

theorem SpacetimeFault.compose_empty_left {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : empty.compose F = F

theorem SpacetimeFault.compose_empty_right {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : F.compose empty = F

theorem SpacetimeFault.compose_assoc {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F₁ F₂ F₃ : SpacetimeFault Q T M) : (F₁.compose F₂).compose F₃ = F₁.compose (F₂.compose F₃)

Space-only and time-only projections

def SpacetimeFault.spaceComponent {Q : Type u_1} {T : Type u_2} {M : Type u_3} (F : SpacetimeFault Q T M) : SpacetimeFault Q T M

The space component of a spacetime fault (keeping only space-faults).

Equations

• F.spaceComponent = { spaceFaults := F.spaceFaults, timeFaults := ∅ }

def SpacetimeFault.timeComponent {Q : Type u_1} {T : Type u_2} {M : Type u_3} (F : SpacetimeFault Q T M) : SpacetimeFault Q T M

The time component of a spacetime fault (keeping only time-faults).

Equations

• F.timeComponent = { spaceFaults := ∅, timeFaults := F.timeFaults }

@[simp]

theorem SpacetimeFault.spaceComponent_isPureSpace {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : F.spaceComponent.isPureSpace

@[simp]

theorem SpacetimeFault.timeComponent_isPureTime {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : F.timeComponent.isPureTime

theorem SpacetimeFault.weight_spaceComponent {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : F.spaceComponent.weight = F.spaceWeight

theorem SpacetimeFault.weight_timeComponent {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : F.timeComponent.weight = F.timeWeight

theorem SpacetimeFault.decompose_space_time {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : F.spaceComponent.compose F.timeComponent = F

Any spacetime fault decomposes into its space and time components.

Pauli operator associated to space-faults at a given time

def SpacetimeFault.spaceFaultsAt {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq T] (F : SpacetimeFault Q T M) (t : T) : Finset (SpaceFault Q T)

The space-faults of a spacetime fault restricted to a specific time.

Equations

• F.spaceFaultsAt t = {f ∈ F.spaceFaults | f.time = t}

def SpacetimeFault.pauliErrorAt {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [Fintype Q] (F : SpacetimeFault Q T M) (t : T) : PauliOp Q

The composite Pauli error on qubit system Q from all space-faults at time t.

Equations

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

@[simp]

theorem SpacetimeFault.pauliErrorAt_empty {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] [Fintype Q] (t : T) : empty.pauliErrorAt t = 1

Convention: Initialization faults as time-faults

The convention that initialization faults are treated as time-faults is captured by modeling each initialization as a measurement. An initialization fault (e.g., preparing |1> instead of |0>) is then a time-fault on that measurement, equivalent to perfect initialization followed by a Pauli X error (space-fault).

def SpacetimeFault.initializationFault {Q : Type u_1} {T : Type u_2} {M : Type u_3} (initMeasurement : M) : SpacetimeFault Q T M

An initialization fault viewed as a time-fault on the initialization measurement.

Equations

• SpacetimeFault.initializationFault initMeasurement = SpacetimeFault.ofTimeFault { measurement := initMeasurement }

def SpacetimeFault.initializationAsSpaceFault {Q : Type u_1} {T : Type u_2} {M : Type u_3} (q : Q) (t : T) : SpacetimeFault Q T M

The equivalent space-fault: perfect initialization followed by Pauli X error.

Equations

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

theorem SpacetimeFault.initializationFault_weight {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (m : M) : (initializationFault m).weight = 1

theorem SpacetimeFault.initializationAsSpaceFault_weight {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (q : Q) (t : T) : (initializationAsSpaceFault q t).weight = 1

Weight bounds

theorem SpacetimeFault.spaceWeight_le_weight {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : F.spaceWeight ≤ F.weight

theorem SpacetimeFault.timeWeight_le_weight {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : F.timeWeight ≤ F.weight

theorem SpacetimeFault.weight_zero_iff {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : F.weight = 0 ↔ F.spaceFaults = ∅ ∧ F.timeFaults = ∅

theorem SpacetimeFault.weight_zero_iff_empty {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : F.weight = 0 ↔ F = empty

Fault classification predicates

def SpacetimeFault.isTrivial {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq T] [DecidableEq M] [DecidableEq (SpaceFault Q T)] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : Prop

A spacetime fault is trivial (identity) if it has no faults at all.

Equations

• F.isTrivial = (F = SpacetimeFault.empty)

def SpacetimeFault.affectedQubits {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq Q] [DecidableEq (SpaceFault Q T)] (F : SpacetimeFault Q T M) : Finset Q

The set of qubits affected by space-faults in a spacetime fault.

Equations

• F.affectedQubits = Finset.image SpaceFault.qubit F.spaceFaults

def SpacetimeFault.activeTimes {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq T] [DecidableEq (SpaceFault Q T)] (F : SpacetimeFault Q T M) : Finset T

The set of times at which space-faults occur.

Equations

• F.activeTimes = Finset.image SpaceFault.time F.spaceFaults

def SpacetimeFault.affectedMeasurements {Q : Type u_1} {T : Type u_2} {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (F : SpacetimeFault Q T M) : Finset M

The set of measurements affected by time-faults.

Equations

• F.affectedMeasurements = Finset.image TimeFault.measurement F.timeFaults

Measurement outcome with faults

A time-fault flips the measurement outcome. In ZMod 2 encoding (0 -> +1, 1 -> -1), this means adding 1 to the ideal outcome.

def observedOutcome {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (idealOutcome : M → ZMod 2) (faults : Finset (TimeFault M)) (m : M) : ZMod 2

The observed measurement outcome given an ideal outcome and a set of time-faults. If measurement m appears in the time-faults, the outcome is flipped.

Equations

• observedOutcome idealOutcome faults m = idealOutcome m + if { measurement := m } ∈ faults then 1 else 0

theorem observedOutcome_no_fault {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (idealOutcome : M → ZMod 2) (faults : Finset (TimeFault M)) (m : M) (h : { measurement := m } ∉ faults) : observedOutcome idealOutcome faults m = idealOutcome m

theorem observedOutcome_with_fault {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (idealOutcome : M → ZMod 2) (faults : Finset (TimeFault M)) (m : M) (h : { measurement := m } ∈ faults) : observedOutcome idealOutcome faults m = idealOutcome m + 1

theorem observedOutcome_flip {M : Type u_3} [DecidableEq M] [DecidableEq (TimeFault M)] (idealOutcome : M → ZMod 2) (faults : Finset (TimeFault M)) (m : M) (h : { measurement := m } ∈ faults) : observedOutcome idealOutcome faults m ≠ idealOutcome m