Def_7: Space and Time Faults

Statement

In the context of fault-tolerant implementation of the gauging measurement procedure:

Space-fault: A Pauli error operator (single-qubit X, Y, or Z error) that occurs on some qubit at some time during the procedure. Space-faults are characterized by the qubit affected and the time of occurrence.

Time-fault (measurement error): An error where the result of a quantum measurement is reported incorrectly. The actual measurement projects onto an eigenspace, but the classical outcome is flipped. Time-faults are characterized by the measurement affected and the time step.

State initialization fault: Treated as equivalent to a time-fault. A faulty initialization of state |ψ⟩ is modeled as perfect initialization followed by an immediate space-fault.

Spacetime fault: A collection of space-faults and time-faults occurring at various locations and times during the procedure. The set of all spacetime faults forms a group under composition.

Main Definitions

• PauliType : The three Pauli error types (X, Y, Z)
• SpaceFault : A single-qubit Pauli error at a specific qubit and time
• TimeFault : A measurement error (bit flip) at a specific measurement and time
• InitializationFault : A state initialization fault (modeled as time-fault)
• SpacetimeFault : A collection of space-faults and time-faults
• SpacetimeFaultGroup : The group structure on spacetime faults

Key Properties

• spaceFault_identity : Identity space-fault (no error)
• timeFault_identity : Identity time-fault (no measurement error)
• spacetimeFault_compose : Composition of spacetime faults
• spacetimeFault_inv : Inverse of a spacetime fault
• spacetimeFault_group : Group structure on spacetime faults

Time Steps

We model time discretely. Each round of the procedure corresponds to a time step. Time steps are indexed by natural numbers.

@[reducible, inline]

abbrev TimeStep : Type

A time step in the fault-tolerant procedure. Time 0 is the start, and time increases with each round.

Equations

• TimeStep = ℕ

Pauli Error Types

A single-qubit Pauli error can be X, Y, or Z. We also include Identity (I) for completeness, representing "no error".

inductive PauliType : Type

The four single-qubit Pauli operators

• I : PauliType
• X : PauliType
• Y : PauliType
• Z : PauliType

instance instDecidableEqPauliType : DecidableEq PauliType

Equations

• instDecidableEqPauliType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprPauliType.repr : PauliType → ℕ → Std.Format

Equations

• instReprPauliType.repr PauliType.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PauliType.I")).group prec✝
• instReprPauliType.repr PauliType.X prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PauliType.X")).group prec✝
• instReprPauliType.repr PauliType.Y prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PauliType.Y")).group prec✝
• instReprPauliType.repr PauliType.Z prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PauliType.Z")).group prec✝

instance instReprPauliType : Repr PauliType

Equations

• instReprPauliType = { reprPrec := instReprPauliType.repr }

def instInhabitedPauliType.default : PauliType

Equations

• instInhabitedPauliType.default = PauliType.I

instance instInhabitedPauliType : Inhabited PauliType

Equations

• instInhabitedPauliType = { default := instInhabitedPauliType.default }

def PauliType.mul : PauliType → PauliType → PauliType

Pauli multiplication table. I is identity, X² = Y² = Z² = I, and XYZ = iI (we ignore global phases).

Equations

• PauliType.I.mul x✝ = x✝
• x✝.mul PauliType.I = x✝
• PauliType.X.mul PauliType.X = PauliType.I
• PauliType.Y.mul PauliType.Y = PauliType.I
• PauliType.Z.mul PauliType.Z = PauliType.I
• PauliType.X.mul PauliType.Y = PauliType.Z
• PauliType.Y.mul PauliType.X = PauliType.Z
• PauliType.Y.mul PauliType.Z = PauliType.X
• PauliType.Z.mul PauliType.Y = PauliType.X
• PauliType.Z.mul PauliType.X = PauliType.Y
• PauliType.X.mul PauliType.Z = PauliType.Y

instance PauliType.instMul : Mul PauliType

Equations

