MerLean-example

17 Def 7: Space and Time Faults

In the context of fault-tolerant implementation of the gauging measurement procedure, we formalize the notions of space-faults (single-qubit Pauli errors), time-faults (measurement errors), initialization faults, and their collective description as spacetime faults forming a group.

Definition 513 Pauli Error Type
#

The Pauli error type is an inductive type with four constructors:

\[ \texttt{PauliType} ::= I \mid X \mid Y \mid Z, \]

representing the identity (no error), bit flip, combined bit-and-phase flip, and phase flip, respectively.

Definition 514 Pauli Multiplication
#

The multiplication of Pauli types is defined by the standard Pauli multiplication table (ignoring global phases):

  • \(I\) is the identity: \(I \cdot p = p \cdot I = p\) for all \(p\).

  • Each Pauli is self-inverse: \(X^2 = Y^2 = Z^2 = I\).

  • Products of distinct non-identity Paulis: \(XY = Z\), \(YX = Z\), \(YZ = X\), \(ZY = X\), \(ZX = Y\), \(XZ = Y\).

Definition 515 Pauli Inverse
#

The inverse of a Pauli type is defined as the identity function, since each Pauli operator is self-inverse (up to global phase): \(p^{-1} = p\) for all \(p : \texttt{PauliType}\).

Definition 516 Pauli isError
#

A Pauli type represents an actual error if it is not the identity:

\[ \operatorname {isError}(p) = \begin{cases} \text{false} & \text{if } p = I, \\ \text{true} & \text{otherwise}. \end{cases} \]
Theorem 517 Pauli Multiplication is Associative
#

For all \(a, b, c : \texttt{PauliType}\), we have \((a \cdot b) \cdot c = a \cdot (b \cdot c)\).

Proof

By case analysis on all combinations of \(a\), \(b\), and \(c\) (each ranging over \(\{ I, X, Y, Z\} \)), each case holds by reflexivity.

Theorem 518 Pauli Inverse Cancellation (right)

For all \(p : \texttt{PauliType}\), \(p \cdot p^{-1} = 1\).

Proof

Since \(p^{-1} = p\), this reduces to \(p \cdot p = I\), which holds by the self-inverse property of each Pauli type.

Theorem 519 Pauli Inverse Cancellation (left)

For all \(p : \texttt{PauliType}\), \(p^{-1} \cdot p = 1\).

Proof

Since \(p^{-1} = p\), this reduces to \(p \cdot p = I\), which holds by the self-inverse property.

Definition 520 Qubit Location
#

Given types \(V\) and \(E\), a qubit location is an inductive type:

\[ \texttt{QubitLoc}(V, E) ::= \operatorname {vertex}(v) \mid \operatorname {edge}(e), \]

where \(v : V\) represents a vertex qubit and \(e : E\) represents an edge qubit.

Definition 521 QubitLoc.isVertex
#

A qubit location is a vertex qubit if it was constructed via the \(\operatorname {vertex}\) constructor:

\[ \operatorname {isVertex}(\operatorname {vertex}(v)) = \text{true}, \quad \operatorname {isVertex}(\operatorname {edge}(e)) = \text{false}. \]
Definition 522 QubitLoc.isEdge
#

A qubit location is an edge qubit if it was constructed via the \(\operatorname {edge}\) constructor:

\[ \operatorname {isEdge}(\operatorname {vertex}(v)) = \text{false}, \quad \operatorname {isEdge}(\operatorname {edge}(e)) = \text{true}. \]
Definition 523 QubitLoc.getVertex
#

Extracts the vertex index from a qubit location, returning \(\operatorname {some}(v)\) if the location is \(\operatorname {vertex}(v)\) and \(\operatorname {none}\) otherwise.

Definition 524 QubitLoc.getEdge
#

Extracts the edge index from a qubit location, returning \(\operatorname {some}(e)\) if the location is \(\operatorname {edge}(e)\) and \(\operatorname {none}\) otherwise.

