MerLean-example

31 Thm 2: Fault Tolerance of Gauging Measurement

This chapter establishes the main fault tolerance theorem: under appropriate conditions on the Cheeger constant \(h(G) \geq 1\) and sufficient measurement rounds \((t_o - t_i) \geq d\), the spacetime fault-distance \(d_{ST}\) equals exactly \(d\), the distance of the original code. The proof combines the spacetime decoupling lemma (Lem 6), the time fault distance bound (Lem 5), the space distance bound (Lem 2), and the spacetime fault distance lemma (Lem 7).

Definition 1001 Fault Tolerance Configuration
#

A fault tolerance configuration is a structure bundling all preconditions needed to establish \(d_{ST} = d\). It consists 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\) (strong expansion).

Definition 1002 Number of Rounds

Given a fault tolerance configuration \(\mathrm{cfg}\), the number of measurement rounds is defined as

\[ \mathrm{numRounds}(\mathrm{cfg}) := t_o - t_i. \]
Lemma 1003 Number of Rounds is Positive

For any fault tolerance configuration \(\mathrm{cfg}\), \(\mathrm{numRounds}(\mathrm{cfg}) {\gt} 0\).

Proof

Since \(t_i {\lt} t_o\) by assumption, we have \(t_o - t_i {\gt} 0\) by the characterization of positive natural subtraction.

Lemma 1004 Number of Rounds At Least \(d\)

For any fault tolerance configuration \(\mathrm{cfg}\), \(\mathrm{numRounds}(\mathrm{cfg}) \geq d\).

Proof

Unfolding the definition of \(\mathrm{numRounds}\), this is exactly the precondition \(t_o - t_i \geq d\) from the configuration.

Definition 1005 Interval Rounds
#

The interval of measurement rounds for a fault tolerance configuration \(\mathrm{cfg}\) is the finite set \([t_i, t_o) := \mathrm{Ico}(t_i, t_o)\).

Theorem 1006 Space Distance Bound

For any fault tolerance configuration \(\mathrm{cfg}\), if \(h(G) \geq 1\), then

\[ \min (h(G), 1) \cdot d = d. \]
Proof

Let \(h(G) \geq 1\). By simplification using the fact that \(\min (h(G), 1) = 1\) when \(h(G) \geq 1\), the product \(\min (h(G), 1) \cdot d\) reduces to \(1 \cdot d = d\).

Theorem 1007 Time Distance Bound

For any fault tolerance configuration \(\mathrm{cfg}\), \(\mathrm{numRounds}(\mathrm{cfg}) \geq d\).

Proof

This follows directly from the lemma that the number of rounds is at least \(d\).

A spacetime fault \(F\) has a spacetime decomposition with respect to a detector collection \(DC\), base outcomes, logical effect predicate, and configuration \(\mathrm{cfg}\) if there exist spacetime faults \(F_{\mathrm{space}}\) and \(F_{\mathrm{time}}\) such that:

  1. \(F\) is equivalent modulo stabilizers to \(F_{\mathrm{space}} \cdot F_{\mathrm{time}}\),

  2. \(F_{\mathrm{space}}\) is a pure space fault at a single time step \(t_i\), and

  3. \(F_{\mathrm{time}}\) is a pure time fault.

The lower bound case enumeration for a spacetime fault \(F\) consists of two cases:

  • Case 1 (timeNontrivial): There exists a pure time fault \(F_{\mathrm{time}}\) with \(\mathrm{weight}(F_{\mathrm{time}}) \geq \mathrm{numRounds}\) and \(\mathrm{weight}(F) \geq \mathrm{weight}(F_{\mathrm{time}})\).

  • Case 2 (spaceLogical): There exists a pure space fault \(F_{\mathrm{space}}\) at time \(t_i\) with \(\mathrm{weight}(F_{\mathrm{space}}) \geq d\) and \(\mathrm{weight}(F) \geq \mathrm{weight}(F_{\mathrm{space}})\).

Theorem 1010 Lower Bound Case 1

When the time component \(F_{\mathrm{time}}\) is nontrivial, i.e., \(\mathrm{weight}(F_{\mathrm{time}}) \geq \mathrm{numRounds}\) and \(\mathrm{weight}(F) \geq \mathrm{weight}(F_{\mathrm{time}})\), then \(\mathrm{weight}(F) \geq d\).

Proof

By a chain of inequalities:

\[ \mathrm{weight}(F) \geq \mathrm{weight}(F_{\mathrm{time}}) \geq \mathrm{numRounds} \geq d. \]

The first inequality is the hypothesis \(h\_ F\_ weight\), the second is \(h\_ time\_ weight\), and the third follows from \(\mathrm{numRounds} \geq d\).

Theorem 1011 Lower Bound Case 2

When the space component is the dominant contributor, i.e., \(\mathrm{weight}(F_{\mathrm{space}}) \geq d\) and \(\mathrm{weight}(F) \geq \mathrm{weight}(F_{\mathrm{space}})\), then \(\mathrm{weight}(F) \geq d\).