• PauliType.instMul = { mul := PauliType.mul }

def PauliType.inv : PauliType → PauliType

Pauli operators are self-inverse (up to phase)

Equations

• PauliType.inv = id

instance PauliType.instInv : Inv PauliType

Equations

• PauliType.instInv = { inv := PauliType.inv }

instance PauliType.instOne : One PauliType

Identity element

Equations

• PauliType.instOne = { one := PauliType.I }

@[simp]

theorem PauliType.one_eq_I : 1 = I

@[simp]

theorem PauliType.mul_I (p : PauliType) : p * I = p

@[simp]

theorem PauliType.I_mul (p : PauliType) : I * p = p

@[simp]

theorem PauliType.mul_self (p : PauliType) : p * p = I

@[simp]

theorem PauliType.inv_eq_self (p : PauliType) : p⁻¹ = p

theorem PauliType.mul_assoc (a b c : PauliType) : a * b * c = a * (b * c)

Pauli multiplication is associative

theorem PauliType.mul_inv_cancel (p : PauliType) : p * p⁻¹ = 1

Pauli inverses work correctly

theorem PauliType.inv_mul_cancel (p : PauliType) : p⁻¹ * p = 1

instance PauliType.instGroup : Group PauliType

PauliType forms a group

Equations

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

def PauliType.isError : PauliType → Bool

Check if a Pauli type represents an actual error (not identity)

Equations

• PauliType.I.isError = false
• x✝.isError = true

@[simp]

theorem PauliType.isError_I : I.isError = false

@[simp]

theorem PauliType.isError_X : X.isError = true

@[simp]

theorem PauliType.isError_Y : Y.isError = true

@[simp]

theorem PauliType.isError_Z : Z.isError = true

Qubit Index Type

Qubits are indexed by some type. In the gauging context, we have:

• Vertex qubits (indexed by V)
• Edge qubits (indexed by E) We use a unified qubit index type that can represent both.

