25 Def 7: Space and Time Faults
In the context of fault-tolerant quantum error correction, we formalize the notions of space-faults (Pauli errors on qubits), time-faults (measurement errors), and their combined spacetime-fault model.
A space-fault (or space error) on a qubit set \(Q\) at times \(T\) is a structure consisting of:
a qubit \(q \in Q\) where the error occurs,
a time \(t \in T\) at which the error occurs,
an \(X\)-component \(x \in \mathbb {Z}/2\mathbb {Z}\) (equal to \(1\) if the error has an \(X\) or \(Y\) component, \(0\) otherwise),
a \(Z\)-component \(z \in \mathbb {Z}/2\mathbb {Z}\) (equal to \(1\) if the error has a \(Z\) or \(Y\) component, \(0\) otherwise),
a nontriviality condition: \(x \neq 0\) or \(z \neq 0\).
This encodes a single-qubit Pauli error (\(X\), \(Y\), or \(Z\)) at a specific qubit and time.
A time-fault (or measurement error) on a measurement set \(M\) is a structure consisting of a single field:
a measurement \(m \in M\) whose outcome is reported incorrectly (i.e., \(+1\) is reported as \(-1\) or vice versa).
By convention, state mis-initialization faults are also modeled as time-faults: initializing \(|0\rangle \) but obtaining \(|1\rangle \) is equivalent to a perfect initialization followed by a Pauli \(X\) error.
A spacetime fault on qubit set \(Q\), time set \(T\), and measurement set \(M\) is a structure consisting of:
a finite set \(\texttt{spaceFaults} \subseteq \operatorname {Finset}(\operatorname {SpaceFault}(Q, T))\) of space-faults,
a finite set \(\texttt{timeFaults} \subseteq \operatorname {Finset}(\operatorname {TimeFault}(M))\) of time-faults.
This represents a collection of Pauli errors on qubits at specific times together with measurement errors.
The weight of a spacetime fault \(F\) is the total number of individual faults:
The empty spacetime fault is the fault-free configuration \((\emptyset , \emptyset )\), consisting of no space-faults and no time-faults.
Given a single space-fault \(f\), the spacetime fault \(\operatorname {ofSpaceFault}(f) = (\{ f\} , \emptyset )\) consists of that single space-fault and no time-faults.
Given a single time-fault \(f\), the spacetime fault \(\operatorname {ofTimeFault}(f) = (\emptyset , \{ f\} )\) consists of no space-faults and that single time-fault.
The composition of two spacetime faults \(F_1\) and \(F_2\) is defined via the symmetric difference:
This captures the fact that applying the same error twice cancels it, and flipping an outcome twice restores it.
A spacetime fault \(F\) is pure-space if it has no time-faults: \(\texttt{timeFaults}(F) = \emptyset \).
A spacetime fault \(F\) is pure-time if it has no space-faults: \(\texttt{spaceFaults}(F) = \emptyset \).
The space weight of a spacetime fault \(F\) is \(\operatorname {spaceWeight}(F) = |\texttt{spaceFaults}(F)|\).
The time weight of a spacetime fault \(F\) is \(\operatorname {timeWeight}(F) = |\texttt{timeFaults}(F)|\).
The empty spacetime fault has weight \(0\):
By simplification using the definitions of weight and empty, we have \(|\emptyset | + |\emptyset | = 0\).
For any spacetime fault \(F\):
By simplification using the definitions of weight, spaceWeight, and timeWeight, all three expand to the same sum of cardinalities.
\(\operatorname {spaceWeight}(\operatorname {empty}) = 0\).
By simplification using the definitions of spaceWeight and empty, the cardinality of the empty set is \(0\).
\(\operatorname {timeWeight}(\operatorname {empty}) = 0\).
By simplification using the definitions of timeWeight and empty, the cardinality of the empty set is \(0\).
For any space-fault \(f\):
By simplification using the definitions of weight and ofSpaceFault, we have \(|\{ f\} | + |\emptyset | = 1 + 0 = 1\).
For any time-fault \(f\):
By simplification using the definitions of weight and ofTimeFault, we have \(|\emptyset | + |\{ f\} | = 0 + 1 = 1\).
The empty spacetime fault is pure-space.
By simplification using the definitions of isPureSpace and empty, the time-faults of the empty fault form the empty set.
The empty spacetime fault is pure-time.
By simplification using the definitions of isPureTime and empty, the space-faults of the empty fault form the empty set.
For any space-fault \(f\), \(\operatorname {ofSpaceFault}(f)\) is pure-space.
By simplification using the definitions of isPureSpace and ofSpaceFault, the time-faults component is \(\emptyset \).
For any time-fault \(f\), \(\operatorname {ofTimeFault}(f)\) is pure-time.
By simplification using the definitions of isPureTime and ofTimeFault, the space-faults component is \(\emptyset \).
If \(\texttt{spaceFaults}(F)\) is nonempty, then \(\operatorname {weight}(F) {\gt} 0\).
Unfolding the definition of weight, since \(\texttt{spaceFaults}(F)\) is nonempty we have \(|\texttt{spaceFaults}(F)| {\gt} 0\) by Finset.card_pos. The result follows by integer arithmetic since \(\operatorname {weight}(F) = |\texttt{spaceFaults}(F)| + |\texttt{timeFaults}(F)| \geq |\texttt{spaceFaults}(F)| {\gt} 0\).
If \(\texttt{timeFaults}(F)\) is nonempty, then \(\operatorname {weight}(F) {\gt} 0\).
Unfolding the definition of weight, since \(\texttt{timeFaults}(F)\) is nonempty we have \(|\texttt{timeFaults}(F)| {\gt} 0\) by Finset.card_pos. The result follows by integer arithmetic since \(\operatorname {weight}(F) = |\texttt{spaceFaults}(F)| + |\texttt{timeFaults}(F)| \geq |\texttt{timeFaults}(F)| {\gt} 0\).
For any spacetime faults \(F_1, F_2\):
By extensionality, it suffices to show equality for each component. For the space-faults component, by the definition of compose and membership in the symmetric difference, \(a \in S_1 \mathbin {\triangle } S_2\) if and only if \(a \in S_2 \mathbin {\triangle } S_1\), which follows by propositional logic (tauto). The same argument applies to the time-faults component.
For any spacetime fault \(F\):
By extensionality, it suffices to check each component. For the space-faults, \(a \in S \mathbin {\triangle } S\) if and only if \(a \in \emptyset \), since \(S \mathbin {\triangle } S = \emptyset \) (an element is in \(S\) and not in \(S\), or vice versa, which is always false). This follows by simplification using the definition of compose, empty, and membership in the symmetric difference. The same holds for the time-faults.
For any spacetime fault \(F\):
By extensionality, for each component we have \(\emptyset \mathbin {\triangle } S = S\). This follows by simplification using the definitions of compose and empty and membership in the symmetric difference.
For any spacetime fault \(F\):
By extensionality, for each component we have \(S \mathbin {\triangle } \emptyset = S\). This follows by simplification using the definitions of compose and empty and membership in the symmetric difference.
For any spacetime faults \(F_1, F_2, F_3\):
By extensionality, it suffices to check each component. For the space-faults, we use the definition of compose and membership in the symmetric difference: \(a \in (S_1 \mathbin {\triangle } S_2) \mathbin {\triangle } S_3\) if and only if \(a \in S_1 \mathbin {\triangle } (S_2 \mathbin {\triangle } S_3)\), which follows by propositional logic (tauto). The same argument applies to the time-faults.
The space component of a spacetime fault \(F\) is the spacetime fault \((\texttt{spaceFaults}(F), \emptyset )\), keeping only the space-faults.
The time component of a spacetime fault \(F\) is the spacetime fault \((\emptyset , \texttt{timeFaults}(F))\), keeping only the time-faults.
For any spacetime fault \(F\), the space component \(F.\operatorname {spaceComponent}\) is pure-space.
By simplification using the definitions of spaceComponent and isPureSpace, the time-faults of the space component are \(\emptyset \).
For any spacetime fault \(F\), the time component \(F.\operatorname {timeComponent}\) is pure-time.
By simplification using the definitions of timeComponent and isPureTime, the space-faults of the time component are \(\emptyset \).
For any spacetime fault \(F\):
By simplification using the definitions of spaceComponent, weight, and spaceWeight, the weight of \((\texttt{spaceFaults}(F), \emptyset )\) equals \(|\texttt{spaceFaults}(F)| + 0 = |\texttt{spaceFaults}(F)|\).
For any spacetime fault \(F\):
By simplification using the definitions of timeComponent, weight, and timeWeight, the weight of \((\emptyset , \texttt{timeFaults}(F))\) equals \(0 + |\texttt{timeFaults}(F)| = |\texttt{timeFaults}(F)|\).
Any spacetime fault \(F\) decomposes into the composition of its space and time components:
By extensionality, for the space-faults component we have \(\texttt{spaceFaults}(F) \mathbin {\triangle } \emptyset = \texttt{spaceFaults}(F)\), and for the time-faults component we have \(\emptyset \mathbin {\triangle } \texttt{timeFaults}(F) = \texttt{timeFaults}(F)\). Both follow by simplification using the definitions of compose, spaceComponent, timeComponent, and membership in the symmetric difference.
The space-faults at time \(t\) of a spacetime fault \(F\) is the subset of space-faults whose time field equals \(t\):
The composite Pauli error at time \(t\) of a spacetime fault \(F\) on the qubit system \(Q\) is the Pauli operator \(P \in \operatorname {PauliOp}(Q)\) defined by:
The sums are taken in \(\mathbb {Z}/2\mathbb {Z}\).
For any time \(t\), the Pauli error of the empty fault at time \(t\) is the identity:
By extensionality over all qubits \(q\), for both the \(x\)- and \(z\)-components: the sum is over \(\operatorname {spaceFaultsAt}(\operatorname {empty}, t)\), which by the definitions of spaceFaultsAt and empty is a filter of \(\emptyset \), hence empty. The empty sum in \(\mathbb {Z}/2\mathbb {Z}\) equals \(0\), which matches the identity Pauli operator.
An initialization fault for initialization measurement \(m\) is the spacetime fault \(\operatorname {ofTimeFault}(\langle m \rangle )\), modeling the initialization error as a time-fault on the measurement associated with the initialization.
The equivalent space-fault view of an initialization error on qubit \(q\) at time \(t\): this is \(\operatorname {ofSpaceFault}(\langle q, t, 1, 0, \cdot \rangle )\), representing a perfect initialization followed by a Pauli \(X\) error (since \(x\)-component is \(1\) and \(z\)-component is \(0\)).
For any measurement \(m\):
By simplification using the definitions of initializationFault, ofTimeFault, and weight, we have \(|\emptyset | + |\{ m\} | = 0 + 1 = 1\).
For any qubit \(q\) and time \(t\):
By simplification using the definitions of initializationAsSpaceFault, ofSpaceFault, and weight, we have \(|\{ \langle q, t, 1, 0, \cdot \rangle \} | + |\emptyset | = 1 + 0 = 1\).
For any spacetime fault \(F\):
Unfolding the definitions of weight and spaceWeight, the claim becomes \(|\texttt{spaceFaults}(F)| \leq |\texttt{spaceFaults}(F)| + |\texttt{timeFaults}(F)|\), which follows by integer arithmetic (omega).
For any spacetime fault \(F\):
Unfolding the definitions of weight and timeWeight, the claim becomes \(|\texttt{timeFaults}(F)| \leq |\texttt{spaceFaults}(F)| + |\texttt{timeFaults}(F)|\), which follows by integer arithmetic (omega).
For any spacetime fault \(F\):
By simplification using the definition of weight, \(\operatorname {weight}(F) = 0\) is equivalent to \(|\texttt{spaceFaults}(F)| + |\texttt{timeFaults}(F)| = 0\), which by the fact that a sum of natural numbers is zero if and only if both summands are zero (Nat.add_eq_zero_iff), and the fact that a finset has cardinality zero if and only if it is empty (Finset.card_eq_zero), gives the desired equivalence.
For any spacetime fault \(F\):
We prove both directions. For the forward direction, assume \(\operatorname {weight}(F) = 0\). From the characterization weight_zero_iff, we obtain that \(\texttt{spaceFaults}(F) = \emptyset \) and \(\texttt{timeFaults}(F) = \emptyset \). By extensionality, and simplifying using the definition of empty, \(F = \operatorname {empty}\). For the reverse direction, assume \(F = \operatorname {empty}\). Substituting, we simplify to obtain \(\operatorname {weight}(\operatorname {empty}) = 0\).
A spacetime fault \(F\) is trivial if \(F = \operatorname {empty}\), i.e., it contains no faults at all.
The set of affected qubits of a spacetime fault \(F\) is the image of the space-faults under the qubit projection:
The set of active times of a spacetime fault \(F\) is the image of the space-faults under the time projection:
The set of affected measurements of a spacetime fault \(F\) is the image of the time-faults under the measurement projection:
Given an ideal measurement outcome function \(\operatorname {ideal} : M \to \mathbb {Z}/2\mathbb {Z}\) and a set of time-faults, the observed outcome for measurement \(m\) is:
A time-fault on measurement \(m\) flips the observed outcome.
If measurement \(m\) is not affected by any time-fault (i.e., \(\langle m \rangle \notin \texttt{faults}\)), then the observed outcome equals the ideal outcome:
By simplification using the definition of observedOutcome and the hypothesis \(\langle m \rangle \notin \texttt{faults}\), the conditional evaluates to \(0\), giving \(\operatorname {ideal}(m) + 0 = \operatorname {ideal}(m)\).
If measurement \(m\) is affected by a time-fault (i.e., \(\langle m \rangle \in \texttt{faults}\)), thenthe observed outcome is the ideal outcome plus \(1\):
By simplification using the definition of observedOutcome and the hypothesis \(\langle m \rangle \in \texttt{faults}\), the conditional evaluates to \(1\), giving \(\operatorname {ideal}(m) + 1\).
If measurement \(m\) is affected by a time-fault (i.e., \(\langle m \rangle \in \texttt{faults}\)), then the observed outcome differs from the ideal outcome:
We first rewrite using the lemma observedOutcome_with_fault, so the goal becomes \(\operatorname {ideal}(m) + 1 \neq \operatorname {ideal}(m)\). Assume for contradiction that \(\operatorname {ideal}(m) + 1 = \operatorname {ideal}(m)\). Then subtracting \(\operatorname {ideal}(m)\) from both sides, we obtain \(0 = 1\) in \(\mathbb {Z}/2\mathbb {Z}\), which is simplified to a contradiction since \(0 \neq 1\).