Proof

By a chain of inequalities:

\[ \mathrm{weight}(F) \geq \mathrm{weight}(F_{\mathrm{space}}) \geq d. \]

The first inequality is \(h\_ F\_ weight\) and the second is \(h\_ space\_ weight\).

Every spacetime logical fault \(F\) satisfying a lower bound case has weight at least \(d\):

\[ \mathrm{weight}(F) \geq d. \]
Proof

We consider two cases based on the \(\mathrm{LowerBoundCase}\) enumeration.

  • Case timeNontrivial: We have a pure time fault \(F_{\mathrm{time}}\) with the appropriate weight bounds. The result follows directly from the Case 1 theorem (lowerBound_case1).

  • Case spaceLogical: We have a pure space fault \(F_{\mathrm{space}}\) with the appropriate weight bounds. The result follows directly from the Case 2 theorem (lowerBound_case2).

Definition 1013 Original Logical Operator
#

An original code logical operator consists of:

  • A time step \(t\) of application (should be \({\lt} t_i\) or \({\gt} t_o\)).

  • A map \(\mathrm{vertexPaulis} : V \to \mathrm{PauliType}\) assigning Pauli operators to each vertex qubit.

  • A weight \(w \in \mathbb {N}\).

Definition 1014 Original Logical to Spacetime Fault

The conversion of an original logical operator \(L\) to a spacetime fault assigns:

  • Space errors: For a vertex qubit \(v\) at time \(t\), the error is \(L.\mathrm{vertexPaulis}(v)\) if \(t = L.\mathrm{time}\), and \(I\) otherwise. For edge qubits, the error is always \(I\).

  • Time errors: All time errors are \(\mathrm{false}\) (no measurement errors).

Theorem 1015 Weight of Original Logical as Spacetime Fault

If \(L.\mathrm{time} \in \mathrm{times}\), then

\[ \mathrm{weight}(L.\mathrm{toSpacetimeFault}, \mathrm{times}) = |\{ v \in V \mid L.\mathrm{vertexPaulis}(v) \neq I\} |. \]
Proof

We unfold the weight definition. First, we show the time error locations are empty: by definition, all time errors of \(L.\mathrm{toSpacetimeFault}\) are \(\mathrm{false}\), so filtering the product set yields the empty set. We rewrite with this, obtaining \(|\emptyset | + 0 = 0\), reducing the weight to the space error count.

For the space errors, we show that \(L.\mathrm{toSpacetimeFault}.\mathrm{spaceErrorLocations}(\mathrm{times})\) equals the image of \(\{ v \in V \mid L.\mathrm{vertexPaulis}(v) \neq I\} \) under the embedding \(v \mapsto (\mathrm{vertex}(v), L.\mathrm{time})\). The forward direction proceeds by case analysis on the qubit location: for vertex qubits, the error is non-identity only when \(t = L.\mathrm{time}\); for edge qubits, the error is always \(I\), giving a contradiction. The reverse direction verifies that the embedded pair satisfies the membership condition. Finally, we apply the fact that the cardinality of a mapped finset equals the cardinality of the original.

Theorem 1016 Upper Bound: Existence of Weight-\(d\) Logical Fault

Given an original logical operator \(L_{\mathrm{orig}}\) with \(|\{ v \mid L_{\mathrm{orig}}.\mathrm{vertexPaulis}(v) \neq I\} | = d\), applied at time \(L_{\mathrm{orig}}.\mathrm{time} {\lt} t_i\), and assuming \(L_{\mathrm{orig}}.\mathrm{time} \in \mathrm{times}\) and the resulting spacetime fault is a logical fault, there exists a spacetime fault \(F\) that is a spacetime logical fault with \(\mathrm{weight}(F, \mathrm{times}) = d\).

Proof

We take \(F := L_{\mathrm{orig}}.\mathrm{toSpacetimeFault}\). The first condition (logical fault) holds by hypothesis. For the weight, we rewrite using the weight computation theorem for original logicals and the hypothesis that the support has cardinality \(d\).

Main Theorem (Fault Tolerance). Under the conditions:

  1. \(h(G) \geq 1\) (Cheeger constant at least 1),

  2. \((t_o - t_i) \geq d\) (sufficient measurement rounds),

the spacetime fault-distance equals exactly \(d\):

\[ d_{ST} = d. \]

Assuming that every spacetime logical fault \(F\) admits a lower bound case decomposition, and there exists a weight-\(d\) logical fault, then

\[ \mathrm{spacetimeFaultDistance}(DC, \mathrm{baseOutcomes}, \mathrm{logicalEffect}, [t_i, t_o)) = d. \]
Proof

We obtain the weight-\(d\) logical fault \(F_d\) with \(\mathrm{weight}(F_d) = d\) from the existence hypothesis.

