Let \((q_1, h_{q_1})\) and \((q_2, h_{q_2})\) be elements of the support with \(\operatorname {mkSpaceFault}(P, t, q_1) = \operatorname {mkSpaceFault}(P, t, q_2)\). By simplification using the definition of \(\operatorname {mkSpaceFault}\) and the injectivity equation for the space fault constructor, we extract that \(q_1 = q_2\), hence the subtypes are equal by extensionality.

Unfolding the definition of \(\operatorname {spaceFaultsOfPauliOp}\), we rewrite using the fact that the image of an injective function preserves cardinality (applying \(\operatorname {mkSpaceFault\_ injective}\)), and then the cardinality of the attached finset equals the cardinality of the support.

Unfolding the definitions of \(\operatorname {spacetimeFaultOfDeformedLogical}\), spacetime fault weight, and Pauli operator weight, then simplifying using the cardinality result \(\operatorname {spaceFaultsOfPauliOp\_ card}\), we obtain the equality.

Unfolding the definitions of \(\operatorname {spacetimeFaultOfDeformedLogical}\) and \(\operatorname {isPureSpace}\), the time-faults component is \(\emptyset \) by construction, so this holds by reflexivity.

Let \(\operatorname {idx}\) be an arbitrary detector index. The time-faults of the space-fault witness are \(\emptyset \) by definition. Rewriting with this fact, the result follows from the theorem that no detector is violated when there are no faults.

By extensionality, it suffices to show equality for each qubit \(q\) in both the \(\operatorname {xVec}\) and \(\operatorname {zVec}\) components.

For the \(\operatorname {xVec}\) component: we simplify the definitions of \(\operatorname {pauliErrorAt}\), \(\operatorname {spaceFaultsAt}\), and \(\operatorname {spacetimeFaultOfDeformedLogical}\). Since all space faults have time \(t_i\), the filter selecting faults at time \(t_i\) returns the full set \(\operatorname {spaceFaultsOfPauliOp}(P, t_i)\). We then perform case analysis on whether \(q \in \operatorname {support}(P)\):

• If \(q \in \operatorname {support}(P)\): there is exactly one fault at qubit \(q\) (namely \(\operatorname {mkSpaceFault}(P, t_i, q)\)). Using \(\operatorname {sum\_ eq\_ single\_ of\_ mem}\), the sum reduces to the single term, which by definition of \(\operatorname {mkSpaceFault}\) gives \(P.\operatorname {xVec}(q)\). All other faults \(f\) with \(f.\operatorname {qubit} \neq q\) contribute zero, as shown by the uniqueness property of the space faults.

• If \(q \notin \operatorname {support}(P)\): then \(P.\operatorname {xVec}(q) = 0\) (from the support membership characterization), and every fault \(f\) in the finset has \(f.\operatorname {qubit} \neq q\) (otherwise \(q\) would be in the support), so each term in the sum is zero.

The \(\operatorname {zVec}\) component follows by a symmetric argument.

We verify the two conditions of \(\operatorname {IsFullGaugingLogicalFault}\). The syndrome-free condition follows from \(\operatorname {spacetimeFaultOfDeformedLogical\_ syndromeFree}\). For the second condition, suppose for contradiction that the fault is outcome-preserving, i.e., that \(\operatorname {pauliErrorAt}\) at \(t_i\) is in the stabilizer group. Rewriting with \(\operatorname {spacetimeFaultOfDeformedLogical\_ pauliErrorAt}\), this would mean \(P\) is in the stabilizer group, contradicting the fact that \(P\) is a logical operator (which by definition is not in the stabilizer group).

We establish that the deformed code equals the constructed deformed stabilizer code by definition. The lift of \(P\) (a pure-\(X\) logical of the original code) to the extended qubit space is a logical of the deformed code, by \(\operatorname {liftToExtended\_ isLogical}\).

Let \(F := \operatorname {spacetimeFaultOfDeformedLogical}(\operatorname {liftToExtended}(P))\) be the space-fault witness. By \(\operatorname {spaceFaultWitness\_ isFullLogicalFault}\), \(F\) is a full gauging logical fault. Then:

