We apply \(\operatorname {Nat.sInf\_ le}\): since \(F\) is a spacetime logical fault, we have \(|F| \in \text{logicalFaultWeights}\) (witnessed by \(\langle F, h_{\mathrm{log}}, \operatorname {rfl}\rangle \)), and therefore \(\inf (\text{logicalFaultWeights}) \le |F|\).

We show the set of logical fault weights is empty. By extensionality, for any \(w\), we simplify the membership condition and note that if \(\langle F, h_{\mathrm{log}}, \_ \rangle \) existed, it would contradict the hypothesis that no logical faults exist. Hence \(\text{logicalFaultWeights} = \emptyset \). Unfolding the definition of \(d_{\mathrm{spacetime}}\) and rewriting with this, we conclude by \(\operatorname {Nat.sInf\_ empty} = 0\).

First, we show \(0 \notin \text{logicalFaultWeights}\): if \(\langle F, h_{\mathrm{log}}, h_w\rangle \) witnessed \(0 \in \text{logicalFaultWeights}\), then by the positivity of the weight of logical faults (since the empty fault is outcome-preserving), we get a contradiction by integer arithmetic. From the existence hypothesis, we obtain \(F\) with \(h_{\mathrm{log}}\), so \(\text{logicalFaultWeights}\) is nonempty (witnessed by \(|F|\)). Rewriting the goal as \(d_{\mathrm{spacetime}} \ne 0\), we assume for contradiction that \(d_{\mathrm{spacetime}} = 0\). By \(\operatorname {Nat.sInf\_ eq\_ zero}\), either \(0 \in \text{logicalFaultWeights}\) (contradicting the above) or \(\text{logicalFaultWeights} = \emptyset \) (contradicting nonemptiness).

Assume for contradiction that \(F\) is a spacetime logical fault. Then by the upper bound theorem, \(d_{\mathrm{spacetime}} \le |F|\), contradicting \(|F| {\lt} d_{\mathrm{spacetime}}\) by integer arithmetic.

Since \(|F| {\lt} d_{\mathrm{spacetime}}\), we have by the previous theorem that \(F\) is not a logical fault. Since \(F\) is syndrome-free, we apply the characterization that a syndrome-free fault is a stabilizer if and only if it is not a logical fault, concluding that \(F\) is a spacetime stabilizer.

From the upper bound theorem, \(d_{\mathrm{spacetime}} \le |F|\). By simplification using the definitions of weight, space weight, and time weight (which gives \(|F| = |F|_{\mathrm{space}} + |F|_{\mathrm{time}}\)), the result follows directly.

We apply \(\operatorname {Nat.sInf\_ le}\): since \(F\) is a gauging logical fault, \(|F| \in \text{gaugingLogicalFaultWeights}\) (witnessed by \(\langle F, h_{\mathrm{log}}, \operatorname {rfl}\rangle \)), and therefore \(\inf (\text{gaugingLogicalFaultWeights}) \le |F|\).

We show the set of gauging logical fault weights is empty. By extensionality, for any \(w\), we simplify the membership condition and note that any witness \(\langle F, h_{\mathrm{log}}, \_ \rangle \) contradicts the hypothesis that no gauging logical faults exist. Hence \(\text{gaugingLogicalFaultWeights} = \emptyset \). Unfolding \(d_{\mathrm{spacetime}}^{\mathrm{gauging}}\) and rewriting, we conclude by \(\operatorname {Nat.sInf\_ empty} = 0\).

First, we show \(0 \notin \text{gaugingLogicalFaultWeights}\). If \(\langle F, h_{\mathrm{log}}, h_w\rangle \) witnessed \(0\) in this set, then unfolding the definition of weight, \(|F.\mathrm{spaceFaults}| + |F.\mathrm{timeFaults}| = 0\), so \(F.\mathrm{spaceFaults} = \emptyset \) and \(F.\mathrm{timeFaults} = \emptyset \) (by \(\operatorname {Finset.card\_ eq\_ zero}\) and integer arithmetic). By cases on \(F\), simplification yields \(F = \text{empty}\), and rewriting in \(h_{\mathrm{log}}\) contradicts the assumption that the empty fault is outcome-preserving (since a logical fault must not be outcome-preserving).

From the existence hypothesis, we obtain \(F\) with \(h_{\mathrm{log}}\), giving nonemptiness of \(\text{gaugingLogicalFaultWeights}\) (witnessed by \(|F|\)). Rewriting the goal as \(d_{\mathrm{spacetime}}^{\mathrm{gauging}} \ne 0\), we assume for contradiction that \(d_{\mathrm{spacetime}}^{\mathrm{gauging}} = 0\). By \(\operatorname {Nat.sInf\_ eq\_ zero}\), either \(0\) is in the set (contradicted above) or the set is empty (contradicted by nonemptiness).

Assume for contradiction that \(F\) is a gauging logical fault. Then \(d_{\mathrm{spacetime}}^{\mathrm{gauging}} \le |F|\) by the upper bound theorem, contradicting \(|F| {\lt} d_{\mathrm{spacetime}}^{\mathrm{gauging}}\) by integer arithmetic.

Since \(|F| {\lt} d_{\mathrm{spacetime}}^{\mathrm{gauging}}\), the previous theorem gives that \(F\) is not a gauging logical fault. We construct the gauging stabilizer proof as the pair of syndrome-freeness and the fact that \(F\) is outcome-preserving: the latter follows by contradiction, since if \(F\) were not outcome-preserving, combined with syndrome-freeness it would constitute a gauging logical fault, contradicting what we just established.

This follows directly from the gauging distance upper bound theorem applied to \(F\).

From the gauging distance upper bound, \(d_{\mathrm{spacetime}}^{\mathrm{gauging}} \le |F|\). By simplification using the definitions of weight, space weight, and time weight (which yields \(|F| = |F|_{\mathrm{space}} + |F|_{\mathrm{time}}\)), the result follows directly.