By extensionality, it suffices to show that for arbitrary \(w\), membership in the left-hand side is equivalent to membership in the right-hand side. We unfold the definitions of logicalFaultWeights, undetectableNonStabilizerWeights, and IsSpacetimeLogicalFault, and simplify the set membership. We prove both directions:

• (\(\Rightarrow \)) Given \(\langle F, \langle h_{\mathrm{empty}}, h_{\mathrm{logical}}\rangle , h_{\mathrm{eq}}\rangle \), we obtain \(\langle F, h_{\mathrm{empty}}, h_{\mathrm{logical}}, h_{\mathrm{eq}}\rangle \) directly.

• (\(\Leftarrow \)) Given \(\langle F, h_{\mathrm{empty}}, h_{\mathrm{logical}}, h_{\mathrm{eq}}\rangle \), we obtain \(\langle F, \langle h_{\mathrm{empty}}, h_{\mathrm{logical}}\rangle , h_{\mathrm{eq}}\rangle \) directly.

This is simply a repackaging of the conjunction.

From the nonemptiness hypothesis, we obtain \(\langle w, F, h_F, \_ \rangle \). Then \(\langle F, h_F \rangle \) witnesses the existential.

From the hypothesis, we obtain \(\langle F, h_F \rangle \). Then \(\langle F.\mathrm{weight}(\mathit{times}),\, F,\, h_F,\, \mathrm{rfl}\rangle \) witnesses nonemptiness.

We unfold the definition of \(\mathrm{spacetimeFaultDistance}\). Since \(F\) is a logical fault, we have \(\mathrm{hasLogicalFault}\) holds. Rewriting with \(\mathrm{dif\_ pos}\), we apply \(\mathrm{WellFounded.min\_ le}\) to the witness \(\langle F, h_F, \mathrm{rfl}\rangle \) showing \(F.\mathrm{weight}(\mathit{times}) \in W\).

This follows directly from Theorem 679.

We unfold the definition of \(\mathrm{spacetimeFaultDistance}\) and rewrite with \(\mathrm{dif\_ pos}\, h\). We establish that the weight set is nonempty by applying \(\mathrm{weights\_ nonempty\_ of\_ hasLogicalFault}\). By \(\mathrm{WellFounded.min\_ mem}\), the minimum is a member of the weight set. Decomposing, we obtain \(\langle F, h_{F,\mathrm{log}}, h_{F,w}\rangle \) and return \(\langle F, h_{F,\mathrm{log}}, h_{F,w}\rangle \).

We unfold the definition of \(\mathrm{spacetimeFaultDistance}\) and rewrite with \(\mathrm{dif\_ neg}\, h\), which selects the sentinel branch returning \(0\).

Assume for contradiction that \(F\) is a spacetime logical fault. By Theorem 679, \(d_{\mathrm{ST}} \leq |F|_{\mathit{times}}\). But \(|F|_{\mathit{times}} {\lt} d_{\mathrm{ST}}\) by hypothesis. By integer arithmetic (omega), this is a contradiction.

Assume for contradiction that both \(\mathrm{hasEmptySyndrome}(\mathit{DC}, F)\) and \(\mathrm{affectsLogicalInfo}(F)\) hold (by pushing the negation inward). Then \(F\) is a spacetime logical fault by definition. This contradicts Theorem 683.

We prove both directions:

• (\(\Rightarrow \)) Assume \(d_{\mathrm{ST}} {\gt} 0\). First, logical faults must exist: otherwise, by Theorem 682, \(d_{\mathrm{ST}} = 0\), contradicting \(d_{\mathrm{ST}} {\gt} 0\) (by \(\mathrm{Nat.not\_ lt\_ zero}\)). Second, for any logical fault \(F\), by Theorem 679, \(d_{\mathrm{ST}} \leq |F|_{\mathit{times}}\), so \(0 {\lt} |F|_{\mathit{times}}\) by integer arithmetic.

• (\(\Leftarrow \)) Assume \(\mathrm{hasLogicalFault}\) and that all logical faults have positive weight. By Theorem 681, there exists \(F\) with \(|F|_{\mathit{times}} = d_{\mathrm{ST}}\) and \(F\) a logical fault. By hypothesis, \(0 {\lt} |F|_{\mathit{times}}\), so \(0 {\lt} d_{\mathrm{ST}}\).

Let \(w \in W\). Then there exists \(F\) with \(h_F\) a proof that \(F\) is a logical fault and \(|F|_{\mathit{times}} = w\). Rewriting with \(h_{\mathrm{eq}}\), the result follows from Theorem 679.

By Theorem 681, there exists \(F\) with \(h_F\) and \(|F|_{\mathit{times}} = d_{\mathrm{ST}}\). Then \(\langle F, h_F, h_{\mathrm{eq}}\rangle \) witnesses membership.

This follows directly from Theorem 681.

We first establish that \(|F|_{\mathit{times}} {\lt} d_{\mathrm{ST}}\): unfolding \(\mathrm{canTolerateFaults}\), we have \(t {\lt} d_{\mathrm{ST}}\) and \(|F|_{\mathit{times}} \leq t\), so by integer arithmetic \(|F|_{\mathit{times}} {\lt} d_{\mathrm{ST}}\). The result then follows from Theorem 684.

We unfold \(\mathrm{canTolerateFaults}\). The goal \(d_{\mathrm{ST}} - 1 {\lt} d_{\mathrm{ST}}\) follows by integer arithmetic (omega) from the hypothesis \(0 {\lt} d_{\mathrm{ST}}\).

Let \(F\) be given with \(|F|_{\mathit{times}} = 0\) and \(\mathrm{hasEmptySyndrome}(F)\). Assume for contradiction that \(\mathrm{affectsLogicalInfo}(F)\) holds. Then \(F\) is a spacetime logical fault (by definition, pairing the empty syndrome and affects-logical hypotheses). By Theorem 679, \(d_{\mathrm{ST}} \leq |F|_{\mathit{times}} = 0\). But \(0 {\lt} d_{\mathrm{ST}}\) by hypothesis. By integer arithmetic, this is a contradiction.

Assume for contradiction that \(\mathbf{1}\) is a spacetime logical fault. From the group-like property of the logical effect, we have \(\mathrm{identity\_ preserves}\), which states that the identity does not affect logical information. This contradicts \(\mathbf{1}.\mathrm{affectsLogical}\) from the logical fault hypothesis.

We verify the two conditions for \(\mathrm{IsGLB}\):

• Lower bound: For any \(w \in W\), \(d_{\mathrm{ST}} \leq w\). This follows directly from Theorem 686.

• Greatest lower bound: Let \(n\) be any lower bound of \(W\). By Theorem 681, there exists \(F\) with \(h_F\) and \(|F|_{\mathit{times}} = d_{\mathrm{ST}}\). Since \(|F|_{\mathit{times}} \in W\) (witnessed by \(\langle F, h_F, \mathrm{rfl}\rangle \)), we have \(n \leq |F|_{\mathit{times}}\) by the lower bound hypothesis. Rewriting with \(h_{\mathrm{eq}}\), we get \(n \leq d_{\mathrm{ST}}\).