where the first inequality uses \(\operatorname {gaugingSpacetimeFaultDistance\_ le}\), the first equality uses \(\operatorname {spacetimeFaultOfDeformedLogical\_ weight}\), the second uses \(\operatorname {liftToExtended\_ weight}\), the third uses the hypothesis \(\operatorname {weight}(P) = d_{\text{orig}}\), and the last uses \(d_{\text{orig}} = d\).

We rewrite \(\operatorname {PreservesGaugingSign}\) and express \(\operatorname {gaussSignFlip}\) as a sum of parities over vertices. We show this sum is zero by proving each summand is zero. For each vertex \(v\), by the dichotomy \(\operatorname {gaussFaultCount\_ zero\_ or\_ d}\), the fault count at \(v\) is either \(0\) or \(d\). If it is \(0\), the term vanishes by simplification. If it is \(d\), we rewrite and use the fact that \(d\) is even implies \(d \equiv 0 \pmod{2}\), so the natural number cast to \(\mathbb {Z}/2\mathbb {Z}\) is zero.

Let \(i\) be an arbitrary check index. We need to show \(\operatorname {PauliCommute}(\operatorname {check}(i), P \cdot s)\). Rewriting \(\operatorname {PauliCommute}\) in terms of the symplectic inner product, we use linearity: \(\langle \operatorname {check}(i), P \cdot s \rangle = \langle \operatorname {check}(i), P \rangle + \langle \operatorname {check}(i), s \rangle \). Since \(P\) is in the centralizer, the first term is \(0\). Since \(s\) is in the stabilizer group (hence in the centralizer), the second term is also \(0\). Thus the sum is \(0 + 0 = 0\).

Unfolding the definition of distance as \(\inf \{ \operatorname {weight}(P) \mid P \text{ is logical} \} \), we apply \(\operatorname {Nat.sInf\_ le}\) with the witness \(\langle P, h_{\text{log}}, \operatorname {rfl} \rangle \).

Let \(q \in \operatorname {support}(\operatorname {pauliErrorAt}(F, t))\), so \(\operatorname {xVec}(q) \neq 0\) or \(\operatorname {zVec}(q) \neq 0\). Suppose for contradiction that \(q\) is not in the image, i.e., no fault \(f\) in \(\operatorname {spaceFaultsAt}(F, t)\) has \(f.\operatorname {qubit} = q\). Then both the \(\operatorname {xVec}\) and \(\operatorname {zVec}\) sums at \(q\) are zero (each summand vanishes because the conditional on \(f.\operatorname {qubit} = q\) is false). This contradicts \(q\) being in the support.

Unfolding the definitions of weight and space weight, we compute:

where the first inequality uses \(\operatorname {pauliErrorAt\_ support\_ subset\_ image}\) (subset implies cardinality inequality), the second uses \(\operatorname {card\_ image\_ le}\) (image cardinality \(\leq \) domain cardinality), and the third uses \(\operatorname {card\_ le\_ card}\) since \(\operatorname {spaceFaultsAt}\) is a filter of \(\operatorname {spaceFaults}\).

We decompose \(F = F_S \cdot F_T \cdot S\) via the space-time decomposition (Lem 7), where \(F_S\) is pure-space, \(F_T\) is pure-time and syndrome-free, and \(S\) is a full gauging stabilizer. We perform case analysis on whether \(F_T\) flips the gauging sign \(\sigma \) or \(F_S\) is a nontrivial deformed code logical.

Case (a): \(F_T\) flips \(\sigma \). We first establish that \(F\) itself flips the gauging sign. Using the additivity of \(\operatorname {gaussSignFlip}\) under composition:

where \(\operatorname {gaussSignFlip}(F_S) = 0\) by \(\operatorname {gaussSignFlip\_ pureSpace}\) and \(\operatorname {gaussSignFlip}(S) = 0\) since \(S\) preserves the sign.

The time component \(F^{\text{time}}\) is pure-time, syndrome-free (same time-faults as \(F\)), and flips the sign (by \(\operatorname {space\_ time\_ independent\_ effects}\), the sign flip depends only on time-faults). We then show \(d\) must be odd: if \(d\) were even, then by \(\operatorname {even\_ d\_ no\_ time\_ sign\_ flip}\), \(F_T\) would preserve the sign, contradicting that it flips. Applying \(\operatorname {pureTime\_ logicalFault\_ weight\_ ge\_ d}\):

