29 Lem 7: Spacetime Fault-Distance Lemma
This chapter formalizes the Spacetime Fault-Distance Lemma: the spacetime fault-distance of the fault-tolerant gauging measurement procedure equals exactly \(d\) (the distance of the original code), provided the Cheeger constant \(h(G) \geq 1\) and the number of measurement rounds satisfies \((t_o - t_i) \geq d\).
A fault distance configuration is a structure consisting of:
A code distance \(d \in \mathbb {N}\) with \(d {\gt} 0\),
An initial time \(t_i\) and final time \(t_o\) with \(t_i {\lt} t_o\) (the deformation interval is nonempty),
The condition \((t_o - t_i) \geq d\) (sufficient measurement rounds),
A Cheeger constant \(h(G) \in \mathbb {R}\) with \(h(G) \geq 1\).
Given a fault distance configuration \(\mathrm{cfg}\), the number of rounds is defined as
For any fault distance configuration \(\mathrm{cfg}\), \(0 {\lt} \mathrm{numRounds}\).
Since \(t_i {\lt} t_o\) by assumption, we have \(t_o - t_i {\gt} 0\) by the characterization of positive natural subtraction.
For any fault distance configuration \(\mathrm{cfg}\), \(\mathrm{numRounds} \geq d\).
Unfolding the definition of \(\mathrm{numRounds}\), this is exactly the hypothesis \(\mathrm{rounds\_ ge\_ d}\): \(t_o - t_i \geq d\).
For any fault distance configuration \(\mathrm{cfg}\), \(t_i \leq t_o\).
This follows directly from \(t_i {\lt} t_o\).
For any fault distance configuration \(\mathrm{cfg}\), \(h(G) \geq 0\).
Since \(0 \leq 1\) and \(h(G) \geq 1\), by transitivity \(h(G) \geq 0\).
For any fault distance configuration \(\mathrm{cfg}\) with \(h(G) \geq 1\), \(\min (h(G), 1) = 1\).
Since \(h(G) \geq 1\), we have \(\min (h(G), 1) = 1\) by the characterization of minimum when the left argument is at least the right.
Given a fault distance configuration \(\mathrm{cfg}\), define the corresponding deformation interval with initial time \(t_i\), final time \(t_o\), and the proof that \(t_i {\lt} t_o\).
A cleaning preserves parity structure, for a fault \(F\) and its cleaned version \(F_{\mathrm{cleaned}}\), asserts:
Equivalence: There exists a spacetime stabilizer \(S\) such that \(F_{\mathrm{cleaned}} = F \cdot S\).
Parity preservation: For each spatial position \(q\), there exists \(k \in \mathbb {N}\) such that for any set of times, the number of non-identity Pauli faults in \(F_{\mathrm{cleaned}}\) plus the number in \(F\) at position \(q\) equals \(2k\) (i.e., has constant parity).
If cleaning preserves parity, then \(|F| \leq |F_{\mathrm{cleaned}}| + (|F| - |F_{\mathrm{cleaned}}|)\).
This follows by integer arithmetic (omega).
A structure asserting that a time fault \(F_{\mathrm{time}}\) spans the interval \([t_i, t_o)\):
For every \(t\) with \(t_i \leq t {\lt} t_o\), there exists a measurement \(m\) such that \(F_{\mathrm{time}}\) has a time error at \((m, t)\).
\(F_{\mathrm{time}}\) is a pure time fault (no space errors).
If \(F_{\mathrm{time}}\) is a pure time fault that spans the interval \([t_i, t_o)\), and the interval rounds are contained in the time set, then \(|F_{\mathrm{time}}| \geq \mathrm{numRounds}\).
We unfold the weight definition. Since \(F_{\mathrm{time}}\) is a pure time fault, the space error locations are empty: for each pair \((q, t)\), the pure time hypothesis gives that the space error is the identity. Rewriting with this, the space error count is zero.
For the time error count, we show \(\mathrm{numRounds} \leq |F_{\mathrm{time}}.\mathrm{timeErrorLocations}|\). Let \(\mathrm{interval} = [t_i, t_o)\). For each \(t \in \mathrm{interval}\), the spanning hypothesis gives a measurement \(m\) with \(F_{\mathrm{time}}.\mathrm{timeErrors}(m, t) = \mathrm{true}\), and the interval inclusion hypothesis ensures \(t \in \mathrm{times}\), so \((m, t) \in F_{\mathrm{time}}.\mathrm{timeErrorLocations}(\mathrm{times})\).
We define a function \(f\) mapping each \(t \in \mathrm{interval}\) to the pair \((\mathrm{Classical.choose}(\ldots ), t)\). This function is injective on the interval since the second component determines \(t\). Its image is contained in the time error locations. By the injection cardinality bound:
If \(F\) is a spacetime logical fault, \(F\) decomposes as \(F = F_{\mathrm{space}} \cdot F_{\mathrm{time}} \cdot S\) for some stabilizer \(S\), \(F_{\mathrm{time}}\) is a nontrivial spacetime logical fault that spans the interval \([t_i, t_o)\), and \(|F| \geq |F_{\mathrm{time}}|\), then \(|F| \geq d\).
If \(F\) is a spacetime logical fault equivalent to a pure space fault \(F_{\mathrm{space}}\) at time \(t_i\) (modulo a stabilizer \(S\)), \(|F_{\mathrm{space}}| \geq d\) (from the space distance bound with \(h(G) \geq 1\)), and \(|F| \geq |F_{\mathrm{space}}|\) (cleaning preserves weight), then \(|F| \geq d\).
By a chain of inequalities:
The first inequality is the weight preservation hypothesis. The second is the space weight hypothesis.
An inductive type capturing the decomposition from the Spacetime Decoupling Lemma (Lem 6) and the resulting case analysis. For a spacetime logical fault \(F\):
Case 1 (timeNontrivial): There exist \(F_{\mathrm{space}}\), \(F_{\mathrm{time}}\), and a stabilizer \(S\) with \(F = F_{\mathrm{space}} \cdot F_{\mathrm{time}} \cdot S\), where \(F_{\mathrm{time}}\) is a nontrivial spacetime logical fault that spans the interval, and \(|F| \geq |F_{\mathrm{time}}|\).
Case 2 (spaceOnly): There exists \(F_{\mathrm{space}}\) which is a pure space fault at time \(t_i\) and a stabilizer \(S\) with \(F = F_{\mathrm{space}} \cdot S\), where \(|F_{\mathrm{space}}| \geq d\) and \(|F| \geq |F_{\mathrm{space}}|\).
Every spacetime logical fault \(F\) satisfies \(|F| \geq d\), provided the interval rounds are contained in the time set and \(F\) admits a spacetime decomposition case.
We perform case analysis on the decomposition case:
Case 1 (timeNontrivial): With \(F_{\mathrm{space}}\), \(F_{\mathrm{time}}\), the decomposition, the time logical fault property, the time spanning property, and the weight relationship, we apply the Case 1 lower bound (Theorem 965) to conclude \(|F| \geq d\).
Case 2 (spaceOnly): With \(F_{\mathrm{space}}\), the pure space property, the equivalence, the space weight bound, and the weight preservation, we apply the Case 2 lower bound (Theorem 966) to conclude \(|F| \geq d\).
An original logical operator applied at a specific time consists of:
A time step \(t\) (intended to be outside the deformation region),
A Pauli assignment \(\mathrm{vertexPaulis} : V \to \mathrm{PauliType}\) on each vertex qubit,
A weight \(w \in \mathbb {N}\) equal to \(|\{ v : \mathrm{vertexPaulis}(v) \neq I\} |\).
Given an original logical operator \(L\) applied at time \(t\), define the corresponding spacetime fault:
Space errors: at qubit \(q\) and time \(t'\), the error is \(L.\mathrm{vertexPaulis}(v)\) if \(q\) is a vertex \(v\) and \(t' = t\), and is \(I\) otherwise (including all edge qubits).
Time errors: identically false (no measurement errors).
If \(L.\mathrm{time} \in \mathrm{times}\), then \(|L.\mathrm{toSpacetimeFault}|_{\mathrm{times}} = L.\mathrm{weight}\).
We unfold the weight definition. First, the time error locations are empty since all time errors are identically false. Rewriting, the time error count is zero and the weight reduces to the space error count.
For the space error locations, we show they equal the image of \(\{ v : L.\mathrm{vertexPaulis}(v) \neq I\} \) under the embedding \(v \mapsto (\mathrm{vertex}(v), L.\mathrm{time})\). In the forward direction: if \((q, t)\) has a non-identity space error, then by the definition of \(\mathrm{toSpacetimeFault}\), \(q\) must be a vertex \(v\) (edge qubits have identity error) and \(t = L.\mathrm{time}\) (otherwise the conditional gives identity). In the reverse direction: if \(v\) has \(L.\mathrm{vertexPaulis}(v) \neq I\), then at \((\mathrm{vertex}(v), L.\mathrm{time})\) the conditional evaluates to a non-identity Pauli.
Taking the cardinality of the image under the injective embedding gives \(|L.\mathrm{toSpacetimeFault}.\mathrm{spaceErrorLocations}| = |\{ v : L.\mathrm{vertexPaulis}(v) \neq I\} | = L.\mathrm{weight}\).
There exists a spacetime logical fault of weight exactly \(d\). Specifically, given an original code logical operator \(L_{\mathrm{orig}}\) of weight \(d\) applied at a time outside the deformation region (either \(t {\lt} t_i\) or \(t {\gt} t_o\)) that produces a spacetime logical fault, the resulting spacetime fault has weight \(d\).
We exhibit \(L_{\mathrm{orig}}.\mathrm{toSpacetimeFault}\) as the witness. The logical fault property holds by hypothesis. The weight equals \(d\) by rewriting with the weight lemma (Lemma 971) applied with the hypothesis that \(L_{\mathrm{orig}}.\mathrm{time} \in \mathrm{times}\), followed by the hypothesis \(L_{\mathrm{orig}}.\mathrm{weight} = d\).
Under the conditions:
\(h(G) \geq 1\) (strong expansion),
\((t_o - t_i) \geq d\) (sufficient measurement rounds),
the spacetime fault-distance equals exactly \(d\):
We prove both inequalities.
Upper bound (\(d_{\mathrm{ST}} \leq d\)): From the hypothesis, there exists a spacetime logical fault \(F_d\) with \(|F_d| = d\). By the general upper bound property \(d_{\mathrm{ST}} \leq |F|\) for any spacetime logical fault \(F\) (applied via spacetimeFaultDistance_le_weight), we have:
Lower bound (\(d_{\mathrm{ST}} \geq d\)): The existence of \(F_d\) ensures that logical faults exist. By the minimality property (spacetimeFaultDistance_is_min), there exists a minimum-weight logical fault \(F_{\min }\) with \(|F_{\min }| = d_{\mathrm{ST}}\). Since every spacetime logical fault admits a decomposition case (by hypothesis), we apply the combined lower bound (Theorem 968) to \(F_{\min }\) to obtain \(|F_{\min }| \geq d\), hence:
Combining both bounds by integer arithmetic, \(d_{\mathrm{ST}} = d\).
Under the same conditions as the main theorem, \(d_{\mathrm{ST}} {\gt} 0\).
Rewriting \(d_{\mathrm{ST}}\) with the main theorem (Theorem 973), we obtain \(d_{\mathrm{ST}} = d\), and \(d {\gt} 0\) by the configuration hypothesis \(d_{\mathrm{pos}}\).
Under the same conditions, if a spacetime fault \(F\) has \(|F| {\lt} d\), then either \(F\) does not have empty syndrome (it is detectable) or \(F\) does not affect the logical information (it is a stabilizer).
We first establish \(d_{\mathrm{ST}} = d\) using the main theorem (Theorem 973). Since \(|F| {\lt} d = d_{\mathrm{ST}}\), the general detectability theorem (detectable_or_stabilizer_if_weight_lt) gives the desired disjunction: \(F\) either has non-empty syndrome or does not affect the logical.
Under the same conditions, the code can tolerate up to \(t\) faults provided \(2t + 1 \leq d\). That is, \(\mathrm{canTolerateFaults}(\ldots , t)\) holds for any \(t\) with \(2t + 1 \leq d\).
Unfolding the definition of \(\mathrm{canTolerateFaults}\), we need \(2t + 1 \leq d_{\mathrm{ST}}\). Rewriting \(d_{\mathrm{ST}} = d\) using the main theorem (Theorem 973), the result follows from the hypothesis \(2t + 1 \leq d\) by integer arithmetic.