Lemma 525 Cardinality of QubitLoc
#

If \(V\) and \(E\) are finite types, then

\[ |\texttt{QubitLoc}(V, E)| = |V| + |E|. \]
Proof

We construct an explicit equivalence between \(\texttt{QubitLoc}(V, E)\) and the sum type \(V \oplus E\): the map sends \(\operatorname {vertex}(v) \mapsto \operatorname {inl}(v)\) and \(\operatorname {edge}(e) \mapsto \operatorname {inr}(e)\), with inverse \(\operatorname {inl}(v) \mapsto \operatorname {vertex}(v)\) and \(\operatorname {inr}(e) \mapsto \operatorname {edge}(e)\). Both compositions are the identity by case analysis. Rewriting the cardinality via this equivalence and applying the formula for the cardinality of a sum type gives \(|V| + |E|\).

Definition 526 Space-Fault
#

A space-fault over qubit types \(V, E\) is a structure consisting of:

  • qubit : \(\texttt{QubitLoc}(V, E)\) — the qubit where the error occurs,

  • time : \(\mathbb {N}\) — the time step when the error occurs,

  • pauliType : \(\texttt{PauliType}\) — the type of Pauli error (\(I\), \(X\), \(Y\), or \(Z\)).

Definition 527 Space-Fault Identity
#

The identity space-fault at a given qubit location \(q\) and time \(t\) is \(\langle q, t, I \rangle \), representing no error.

Definition 528 Space-Fault isActualError
#

A space-fault \(f\) represents an actual error if \(\operatorname {isError}(f.\texttt{pauliType}) = \text{true}\), i.e., the Pauli type is not \(I\).

Definition 529 Space-Fault Composition
#

Given two space-faults \(f\) and \(g\) at the same qubit and time (i.e., \(f.\texttt{qubit} = g.\texttt{qubit}\) and \(f.\texttt{time} = g.\texttt{time}\)), their composition is:

\[ f \circ g = \langle f.\texttt{qubit},\; f.\texttt{time},\; f.\texttt{pauliType} \cdot g.\texttt{pauliType} \rangle . \]
Definition 530 Space-Fault Inverse
#

The inverse of a space-fault \(f\) is \(\langle f.\texttt{qubit},\; f.\texttt{time},\; f.\texttt{pauliType}^{-1} \rangle \). Since Pauli operators are self-inverse, \(f^{-1}\) has the same Pauli type as \(f\).

Definition 531 Space-Fault on Vertex
#

A space-fault on a vertex qubit \(v\) at time \(t\) with Pauli type \(p\) is \(\langle \operatorname {vertex}(v), t, p \rangle \).

Definition 532 Space-Fault on Edge
#

A space-fault on an edge qubit \(e\) at time \(t\) with Pauli type \(p\) is \(\langle \operatorname {edge}(e), t, p \rangle \).

Definition 533 Time-Fault
#

A time-fault (measurement error) over measurement type \(M\) is a structure consisting of:

  • measurement : \(M\) — the measurement that is affected,

  • time : \(\mathbb {N}\) — the time step when the measurement occurs,

  • isFlipped : \(\texttt{Bool}\) — whether the classical outcome is flipped (\(\text{true}\) means error).

Definition 534 Time-Fault Identity
#

The identity time-fault at measurement \(m\) and time \(t\) is \(\langle m, t, \text{false} \rangle \), representing no measurement error.

Definition 535 Time-Fault Active
#

An active time-fault at measurement \(m\) and time \(t\) is \(\langle m, t, \text{true} \rangle \), representing a flipped measurement outcome.

Definition 536 Time-Fault isActualError
#

A time-fault \(f\) represents an actual error if \(f.\texttt{isFlipped} = \text{true}\).

Definition 537 Time-Fault Composition
#

Given two time-faults \(f\) and \(g\) at the same measurement and time, their composition is:

\[ f \circ g = \langle f.\texttt{measurement},\; f.\texttt{time},\; f.\texttt{isFlipped} \oplus g.\texttt{isFlipped} \rangle , \]

