22 Def 12: Time Step Convention
We use a half-integer time step convention for the fault-tolerant gauging measurement procedure. Integer time steps \(t = 0, 1, 2, \ldots \) are associated with qubit states and Pauli space-errors, while half-integer time steps \(t + \tfrac {1}{2}\) are associated with measurements and measurement errors.
A half-integer time representation, defined as an inductive type with two constructors:
\(\mathtt{integer}(n)\) represents the integer time step \(n \in \mathbb {Z}\),
\(\mathtt{halfInteger}(n)\) represents the half-integer time step \(n + \tfrac {1}{2}\) for \(n \in \mathbb {Z}\).
Convert a half-integer time to a rational number for comparison:
A predicate that checks whether a half-integer time is an integer time:
A predicate that checks whether a half-integer time is a half-integer time:
The floor (integer part) of a half-integer time:
The ceiling (rounded-up integer part) of a half-integer time:
For any \(n \in \mathbb {Z}\), we have \(\mathtt{integer}(n) {\lt} \mathtt{halfInteger}(n)\), i.e., \(n {\lt} n + \tfrac {1}{2}\).
We unfold the ordering to the rational comparison \(n {\lt} n + \tfrac {1}{2}\). This follows by linear arithmetic.
For any \(n \in \mathbb {Z}\), we have \(\mathtt{halfInteger}(n) {\lt} \mathtt{integer}(n+1)\), i.e., \(n + \tfrac {1}{2} {\lt} n + 1\).
We unfold the ordering to the rational comparison \(n + \tfrac {1}{2} {\lt} n + 1\). Using the fact that \(\mathrm{cast}(n+1) = \mathrm{cast}(n) + 1\), this follows by linear arithmetic.
The successor function on half-integer times, advancing by \(\tfrac {1}{2}\):
That is, \(n \mapsto n + \tfrac {1}{2}\) and \(n + \tfrac {1}{2} \mapsto n + 1\).
The predecessor function on half-integer times, retreating by \(\tfrac {1}{2}\):
That is, \(n \mapsto n - \tfrac {1}{2}\) and \(n + \tfrac {1}{2} \mapsto n\).
For any half-integer time \(t\), \(\mathrm{pred}(\mathrm{succ}(t)) = t\).
We consider two cases. Case 1: \(t = \mathtt{integer}(n)\). Then \(\mathrm{succ}(t) = \mathtt{halfInteger}(n)\) and \(\mathrm{pred}(\mathtt{halfInteger}(n)) = \mathtt{integer}(n) = t\). This holds by simplification using the definitions of succ and pred. Case 2: \(t = \mathtt{halfInteger}(n)\). Then \(\mathrm{succ}(t) = \mathtt{integer}(n+1)\) and \(\mathrm{pred}(\mathtt{integer}(n+1)) = \mathtt{halfInteger}(n) = t\). This again holds by simplification.
For any half-integer time \(t\), \(\mathrm{succ}(\mathrm{pred}(t)) = t\).
We consider two cases. Case 1: \(t = \mathtt{integer}(n)\). Then \(\mathrm{pred}(t) = \mathtt{halfInteger}(n-1)\) and \(\mathrm{succ}(\mathtt{halfInteger}(n-1)) = \mathtt{integer}(n) = t\). This holds by simplification. Case 2: \(t = \mathtt{halfInteger}(n)\). Then \(\mathrm{pred}(t) = \mathtt{integer}(n)\) and \(\mathrm{succ}(\mathtt{integer}(n)) = \mathtt{halfInteger}(n) = t\). This also holds by simplification.
For any half-integer time \(t\), \(t {\lt} \mathrm{succ}(t)\).
We consider two cases. Case 1: \(t = \mathtt{integer}(n)\). Then \(\mathrm{succ}(t) = \mathtt{halfInteger}(n)\), and \(\mathtt{integer}(n) {\lt} \mathtt{halfInteger}(n)\) follows from the lemma integer_lt_halfInteger_same. Case 2: \(t = \mathtt{halfInteger}(n)\). Then \(\mathrm{succ}(t) = \mathtt{integer}(n+1)\), and \(\mathtt{halfInteger}(n) {\lt} \mathtt{integer}(n+1)\) follows from the lemma halfInteger_lt_integer_succ.
For any half-integer time \(t\), \(\mathrm{pred}(t) {\lt} t\).
We consider two cases. Case 1: \(t = \mathtt{integer}(n)\). Then \(\mathrm{pred}(t) = \mathtt{halfInteger}(n-1)\). We unfold the ordering to the rational comparison \((n-1) + \tfrac {1}{2} {\lt} n\), i.e., \(n - \tfrac {1}{2} {\lt} n\), which follows by linear arithmetic. Case 2: \(t = \mathtt{halfInteger}(n)\). Then \(\mathrm{pred}(t) = \mathtt{integer}(n)\). We unfold to \(n {\lt} n + \tfrac {1}{2}\), which follows by linear arithmetic.
Converts an integer time step \(t\) to the half-integer time \(\mathtt{integer}(t)\).
Converts a measurement time step \(t\) (representing \(t + \tfrac {1}{2}\)) to the half-integer time \(\mathtt{halfInteger}(t)\).
The measurement time immediately after integer time \(t\) is \(t + \tfrac {1}{2}\), represented by the measurement time step \(t\).
The measurement time immediately before integer time \(t\) is \(t - \tfrac {1}{2}\), represented by the measurement time step \(t - 1\).
The integer time immediately after measurement time \(t + \tfrac {1}{2}\) is \(t + 1\).
The integer time immediately before measurement time \(t + \tfrac {1}{2}\) is \(t\).
A measurement at time \(t + \tfrac {1}{2}\) occurs between qubit states at times \(t\) and \(t + 1\). Formally, for any measurement time step \(t\):
The first inequality follows directly from integer_lt_halfInteger_same\((t)\), and the second follows directly from halfInteger_lt_integer_succ\((t)\).
A Pauli error at integer time \(t\) affects the state between measurements at \(t - \tfrac {1}{2}\) and \(t + \tfrac {1}{2}\). Formally:
We prove both conjuncts. For the first, we unfold the ordering to the rational comparison \((t-1) + \tfrac {1}{2} {\lt} t\), which simplifies using \(\mathrm{cast}(t-1) = \mathrm{cast}(t) - 1\) and follows by linear arithmetic. For the second, this is exactly integer_lt_halfInteger_same\((t)\).
A configuration of key time points in the gauging procedure, consisting of:
\(t_{\mathrm{start}}\): the start of the procedure,
\(t_{\mathrm{initial}}\): the time of the initial gauging code deformation,
\(t_{\mathrm{final}}\): the time of the final ungauging code deformation,
subject to the ordering constraint \(t_{\mathrm{start}} \le t_{\mathrm{initial}} \le t_{\mathrm{final}}\).
The total duration of the gauging measurement procedure:
The duration of the gauged phase, from \(t_{\mathrm{initial}}\) to \(t_{\mathrm{final}}\):
The first \(A_v\) measurement time \(t_{\mathrm{initial}} - \tfrac {1}{2}\), represented as measurement time step \(t_{\mathrm{initial}} - 1\).
The second \(A_v\) measurement time \(t_{\mathrm{initial}} + \tfrac {1}{2}\), represented as measurement time step \(t_{\mathrm{initial}}\).
The last \(A_v\) measurement time before the final time \(t_{\mathrm{final}} - \tfrac {1}{2}\), represented as measurement time step \(t_{\mathrm{final}} - 1\).
The final \(A_v\) measurement time \(t_{\mathrm{final}} + \tfrac {1}{2}\), represented as measurement time step \(t_{\mathrm{final}}\).
The first \(A_v\) measurement at \(t_{\mathrm{initial}} - \tfrac {1}{2}\) comes before the integer time \(t_{\mathrm{initial}}\):
We simplify using the definition of firstGaugeMeasurement and unfold the ordering to the rational comparison \((t_{\mathrm{initial}} - 1) + \tfrac {1}{2} {\lt} t_{\mathrm{initial}}\). Using \(\mathrm{cast}(t_{\mathrm{initial}} - 1) = \mathrm{cast}(t_{\mathrm{initial}}) - 1\), this becomes \(t_{\mathrm{initial}} - \tfrac {1}{2} {\lt} t_{\mathrm{initial}}\), which follows by linear arithmetic.
The second \(A_v\) measurement at \(t_{\mathrm{initial}} + \tfrac {1}{2}\) comes after the integer time \(t_{\mathrm{initial}}\):
We simplify using the definition of secondGaugeMeasurement and apply integer_lt_halfInteger_same to \(t_{\mathrm{initial}}\).
The time step convention type, a structure recording:
integerTimesForStates: whether integer times are used for qubit states (default: true),
halfIntegerTimesForMeasurements: whether half-integer times are used for measurements (default: true).
The standard half-integer convention, where integer times are for qubit states and half-integer times are for measurements.
Space faults (Pauli errors) occur at integer times. Given a time step \(t\), the associated half-integer time is \(\mathtt{integer}(t)\).
Time faults (measurement errors) occur at half-integer times. Given a time step \(t\), the associated half-integer time is \(\mathtt{halfInteger}(t)\).
A space fault at time \(t\) (with \(t {\gt} 0\)) is between measurements at \(t - \tfrac {1}{2}\) and \(t + \tfrac {1}{2}\):
We prove both conjuncts. For the first, we simplify using the definition of spaceFaultTime and unfold the ordering to the rational comparison \((t-1) + \tfrac {1}{2} {\lt} t\). Using \(\mathrm{cast}(t-1) = \mathrm{cast}(t) - 1\), this follows by linear arithmetic. For the second, we simplify using spaceFaultTime and apply integer_lt_halfInteger_same to \(t\).
A measurement fault at time \(t + \tfrac {1}{2}\) is between states at times \(t\) and \(t + 1\):
We simplify using the definitions of spaceFaultTime and timeFaultTime. For the first conjunct, \(\mathtt{integer}(t) {\lt} \mathtt{halfInteger}(t)\) follows from integer_lt_halfInteger_same\((t)\). For the second conjunct, we use halfInteger_lt_integer_succ\((t)\), which gives \(\mathtt{halfInteger}(t) {\lt} \mathtt{integer}(t+1)\). After simplification using \(\mathrm{cast}(t+1) = \mathrm{cast}(t) + 1\), this yields the desired inequality.
The set of integer time steps in a range \([t_1, t_2]\):
The set of measurement time steps in a range \([t_1 + \tfrac {1}{2}, t_2 - \tfrac {1}{2}]\):
The set of all half-integer times between integer times \(t_1\) and \(t_2\):