Upper bound (\(d_{ST} \leq d\)): By the property that the spacetime fault distance is at most the weight of any logical fault, we have

\[ d_{ST} \leq \mathrm{weight}(F_d) = d. \]

Lower bound (\(d_{ST} \geq d\)): Since \(F_d\) witnesses that logical faults exist, we obtain a minimum-weight logical fault \(F_{\min }\) with \(\mathrm{weight}(F_{\min }) = d_{ST}\) from the property that the spacetime fault distance is achieved. We apply the decomposition hypothesis to \(F_{\min }\) to obtain a lower bound case, then apply the combined lower bound theorem to get \(\mathrm{weight}(F_{\min }) \geq d\). Therefore:

\[ d \leq \mathrm{weight}(F_{\min }) = d_{ST}. \]

Conclusion: Combining \(d \leq d_{ST} \leq d\), we conclude \(d_{ST} = d\) by integer arithmetic (omega).

Corollary 1018 Spacetime Fault Distance is Positive

Under the hypotheses of the Fault Tolerance Theorem,

\[ d_{ST} {\gt} 0. \]
Proof

Rewriting with the Fault Tolerance Theorem, \(d_{ST} = d\). Since \(d {\gt} 0\) by the configuration hypothesis, the result follows.

Corollary 1019 Faults Below \(d\) are Detectable or Stabilizers

Under the hypotheses of the Fault Tolerance Theorem, for any spacetime fault \(F\) with \(\mathrm{weight}(F) {\lt} d\):

\[ \neg \, \mathrm{hasEmptySyndrome}(F) \; \lor \; \neg \, \mathrm{affectsLogicalInfo}(F). \]

That is, \(F\) either triggers a detector (is detectable) or does not affect logical information (is a stabilizer).

Proof

By the Fault Tolerance Theorem, \(d_{ST} = d\). Since \(\mathrm{weight}(F) {\lt} d = d_{ST}\), the result follows from the theorem that faults with weight below the fault distance are either detectable or stabilizers.

Corollary 1020 Fault Correction Threshold

Under the hypotheses of the Fault Tolerance Theorem, for any \(t \in \mathbb {N}\) with \(2t + 1 \leq d\), the code can tolerate \(t\) faults:

\[ \mathrm{canTolerateFaults}(DC, \mathrm{baseOutcomes}, \mathrm{logicalEffect}, [t_i, t_o), t). \]

In particular, the code can correct up to \(\lfloor (d-1)/2\rfloor \) faults.

Proof

We unfold the definition of \(\mathrm{canTolerateFaults}\). Rewriting with the Fault Tolerance Theorem gives \(d_{ST} = d\). The condition \(2t + 1 \leq d\) then directly implies the required inequality by integer arithmetic (omega).

Under the hypotheses of the Fault Tolerance Theorem,

\[ d_{ST} = d \; \Longleftrightarrow \; \left(\forall F,\; \mathrm{IsSpacetimeLogicalFault}(F) \Rightarrow \mathrm{weight}(F) \geq d\right) \; \land \; \left(\exists F,\; \mathrm{IsSpacetimeLogicalFault}(F) \land \mathrm{weight}(F) = d\right). \]
Proof

We prove each direction separately.

\((\Rightarrow )\): Assume \(d_{ST} = d\). For the first conjunct, let \(F\) be any spacetime logical fault. Then \(\mathrm{weight}(F) \geq d_{ST} = d\) by the property that the fault distance is a lower bound on logical fault weights. The second conjunct is provided by the existence hypothesis.

\((\Leftarrow )\): Assume both conditions hold. The result follows directly from the Fault Tolerance Theorem.

Given that the logical effect is group-like, the syndrome is a group homomorphism, and cleaning exists, any spacetime logical fault \(F\) decomposes as \(F \sim F_{\mathrm{space}} \cdot F_{\mathrm{time}}\), where \(F_{\mathrm{space}}\) is a pure space fault at time \(t_i\) and \(F_{\mathrm{time}}\) is a pure time fault.

Proof

This follows directly from the spacetime decoupling lemma (Lem 6), applied with the gauging interval derived from the fault tolerance configuration.

Definition 1023 Algorithm 1 Fault Tolerance Data

A record bundling the data required to apply the fault tolerance theorem to Algorithm 1:

  • A proof that every spacetime logical fault admits a lower bound case decomposition.

  • A witness: a spacetime logical fault of weight exactly \(d\).

Theorem 1024 Algorithm 1 Distance Equals \(d\)

Given \(\mathrm{Algorithm1FaultToleranceData}\), the spacetime fault distance equals \(d\):

\[ \mathrm{spacetimeFaultDistance}(DC, \mathrm{baseOutcomes}, \mathrm{logicalEffect}, [t_i, t_o)) = d. \]
Proof

This follows directly from the Fault Tolerance Theorem applied with the decomposition and existence data from the record.