Case (b): \(F_S\) yields a nontrivial deformed code logical. The deformed code distance satisfies \(d^* \geq d\) by \(\operatorname {sufficient\_ expansion\_ gives\_ dstar\_ ge\_ d}\) (using \(h(G) \geq 1\)).

We compute \(\operatorname {pauliErrorAt}(F, t_i)\) via the decomposition. Using \(\operatorname {pauliErrorAt\_ compose\_ mul}\):

Since \(F_T\) is pure-time, \(\operatorname {pauliErrorAt}(F_T, t_i) = 1\) by \(\operatorname {pureTime\_ pauliError\_ trivial}\). Thus \(\operatorname {pauliErrorAt}(F, t_i) = \operatorname {pauliErrorAt}(F_S, t_i) \cdot \operatorname {pauliErrorAt}(S, t_i)\).

We show \(\operatorname {pauliErrorAt}(F, t_i)\) is a logical of the deformed code. It is in the centralizer by \(\operatorname {inCentralizer\_ mul\_ stabilizerGroup}\) (product of centralizer element and stabilizer element). It is not in the stabilizer group: if \(P \cdot s \in \operatorname {Stab}\), then \(P = (P \cdot s) \cdot s^{-1} \in \operatorname {Stab}\), contradicting that \(F_S\)’s Pauli error is not a stabilizer. Similarly, it is not the identity: if \(P \cdot s = 1\), then \(P = s^{-1} \in \operatorname {Stab}\), again a contradiction.

Therefore:

where the inequalities use \(\operatorname {sufficient\_ expansion\_ gives\_ dstar\_ ge\_ d}\), \(\operatorname {distance\_ le\_ weight\_ of\_ isLogicalOp}\), \(\operatorname {pauliErrorAt\_ weight\_ le\_ spaceWeight}\), and \(\operatorname {spaceWeight\_ le\_ weight}\) respectively.

We first verify that the deformed code has logical operators by constructing the lift: \(\operatorname {liftToExtended}(P)\) is a logical of the deformed code by \(\operatorname {liftToExtended\_ isLogical}\). This establishes that the set of gauging logical fault weights is nonempty (the space-fault witness provides a member via \(\operatorname {spaceFaultWitness\_ isFullLogicalFault}\)).

We then apply \(\operatorname {le\_ csInf}\) to the nonempty set: for every \(w\) in the set of logical fault weights, there exists a fault \(F\) with \(\operatorname {weight}(F) = w\) that is a full gauging logical fault. By \(\operatorname {fullLogicalFault\_ weight\_ ge\_ d}\), \(d \leq \operatorname {weight}(F) = w\).

We apply antisymmetry of \(\leq \). The upper bound \(d_{\text{spacetime}} \leq d\) follows from \(\operatorname {spacetimeFaultDistance\_ le\_ d}\), and the lower bound \(d \leq d_{\text{spacetime}}\) follows from \(\operatorname {spacetimeFaultDistance\_ ge\_ d}\).

Rewriting with \(\operatorname {spacetimeFaultDistance\_ eq\_ d}\), the goal becomes \(0 {\lt} d\), which holds by the positivity assumption \(d {\gt} 0\) from the procedure.

We first establish that \(\operatorname {weight}(F) {\lt} d_{\text{spacetime}}\) by rewriting \(d_{\text{spacetime}} = d\) using \(\operatorname {spacetimeFaultDistance\_ eq\_ d}\), combined with the hypothesis \(\operatorname {weight}(F) {\lt} d\). The result then follows directly from \(\operatorname {syndromeFree\_ gauging\_ weight\_ lt\_ is\_ stabilizer}\), which states that any syndrome-free fault of weight below the spacetime fault-distance is a stabilizer.

Rewriting with \(\operatorname {spacetimeFaultDistance\_ eq\_ d}\), the goal becomes \(d = t_{\text{phase3}} - t_{\text{phase2}}\), which holds by the symmetry of \(\operatorname {phase2\_ duration}\).

This follows directly from \(\operatorname {sufficient\_ expansion\_ gives\_ dstar\_ ge\_ d}\), applied with the deformed code data.