inductive QubitLoc (V : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A qubit location in the system. Can be a vertex qubit or an edge qubit.

• vertex {V : Type u_1} {E : Type u_2} : V → QubitLoc V E
• edge {V : Type u_1} {E : Type u_2} : E → QubitLoc V E

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

Equations

• instDecidableEqQubitLoc.decEq (QubitLoc.vertex a) (QubitLoc.vertex b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqQubitLoc.decEq (QubitLoc.vertex a) (QubitLoc.edge a_1) = isFalse ⋯
• instDecidableEqQubitLoc.decEq (QubitLoc.edge a) (QubitLoc.vertex a_1) = isFalse ⋯
• instDecidableEqQubitLoc.decEq (QubitLoc.edge a) (QubitLoc.edge b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance instDecidableEqQubitLoc {V✝ : Type u_1} {E✝ : Type u_2} [DecidableEq V✝] [DecidableEq E✝] : DecidableEq (QubitLoc V✝ E✝)

Equations

• instDecidableEqQubitLoc = instDecidableEqQubitLoc.decEq

def QubitLoc.isVertex {V : Type u_1} {E : Type u_2} : QubitLoc V E → Bool

Check if a location is a vertex qubit

Equations

• (QubitLoc.vertex a).isVertex = true
• (QubitLoc.edge a).isVertex = false

def QubitLoc.isEdge {V : Type u_1} {E : Type u_2} : QubitLoc V E → Bool

Check if a location is an edge qubit

Equations

• (QubitLoc.vertex a).isEdge = false
• (QubitLoc.edge a).isEdge = true

@[simp]

theorem QubitLoc.isVertex_vertex {V : Type u_1} {E : Type u_2} (v : V) : (vertex v).isVertex = true

@[simp]

theorem QubitLoc.isVertex_edge {V : Type u_1} {E : Type u_2} (e : E) : (edge e).isVertex = false

@[simp]

theorem QubitLoc.isEdge_vertex {V : Type u_1} {E : Type u_2} (v : V) : (vertex v).isEdge = false

@[simp]

theorem QubitLoc.isEdge_edge {V : Type u_1} {E : Type u_2} (e : E) : (edge e).isEdge = true

def QubitLoc.getVertex {V : Type u_1} {E : Type u_2} : QubitLoc V E → Option V

Extract the vertex index if this is a vertex qubit

Equations

• (QubitLoc.vertex a).getVertex = some a
• (QubitLoc.edge a).getVertex = none

def QubitLoc.getEdge {V : Type u_1} {E : Type u_2} : QubitLoc V E → Option E

Extract the edge index if this is an edge qubit

Equations

• (QubitLoc.vertex a).getEdge = none
• (QubitLoc.edge a).getEdge = some a

instance QubitLoc.instFintype {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] : Fintype (QubitLoc V E)

Equations

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

@[simp]

theorem QubitLoc.card_qubitLoc {V : Type u_1} {E : Type u_2} [Fintype V] [Fintype E] : Fintype.card (QubitLoc V E) = Fintype.card V + Fintype.card E

Measurement Index Type

Measurements are indexed by type M. Each measurement corresponds to measuring some check operator (Gauss law A_v, flux B_p, or original stabilizer s_j).

@[reducible, inline]

abbrev MeasurementIdx (M : Type u_1) : Type u_1

A measurement index. This identifies which measurement is being referred to.

Equations

• MeasurementIdx M = M

Space-Faults

A space-fault is a single-qubit Pauli error occurring on a specific qubit at a specific time.

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

A space-fault: a Pauli error on a specific qubit at a specific time. The error pauliType occurs on qubit qubit at time time.

• qubit : QubitLoc V E

  The qubit where the error occurs

• time : TimeStep

  The time step when the error occurs

• pauliType : PauliType

  The type of Pauli error (X, Y, Z, or I for no error)

instance instDecidableEqSpaceFault {V✝ : Type u_1} {E✝ : Type u_2} [DecidableEq V✝] [DecidableEq E✝] : DecidableEq (SpaceFault V✝ E✝)

Equations

• instDecidableEqSpaceFault = instDecidableEqSpaceFault.decEq

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

Equations

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

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

The identity space-fault at a given location and time (no error)

Equations

• SpaceFault.identity q t = { qubit := q, time := t, pauliType := PauliType.I }

def SpaceFault.isActualError {V : Type u_1} {E : Type u_2} (f : SpaceFault V E) : Bool

Check if this space-fault represents an actual error

Equations

• f.isActualError = f.pauliType.isError

@[simp]

theorem SpaceFault.isActualError_identity {V : Type u_1} {E : Type u_2} (q : QubitLoc V E) (t : TimeStep) : (identity q t).isActualError = false

def SpaceFault.compose {V : Type u_1} {E : Type u_2} (f g : SpaceFault V E) (_h_qubit : f.qubit = g.qubit) (_h_time : f.time = g.time) : SpaceFault V E

Compose two space-faults at the same location and time

Equations

• f.compose g _h_qubit _h_time = { qubit := f.qubit, time := f.time, pauliType := f.pauliType * g.pauliType }

def SpaceFault.inv {V : Type u_1} {E : Type u_2} (f : SpaceFault V E) : SpaceFault V E

The inverse of a space-fault (same fault, since Paulis are self-inverse)

Equations

• f.inv = { qubit := f.qubit, time := f.time, pauliType := f.pauliType⁻¹ }

@[simp]

theorem SpaceFault.inv_pauliType {V : Type u_1} {E : Type u_2} (f : SpaceFault V E) : f.inv.pauliType = f.pauliType

@[simp]

theorem SpaceFault.inv_qubit {V : Type u_1} {E : Type u_2} (f : SpaceFault V E) : f.inv.qubit = f.qubit

@[simp]

theorem SpaceFault.inv_time {V : Type u_1} {E : Type u_2} (f : SpaceFault V E) : f.inv.time = f.time

def SpaceFault.onVertex {V : Type u_1} {E : Type u_2} (v : V) (t : TimeStep) (p : PauliType) : SpaceFault V E

A space-fault on a vertex qubit

Equations

• SpaceFault.onVertex v t p = { qubit := QubitLoc.vertex v, time := t, pauliType := p }

def SpaceFault.onEdge {V : Type u_1} {E : Type u_2} (e : E) (t : TimeStep) (p : PauliType) : SpaceFault V E

A space-fault on an edge qubit

Equations

• SpaceFault.onEdge e t p = { qubit := QubitLoc.edge e, time := t, pauliType := p }

@[simp]

theorem SpaceFault.onVertex_qubit {V : Type u_1} {E : Type u_2} (v : V) (t : TimeStep) (p : PauliType) : (onVertex v t p).qubit = QubitLoc.vertex v

@[simp]

theorem SpaceFault.onEdge_qubit {V : Type u_1} {E : Type u_2} (e : E) (t : TimeStep) (p : PauliType) : (onEdge e t p).qubit = QubitLoc.edge e

@[reducible, inline]

abbrev SpaceFault.X_vertex {V : Type u_1} {E : Type u_2} (v : V) (t : TimeStep) : SpaceFault V E

An X error on a vertex qubit

Equations

• SpaceFault.X_vertex v t = SpaceFault.onVertex v t PauliType.X

@[reducible, inline]

abbrev SpaceFault.Y_vertex {V : Type u_1} {E : Type u_2} (v : V) (t : TimeStep) : SpaceFault V E

A Y error on a vertex qubit

Equations

• SpaceFault.Y_vertex v t = SpaceFault.onVertex v t PauliType.Y

@[reducible, inline]

abbrev SpaceFault.Z_vertex {V : Type u_1} {E : Type u_2} (v : V) (t : TimeStep) : SpaceFault V E

A Z error on a vertex qubit

Equations

• SpaceFault.Z_vertex v t = SpaceFault.onVertex v t PauliType.Z

@[reducible, inline]

abbrev SpaceFault.X_edge {V : Type u_1} {E : Type u_2} (e : E) (t : TimeStep) : SpaceFault V E

An X error on an edge qubit

Equations

• SpaceFault.X_edge e t = SpaceFault.onEdge e t PauliType.X

@[reducible, inline]

abbrev SpaceFault.Y_edge {V : Type u_1} {E : Type u_2} (e : E) (t : TimeStep) : SpaceFault V E

A Y error on an edge qubit

Equations

• SpaceFault.Y_edge e t = SpaceFault.onEdge e t PauliType.Y

@[reducible, inline]

abbrev SpaceFault.Z_edge {V : Type u_1} {E : Type u_2} (e : E) (t : TimeStep) : SpaceFault V E

A Z error on an edge qubit

Equations

• SpaceFault.Z_edge e t = SpaceFault.onEdge e t PauliType.Z

Time-Faults (Measurement Errors)

A time-fault is a measurement error: the classical outcome of a measurement is flipped. This is also called a "measurement error" or "readout error".

structure TimeFault (M : Type u_1) : Type u_1

A time-fault: a measurement whose classical outcome is flipped. The measurement measurement at time time reports the wrong outcome.

• measurement : M

  The measurement that is affected

• time : TimeStep

  The time step when the measurement occurs

• isFlipped : Bool

  Whether this fault is active (true = flipped outcome)

instance instDecidableEqTimeFault {M✝ : Type u_1} [DecidableEq M✝] : DecidableEq (TimeFault M✝)

Equations

• instDecidableEqTimeFault = instDecidableEqTimeFault.decEq

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

Equations

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

def TimeFault.identity {M : Type u_1} (m : M) (t : TimeStep) : TimeFault M

The identity time-fault (no measurement error)

Equations

• TimeFault.identity m t = { measurement := m, time := t, isFlipped := false }

def TimeFault.active {M : Type u_1} (m : M) (t : TimeStep) : TimeFault M

An active measurement error

Equations

• TimeFault.active m t = { measurement := m, time := t, isFlipped := true }

def TimeFault.isActualError {M : Type u_1} (f : TimeFault M) : Bool

Check if this time-fault represents an actual error

Equations

• f.isActualError = f.isFlipped

@[simp]

theorem TimeFault.isActualError_identity {M : Type u_1} (m : M) (t : TimeStep) : (identity m t).isActualError = false

@[simp]

theorem TimeFault.isActualError_active {M : Type u_1} (m : M) (t : TimeStep) : (active m t).isActualError = true

def TimeFault.compose {M : Type u_1} (f g : TimeFault M) (_h_meas : f.measurement = g.measurement) (_h_time : f.time = g.time) : TimeFault M

Compose two time-faults at the same measurement and time (XOR of flips)

Equations

• f.compose g _h_meas _h_time = { measurement := f.measurement, time := f.time, isFlipped := f.isFlipped ^^ g.isFlipped }

def TimeFault.inv {M : Type u_1} (f : TimeFault M) : TimeFault M

The inverse of a time-fault (same fault, since flip is self-inverse)

Equations

• f.inv = f

@[simp]

theorem TimeFault.inv_isFlipped {M : Type u_1} (f : TimeFault M) : f.inv.isFlipped = f.isFlipped

@[simp]

theorem TimeFault.inv_measurement {M : Type u_1} (f : TimeFault M) : f.inv.measurement = f.measurement

@[simp]

theorem TimeFault.inv_time {M : Type u_1} (f : TimeFault M) : f.inv.time = f.time

Initialization Faults

A state initialization fault is treated as equivalent to a time-fault. A faulty initialization of state |ψ⟩ is modeled as perfect initialization followed by an immediate space-fault.

We model this by having initialization faults be a special case that can be represented either as a time-fault on the initialization "measurement" or as a space-fault immediately after initialization.

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

An initialization fault on a qubit. This represents a faulty preparation of the initial state. It is modeled as equivalent to perfect initialization followed by a space-fault.

• qubit : QubitLoc V E

  The qubit being initialized

• time : TimeStep

  The time step of initialization

• effectiveError : PauliType

  The effective Pauli error (applied after "perfect" initialization)

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

Equations

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

instance instDecidableEqInitializationFault {V✝ : Type u_1} {E✝ : Type u_2} [DecidableEq V✝] [DecidableEq E✝] : DecidableEq (InitializationFault V✝ E✝)

Equations

• instDecidableEqInitializationFault = instDecidableEqInitializationFault.decEq

def InitializationFault.toSpaceFault {V : Type u_1} {E : Type u_2} (f : InitializationFault V E) : SpaceFault V E

Convert an initialization fault to an equivalent space-fault. The space-fault occurs at the same time as the initialization.

Equations

• f.toSpaceFault = { qubit := f.qubit, time := f.time, pauliType := f.effectiveError }

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

The identity initialization fault (no error)

Equations

• InitializationFault.identity q t = { qubit := q, time := t, effectiveError := PauliType.I }

def InitializationFault.isActualError {V : Type u_1} {E : Type u_2} (f : InitializationFault V E) : Bool

Check if this initialization fault represents an actual error

Equations

• f.isActualError = f.effectiveError.isError

@[simp]

theorem InitializationFault.toSpaceFault_qubit {V : Type u_1} {E : Type u_2} (f : InitializationFault V E) : f.toSpaceFault.qubit = f.qubit

@[simp]

theorem InitializationFault.toSpaceFault_time {V : Type u_1} {E : Type u_2} (f : InitializationFault V E) : f.toSpaceFault.time = f.time

@[simp]

theorem InitializationFault.toSpaceFault_pauliType {V : Type u_1} {E : Type u_2} (f : InitializationFault V E) : f.toSpaceFault.pauliType = f.effectiveError

@[simp]

theorem InitializationFault.toSpaceFault_identity {V : Type u_1} {E : Type u_2} (q : QubitLoc V E) (t : TimeStep) : (identity q t).toSpaceFault = SpaceFault.identity q t

Spacetime Faults

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

structure SpacetimeFault (V : Type u_1) (E : Type u_2) (M : Type u_3) : Type (max (max u_1 u_2) u_3)

A spacetime fault: a collection of space-faults and time-faults.

We represent this as:

• A function from (qubit, time) pairs to Pauli errors (for space-faults)
• A function from (measurement, time) pairs to flip flags (for time-faults)

This representation allows for efficient composition (pointwise multiplication/XOR).

• spaceErrors : QubitLoc V E → TimeStep → PauliType

  The Pauli error at each (qubit, time) location. Identity means no error.

• timeErrors : M → TimeStep → Bool

  Whether each (measurement, time) has a flipped outcome. False means no error.

theorem SpacetimeFault.ext {V : Type u_1} {E : Type u_2} {M : Type u_3} {x y : SpacetimeFault V E M} (spaceErrors : x.spaceErrors = y.spaceErrors) (timeErrors : x.timeErrors = y.timeErrors) : x = y

theorem SpacetimeFault.ext_iff {V : Type u_1} {E : Type u_2} {M : Type u_3} {x y : SpacetimeFault V E M} : x = y ↔ x.spaceErrors = y.spaceErrors ∧ x.timeErrors = y.timeErrors

def SpacetimeFault.identity {V : Type u_1} {E : Type u_2} {M : Type u_3} : SpacetimeFault V E M

The identity spacetime fault (no errors anywhere)

Equations

• SpacetimeFault.identity = { spaceErrors := fun (x : QubitLoc V E) (x_1 : TimeStep) => PauliType.I, timeErrors := fun (x : M) (x_1 : TimeStep) => false }

instance SpacetimeFault.instOne {V : Type u_1} {E : Type u_2} {M : Type u_3} : One (SpacetimeFault V E M)

Equations

• SpacetimeFault.instOne = { one := SpacetimeFault.identity }

@[simp]

theorem SpacetimeFault.one_spaceErrors {V : Type u_1} {E : Type u_2} {M : Type u_3} (q : QubitLoc V E) (t : TimeStep) : spaceErrors 1 q t = PauliType.I

@[simp]

theorem SpacetimeFault.one_timeErrors {V : Type u_1} {E : Type u_2} {M : Type u_3} (m : M) (t : TimeStep) : timeErrors 1 m t = false

def SpacetimeFault.compose {V : Type u_1} {E : Type u_2} {M : Type u_3} (f g : SpacetimeFault V E M) : SpacetimeFault V E M

Composition of spacetime faults (pointwise multiplication/XOR)

Equations

• f.compose g = { spaceErrors := fun (q : QubitLoc V E) (t : TimeStep) => f.spaceErrors q t * g.spaceErrors q t, timeErrors := fun (m : M) (t : TimeStep) => f.timeErrors m t ^^ g.timeErrors m t }

instance SpacetimeFault.instMul {V : Type u_1} {E : Type u_2} {M : Type u_3} : Mul (SpacetimeFault V E M)

Equations

• SpacetimeFault.instMul = { mul := SpacetimeFault.compose }

@[simp]

theorem SpacetimeFault.mul_spaceErrors {V : Type u_1} {E : Type u_2} {M : Type u_3} (f g : SpacetimeFault V E M) (q : QubitLoc V E) (t : TimeStep) : (f * g).spaceErrors q t = f.spaceErrors q t * g.spaceErrors q t

@[simp]

theorem SpacetimeFault.mul_timeErrors {V : Type u_1} {E : Type u_2} {M : Type u_3} (f g : SpacetimeFault V E M) (m : M) (t : TimeStep) : (f * g).timeErrors m t = (f.timeErrors m t ^^ g.timeErrors m t)

def SpacetimeFault.inv {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) : SpacetimeFault V E M

Inverse of a spacetime fault

Equations

• f.inv = { spaceErrors := fun (q : QubitLoc V E) (t : TimeStep) => (f.spaceErrors q t)⁻¹, timeErrors := f.timeErrors }

instance SpacetimeFault.instInv {V : Type u_1} {E : Type u_2} {M : Type u_3} : Inv (SpacetimeFault V E M)

Equations

• SpacetimeFault.instInv = { inv := SpacetimeFault.inv }

@[simp]

theorem SpacetimeFault.inv_spaceErrors {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) (q : QubitLoc V E) (t : TimeStep) : f⁻¹.spaceErrors q t = (f.spaceErrors q t)⁻¹

@[simp]

theorem SpacetimeFault.inv_timeErrors {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) (m : M) (t : TimeStep) : f⁻¹.timeErrors m t = f.timeErrors m t

theorem SpacetimeFault.mul_assoc {V : Type u_1} {E : Type u_2} {M : Type u_3} (a b c : SpacetimeFault V E M) : a * b * c = a * (b * c)

Spacetime faults form a group under composition

theorem SpacetimeFault.one_mul {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) : 1 * f = f

theorem SpacetimeFault.mul_one {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) : f * 1 = f

theorem SpacetimeFault.inv_mul_cancel {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) : f⁻¹ * f = 1

instance SpacetimeFault.instGroup {V : Type u_1} {E : Type u_2} {M : Type u_3} : Group (SpacetimeFault V E M)

Equations

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

def SpacetimeFault.fromSpaceFault {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] (f : SpaceFault V E) : SpacetimeFault V E M

Create a spacetime fault from a single space-fault

Equations

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

def SpacetimeFault.fromTimeFault {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq M] (f : TimeFault M) : SpacetimeFault V E M

Create a spacetime fault from a single time-fault

Equations

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

def SpacetimeFault.fromInitializationFault {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] (f : InitializationFault V E) : SpacetimeFault V E M

Create a spacetime fault from a single initialization fault

Equations

• SpacetimeFault.fromInitializationFault f = SpacetimeFault.fromSpaceFault f.toSpaceFault

@[simp]

theorem SpacetimeFault.fromSpaceFault_at_location {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] (f : SpaceFault V E) : (fromSpaceFault f).spaceErrors f.qubit f.time = f.pauliType

@[simp]

theorem SpacetimeFault.fromTimeFault_at_location {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq M] (f : TimeFault M) : (fromTimeFault f).timeErrors f.measurement f.time = f.isFlipped

def SpacetimeFault.spaceErrorLocations {V : Type u_1} {E : Type u_2} {M : Type u_3} [Fintype V] [Fintype E] (f : SpacetimeFault V E M) (times : Finset TimeStep) : Finset (QubitLoc V E × TimeStep)

The set of (qubit, time) locations where space errors occur

Equations

• f.spaceErrorLocations times = {x ∈ Finset.univ ×ˢ times | match x with | (q, t) => f.spaceErrors q t ≠ PauliType.I}

def SpacetimeFault.timeErrorLocations {V : Type u_1} {E : Type u_2} {M : Type u_3} [Fintype M] (f : SpacetimeFault V E M) (times : Finset TimeStep) : Finset (M × TimeStep)

The set of (measurement, time) locations where time errors occur

Equations

• f.timeErrorLocations times = {x ∈ Finset.univ ×ˢ times | match x with | (m, t) => f.timeErrors m t = true}

def SpacetimeFault.weight {V : Type u_1} {E : Type u_2} {M : Type u_3} [Fintype V] [Fintype E] [Fintype M] (f : SpacetimeFault V E M) (times : Finset TimeStep) : ℕ

The total weight of a spacetime fault (number of non-trivial errors) over given time range

Equations

• f.weight times = (f.spaceErrorLocations times).card + (f.timeErrorLocations times).card

@[simp]

theorem SpacetimeFault.weight_identity {V : Type u_1} {E : Type u_2} {M : Type u_3} [Fintype V] [Fintype E] [Fintype M] (times : Finset TimeStep) : weight 1 times = 0

def SpacetimeFault.isPureSpace {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) : Prop

A spacetime fault is "pure space" if it has no time errors

Equations

• f.isPureSpace = ∀ (m : M) (t : TimeStep), f.timeErrors m t = false

def SpacetimeFault.isPureTime {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) : Prop

A spacetime fault is "pure time" if it has no space errors

Equations

• f.isPureTime = ∀ (q : QubitLoc V E) (t : TimeStep), f.spaceErrors q t = PauliType.I

@[simp]

theorem SpacetimeFault.identity_isPureSpace {V : Type u_1} {E : Type u_2} {M : Type u_3} : isPureSpace 1

@[simp]

theorem SpacetimeFault.identity_isPureTime {V : Type u_1} {E : Type u_2} {M : Type u_3} : isPureTime 1

theorem SpacetimeFault.fromSpaceFault_isPureSpace {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] (f : SpaceFault V E) : (fromSpaceFault f).isPureSpace

theorem SpacetimeFault.fromTimeFault_isPureTime {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq M] (f : TimeFault M) : (fromTimeFault f).isPureTime

def SpacetimeFault.spaceComponent {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) : SpacetimeFault V E M

The space-only component of a spacetime fault

Equations

• f.spaceComponent = { spaceErrors := f.spaceErrors, timeErrors := fun (x : M) (x_1 : TimeStep) => false }

def SpacetimeFault.timeComponent {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) : SpacetimeFault V E M

The time-only component of a spacetime fault

Equations

• f.timeComponent = { spaceErrors := fun (x : QubitLoc V E) (x_1 : TimeStep) => PauliType.I, timeErrors := f.timeErrors }

@[simp]

theorem SpacetimeFault.spaceComponent_isPureSpace {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) : f.spaceComponent.isPureSpace

@[simp]

theorem SpacetimeFault.timeComponent_isPureTime {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) : f.timeComponent.isPureTime

theorem SpacetimeFault.decompose {V : Type u_1} {E : Type u_2} {M : Type u_3} (f : SpacetimeFault V E M) : f = f.spaceComponent * f.timeComponent

A spacetime fault decomposes into its space and time components

The Group of Spacetime Faults

The set of all spacetime faults forms a group under composition. This is captured by the Group instance on SpacetimeFault.

def pureSpaceFaults (V : Type u_1) (E : Type u_2) (M : Type u_3) : Subgroup (SpacetimeFault V E M)

The subgroup of pure space-faults

Equations

• pureSpaceFaults V E M = { carrier := {f : SpacetimeFault V E M | f.isPureSpace}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

def pureTimeFaults (V : Type u_1) (E : Type u_2) (M : Type u_3) : Subgroup (SpacetimeFault V E M)

The subgroup of pure time-faults

Equations

• pureTimeFaults V E M = { carrier := {f : SpacetimeFault V E M | f.isPureTime}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Summary

This formalization captures the fault model for fault-tolerant quantum error correction:

1. Space-faults: Single-qubit Pauli errors (X, Y, Z) occurring at specific qubits and times.

   • Represented by SpaceFault V E which records qubit location, time, and error type.
   • Can occur on vertex qubits (V) or edge qubits (E).

2. Time-faults: Measurement errors where classical outcomes are flipped.

   • Represented by TimeFault M which records measurement index, time, and flip status.
   • Models readout errors in the measurement process.

3. Initialization faults: Faulty state preparation.

   • Modeled as equivalent to a space-fault immediately after initialization.
   • Represented by InitializationFault V E.

4. Spacetime faults: Collections of space and time faults.

   • Represented by SpacetimeFault V E M as functions from locations to errors.
   • Form a group under pointwise composition (Group instance).
   • Can be decomposed into pure-space and pure-time components.

Key properties proven:

• PauliType forms a group (Pauli operators under multiplication)
• SpacetimeFault forms a group under composition
• Pure space-faults form a subgroup
• Pure time-faults form a subgroup
• Every spacetime fault decomposes as space_component * time_component