where \(\oplus \) denotes XOR (exclusive or).

Definition 538 Time-Fault Inverse
#

The inverse of a time-fault \(f\) is \(f\) itself, since flipping is self-inverse (\(\text{flip} \oplus \text{flip} = \text{false}\)).

Definition 539 Initialization Fault
#

An initialization fault over qubit types \(V, E\) is a structure consisting of:

  • qubit : \(\texttt{QubitLoc}(V, E)\) — the qubit being initialized,

  • time : \(\mathbb {N}\) — the time step of initialization,

  • effectiveError : \(\texttt{PauliType}\) — the effective Pauli error applied after perfect initialization.

A faulty initialization of state \(|\psi \rangle \) is modeled as perfect initialization followed by an immediate space-fault.

Definition 540 Initialization Fault to Space-Fault

An initialization fault \(f\) is converted to an equivalent space-fault:

\[ f.\operatorname {toSpaceFault} = \langle f.\texttt{qubit},\; f.\texttt{time},\; f.\texttt{effectiveError} \rangle . \]

The space-fault occurs at the same qubit and time as the initialization.

Definition 541 Initialization Fault Identity

The identity initialization fault at qubit \(q\) and time \(t\) is \(\langle q, t, I \rangle \), representing no error during initialization.

Definition 542 Initialization Fault isActualError

An initialization fault \(f\) represents an actual error if \(\operatorname {isError}(f.\texttt{effectiveError}) = \text{true}\).

Definition 543 Spacetime Fault
#

A spacetime fault over qubit types \(V, E\) and measurement type \(M\) is a structure consisting of:

  • \(\texttt{spaceErrors} : \texttt{QubitLoc}(V, E) \to \mathbb {N} \to \texttt{PauliType}\) — the Pauli error at each (qubit, time) location; identity means no error.

  • \(\texttt{timeErrors} : M \to \mathbb {N} \to \texttt{Bool}\) — whether each (measurement, time) has a flipped outcome; \(\text{false}\) means no error.

This functional representation allows efficient pointwise composition.

Definition 544 Spacetime Fault Identity
#

The identity spacetime fault has no errors anywhere:

\[ \texttt{spaceErrors}(q, t) = I \quad \text{and} \quad \texttt{timeErrors}(m, t) = \text{false} \]

for all qubits \(q\), measurements \(m\), and times \(t\).

Definition 545 Spacetime Fault Composition
#

The composition of spacetime faults \(f\) and \(g\) is defined pointwise:

\begin{align} (f \cdot g).\texttt{spaceErrors}(q, t) & = f.\texttt{spaceErrors}(q, t) \cdot g.\texttt{spaceErrors}(q, t), \\ (f \cdot g).\texttt{timeErrors}(m, t) & = f.\texttt{timeErrors}(m, t) \oplus g.\texttt{timeErrors}(m, t). \end{align}
Definition 546 Spacetime Fault Inverse
#

The inverse of a spacetime fault \(f\) is:

\begin{align} f^{-1}.\texttt{spaceErrors}(q, t) & = (f.\texttt{spaceErrors}(q, t))^{-1}, \\ f^{-1}.\texttt{timeErrors}(m, t) & = f.\texttt{timeErrors}(m, t), \end{align}

since Pauli operators are self-inverse and XOR is self-inverse.

Theorem 547 Spacetime Fault Associativity

For all spacetime faults \(a, b, c\), we have \((a \cdot b) \cdot c = a \cdot (b \cdot c)\).

Proof

By extensionality, it suffices to show equality at each \((q, t)\) for space errors and each \((m, t)\) for time errors. For space errors, we apply associativity of Pauli multiplication. For time errors, we verify by case analysis on the boolean values of \(a.\texttt{timeErrors}(q, t)\), \(b.\texttt{timeErrors}(q, t)\), and \(c.\texttt{timeErrors}(q, t)\) that XOR is associative; each of the eight cases holds by reflexivity.

