34 Rem 11: Initial and Final Boundary Conditions
Following standard practice, we use the convention that the initial and final round of stabilizer measurements are perfect. This facilitates clean statements of results and should not be taken literally. The justification is that \(d\) rounds of error correction in the original code before and after the gauging measurement ensure that any error process involving both the gauging measurement and the initial or final boundary condition must have distance greater than \(d\). In practice, the gauging measurement is one component of a larger fault-tolerant quantum computation which determines the appropriate realistic boundary conditions.
An inductive type representing the boundary of the gauging procedure, with two constructors:
initial: the initial round of stabilizer measurements,
final: the final round of stabilizer measurements.
An inductive type describing the quality of measurements at the boundary:
perfect: idealized, error-free measurements,
realistic: measurements subject to noise and errors.
A structure encoding the Perfect Boundary Assumption: the boundary measurements are error-free. It consists of:
initialQuality: the quality of initial boundary measurements (default: perfect),
finalQuality: the quality of final boundary measurements (default: perfect).
The standard convention in which both the initial and final boundaries are perfect:
A structure capturing the configuration of error correction rounds around the gauging measurement. It consists of:
\(d\): the code distance (a positive natural number),
roundsBefore: the number of EC rounds before gauging,
roundsAfter: the number of EC rounds after gauging.
Given a code distance \(d {\gt} 0\), the standard configuration sets roundsBefore \(= d\) and roundsAfter \(= d\).
An error correction configuration provides full protection if
For any \(d {\gt} 0\), the standard error correction configuration \((\texttt{standardErrorCorrectionRounds}\; d)\) provides full protection.
Both conditions hold by reflexivity, since roundsBefore and roundsAfter are both defined to be \(d\).
An abstract error process in the fault-tolerant procedure, consisting of:
weight: the total number of faults,
involvesGauging: whether the process involves the gauging measurement,
involvesInitialBoundary: whether the process involves the initial boundary,
involvesFinalBoundary: whether the process involves the final boundary.
An error process spans to the boundary if it involves the gauging measurement and at least one boundary (initial or final):
An error process spans to the initial boundary if it involves both the gauging measurement and the initial boundary.
An error process spans to the final boundary if it involves both the gauging measurement and the final boundary.
Let \(\textit{ec}\) be an error correction configuration providing full protection, and let \(\textit{ep}\) be an error process with \(\texttt{weight} {\gt} 0\) that spans to a boundary. Suppose the propagation model holds: if the process involves gauging and the initial boundary then \(\texttt{weight} \geq \texttt{roundsBefore} + 1\), and similarly for the final boundary. Then
We simplify the definition of spansToBoundary using Boolean logic to obtain that involvesGauging holds and either involvesInitialBoundary or involvesFinalBoundary holds. We decompose and consider two cases:
Case 1 (spans to initial boundary): From the propagation hypothesis, \(\texttt{weight} \geq \texttt{roundsBefore} + 1\). Since full protection gives \(\texttt{roundsBefore} = d\), we conclude \(\texttt{weight} {\gt} d\) by integer arithmetic.
Case 2 (spans to final boundary): From the propagation hypothesis, \(\texttt{weight} \geq \texttt{roundsAfter} + 1\). Since full protection gives \(\texttt{roundsAfter} = d\), we conclude \(\texttt{weight} {\gt} d\) by integer arithmetic.
Let \(\textit{ec}\) be an error correction configuration providing full protection, and let \(\textit{ep}\) be an error process with \(\texttt{weight} \leq d\). Under the propagation model, \(\textit{ep}\) does not span to any boundary:
We proceed by contradiction. Assume \(\texttt{spansToBoundary}(\textit{ep}) = \texttt{true}\). Simplifying the Boolean expression, we obtain that involvesGauging holds and either involvesInitialBoundary or involvesFinalBoundary holds. We consider two cases:
Case 1 (initial boundary): By the propagation hypothesis, \(\texttt{weight} \geq \texttt{roundsBefore} + 1\). Since \(\texttt{roundsBefore} = d\) by full protection, we get \(\texttt{weight} \geq d + 1\), contradicting \(\texttt{weight} \leq d\).
Case 2 (final boundary): By the propagation hypothesis, \(\texttt{weight} \geq \texttt{roundsAfter} + 1\). Since \(\texttt{roundsAfter} = d\) by full protection, we get \(\texttt{weight} \geq d + 1\), contradicting \(\texttt{weight} \leq d\).
A structure capturing the full boundary condition convention:
a perfect boundary assumption,
an error correction configuration,
a proof that the configuration provides full protection,
a flag indicating this is a simplification (default: true).
For a given code distance \(d {\gt} 0\), the standard boundary condition convention uses perfect boundaries and \(d\) rounds of error correction before and after gauging.
Let \(\textit{conv}\) be a boundary condition convention. For every error process \(\textit{ep}\) such that \(\texttt{spansToBoundary}(\textit{ep}) = \texttt{true}\), under the propagation model (spanning to the initial boundary requires weight \(\geq \texttt{roundsBefore} + 1\), and similarly for the final boundary), we have
Let \(\textit{ep}\) be an error process satisfying the hypotheses. We simplify the definition of spansToBoundary to obtain that involvesGauging holds and either involvesInitialBoundary or involvesFinalBoundary holds. We consider two cases:
Case 1 (initial boundary): By the propagation hypothesis applied to gauging and initial boundary, \(\texttt{weight} \geq \texttt{roundsBefore} + 1\). Since the convention’s full protection gives \(\texttt{roundsBefore} = d\), we obtain \(\texttt{weight} {\gt} d\) by integer arithmetic.
Case 2 (final boundary): By the propagation hypothesis applied to gauging and final boundary, \(\texttt{weight} \geq \texttt{roundsAfter} + 1\). Since the convention’s full protection gives \(\texttt{roundsAfter} = d\), we obtain \(\texttt{weight} {\gt} d\) by integer arithmetic.
A structure describing realistic boundary conditions determined by the surrounding computation context:
a description of the surrounding computation,
the actual initial boundary condition quality,
the actual final boundary condition quality.
The theoretical convention can be replaced by realistic conditions: given a boundary condition convention and a realistic boundary context, the realistic context is returned unchanged (since in practice, the surrounding computation determines the conditions).
Let \(\textit{conv}\) be a boundary condition convention with code distance \(d\). For every error process \(\textit{ep}\) with \(\texttt{weight} \leq d\), under the propagation model, the error cannot span to any boundary:
This captures the fact that boundary quality is irrelevant for low-weight errors.
Let \(\textit{ep}\) be an error process with \(\texttt{weight} \leq d\). We first establish that \(\texttt{weight} \leq \textit{conv}.\texttt{ecConfig}.\texttt{codeDistance}\) by integer arithmetic (since \(d = \textit{conv}.\texttt{ecConfig}.\texttt{codeDistance}\)). The result then follows directly from the theorem low_weight_cannot_span_boundary applied to \(\textit{conv}.\texttt{ecConfig}\), \(\textit{conv}.\texttt{fullProtection}\), and the propagation hypotheses.
The initial boundary occurs at time \(t_0 = \texttt{config.t\_ start}\), the start of the procedure.
The final boundary occurs at time \(t_{\mathrm{final}} = \texttt{config.t\_ final}\).
The gauging measurement occurs at times in the range
The time separation between the initial boundary and the start of gauging, defined as \((t_{\mathrm{initial}} - t_{\mathrm{start}})\) converted to a natural number.
The time separation between the end of gauging and the final boundary. Since the final boundary is at \(t_{\mathrm{final}}\), this is defined to be \(0\).
If \(t_{\mathrm{initial}} - t_{\mathrm{start}} = \texttt{roundsBefore}\) for an error correction configuration \(\textit{ec}\), then the initial boundary separation equals \(\texttt{roundsBefore}\):
We unfold the definition of initialBoundarySeparation. Rewriting using the hypothesis \(t_{\mathrm{initial}} - t_{\mathrm{start}} = \texttt{roundsBefore}\), the result follows from the fact that converting a natural number cast to an integer back to a natural number yields the original value (Int.toNat_natCast).