Theorem 548 Spacetime Fault Left Identity

For all spacetime faults \(f\), \(1 \cdot f = f\).

Proof

By extensionality. For space errors, \(I \cdot f.\texttt{spaceErrors}(q, t) = f.\texttt{spaceErrors}(q, t)\) by left identity of Pauli multiplication. For time errors, \(\text{false} \oplus f.\texttt{timeErrors}(m, t) = f.\texttt{timeErrors}(m, t)\) by simplification.

Theorem 549 Spacetime Fault Right Identity

For all spacetime faults \(f\), \(f \cdot 1 = f\).

Proof

By extensionality. For space errors, \(f.\texttt{spaceErrors}(q, t) \cdot I = f.\texttt{spaceErrors}(q, t)\) by right identity. For time errors, \(f.\texttt{timeErrors}(m, t) \oplus \text{false} = f.\texttt{timeErrors}(m, t)\) by simplification.

Theorem 550 Spacetime Fault Inverse Cancellation

For all spacetime faults \(f\), \(f^{-1} \cdot f = 1\).

Proof

By extensionality. For space errors, \((f.\texttt{spaceErrors}(q, t))^{-1} \cdot f.\texttt{spaceErrors}(q, t) = I\) by the left inverse cancellation of Pauli types. For time errors, \(f.\texttt{timeErrors}(q, t) \oplus f.\texttt{timeErrors}(q, t) = \text{false}\) holds by case analysis on the boolean value (both cases yield \(\text{false}\) by reflexivity).

Definition 551 Spacetime Fault from Space-Fault

Given a single space-fault \(f\), the corresponding spacetime fault has:

\[ \texttt{spaceErrors}(q, t) = \begin{cases} f.\texttt{pauliType} & \text{if } q = f.\texttt{qubit} \text{ and } t = f.\texttt{time}, \\ I & \text{otherwise}, \end{cases} \]

and \(\texttt{timeErrors}(m, t) = \text{false}\) for all \(m, t\).

Definition 552 Spacetime Fault from Time-Fault

Given a single time-fault \(f\), the corresponding spacetime fault has \(\texttt{spaceErrors}(q, t) = I\) for all \(q, t\), and:

\[ \texttt{timeErrors}(m, t) = \begin{cases} f.\texttt{isFlipped} & \text{if } m = f.\texttt{measurement} \text{ and } t = f.\texttt{time}, \\ \text{false} & \text{otherwise}. \end{cases} \]
Definition 553 Spacetime Fault from Initialization Fault

Given an initialization fault \(f\), the corresponding spacetime fault is obtained by first converting \(f\) to its equivalent space-fault via \(\operatorname {toSpaceFault}\), then embedding it via \(\operatorname {fromSpaceFault}\).

Definition 554 Space Error Locations

Given a spacetime fault \(f\) and a set of time steps \(T\), the set of space error locations is:

\[ \{ (q, t) \in \texttt{QubitLoc}(V,E) \times T \mid f.\texttt{spaceErrors}(q, t) \neq I\} . \]
Definition 555 Time Error Locations
#

Given a spacetime fault \(f\) and a set of time steps \(T\), the set of time error locations is:

\[ \{ (m, t) \in M \times T \mid f.\texttt{timeErrors}(m, t) = \text{true}\} . \]
Definition 556 Spacetime Fault Weight
#

The weight of a spacetime fault \(f\) over a set of time steps \(T\) is the total number of non-trivial errors:

\[ \operatorname {weight}(f, T) = |\operatorname {spaceErrorLocations}(f, T)| + |\operatorname {timeErrorLocations}(f, T)|. \]
Lemma 557 Weight of Identity is Zero

For any set of time steps \(T\), \(\operatorname {weight}(1, T) = 0\).

Proof

By simplification: the identity spacetime fault has \(\texttt{spaceErrors}(q,t) = I\) for all \(q, t\), so the space error locations filter yields the empty set; similarly \(\texttt{timeErrors}(m,t) = \text{false}\) for all \(m, t\), so the time error locations filter yields the empty set. Both cardinalities are \(0\).

Definition 558 Pure Space Fault
#

A spacetime fault \(f\) is pure space if it has no time errors:

\[ \forall \, m,\, t,\quad f.\texttt{timeErrors}(m, t) = \text{false}. \]
Definition 559 Pure Time Fault
#

A spacetime fault \(f\) is pure time if it has no space errors:

\[ \forall \, q,\, t,\quad f.\texttt{spaceErrors}(q, t) = I. \]
Lemma 560 From Space-Fault is Pure Space

For any space-fault \(f\), the spacetime fault \(\operatorname {fromSpaceFault}(f)\) is pure space.

Proof

By the definition of \(\operatorname {fromSpaceFault}\), all time errors are set to \(\text{false}\). By simplification, the pure space condition holds.

Lemma 561 From Time-Fault is Pure Time

For any time-fault \(f\), the spacetime fault \(\operatorname {fromTimeFault}(f)\) is pure time.

Proof

By the definition of \(\operatorname {fromTimeFault}\), all space errors are set to \(I\). By simplification, the pure time condition holds.

Definition 562 Space Component
#

The space-only component of a spacetime fault \(f\) retains the space errors and sets all time errors to \(\text{false}\):

\[ f.\operatorname {spaceComponent}.\texttt{spaceErrors} = f.\texttt{spaceErrors}, \quad f.\operatorname {spaceComponent}.\texttt{timeErrors}(m, t) = \text{false}. \]
Definition 563 Time Component

The time-only component of a spacetime fault \(f\) sets all space errors to \(I\) and retains the time errors:

\[ f.\operatorname {timeComponent}.\texttt{spaceErrors}(q, t) = I, \quad f.\operatorname {timeComponent}.\texttt{timeErrors} = f.\texttt{timeErrors}. \]
Theorem 564 Spacetime Fault Decomposition

Every spacetime fault \(f\) decomposes as the product of its space and time components:

\[ f = f.\operatorname {spaceComponent} \cdot f.\operatorname {timeComponent}. \]
Proof

By extensionality, it suffices to verify equality at each component. For space errors at \((q, t)\): the product gives \(f.\texttt{spaceErrors}(q, t) \cdot I = f.\texttt{spaceErrors}(q, t)\) by simplification (right identity of Pauli multiplication). For time errors at \((m, t)\): the product gives \(\text{false} \oplus f.\texttt{timeErrors}(q, t)\). By case analysis on \(f.\texttt{timeErrors}(q, t)\): if \(\text{false}\), then \(\text{false} \oplus \text{false} = \text{false}\); if \(\text{true}\), then \(\text{false} \oplus \text{true} = \text{true}\). Both cases hold by reflexivity.

Definition 565 Subgroup of Pure Space-Faults
#

The set of pure space-faults forms a subgroup of \(\texttt{SpacetimeFault}(V, E, M)\):

\[ \operatorname {pureSpaceFaults}(V, E, M) = \{ f \in \texttt{SpacetimeFault}(V, E, M) \mid f.\operatorname {isPureSpace}\} . \]

This is verified to be closed under multiplication (since \(\text{false} \oplus \text{false} = \text{false}\)), contains the identity (which has all time errors \(\text{false}\)), and is closed under inversion (since the inverse preserves time errors).

Definition 566 Subgroup of Pure Time-Faults
#

The set of pure time-faults forms a subgroup of \(\texttt{SpacetimeFault}(V, E, M)\):

\[ \operatorname {pureTimeFaults}(V, E, M) = \{ f \in \texttt{SpacetimeFault}(V, E, M) \mid f.\operatorname {isPureTime}\} . \]

This is verified to be closed under multiplication (since \(I \cdot I = I\)), contains the identity (which has all space errors \(I\)), and is closed under inversion (since \(I^{-1} = I\)).