We unfold the definitions of \(\mathrm{hasEmptySyndrome}\) and \(\mathrm{computeSyndrome}\), then rewrite using the fact that a filter over a finset is empty if and only if the predicate holds for no element. For the forward direction, assume \(\mathrm{hasEmptySyndrome}\) holds, let \(D \in \mathrm{DC}.\mathrm{detectors}\), and rewrite using \(\mathrm{Detector.satisfied\_ iff\_ not\_ violated}\) to conclude \(D\) is satisfied. For the converse, assume every detector is satisfied, let \(D \in \mathrm{DC}.\mathrm{detectors}\), rewrite using the negation of \(\mathrm{Detector.satisfied\_ iff\_ not\_ violated}\), and apply the hypothesis.

We rewrite using the characterization \(\mathrm{hasEmptySyndrome\_ iff}\). Let \(D \in \mathrm{DC}.\mathrm{detectors}\). We first establish that \(\mathrm{applyFaultToOutcomes}(\mathrm{base}, 1) = \mathrm{base}\) by extensionality: for all \(m, t\), since the identity fault has no time errors, the outcome is unchanged. This holds by reflexivity. Rewriting with this equality, the hypothesis \(\mathrm{DC}.\mathrm{allSatisfied}(\mathrm{base})\), expanded via \(\mathrm{DetectorCollection.allSatisfied\_ iff}\), gives \(D.\mathrm{isSatisfied}(\mathrm{base})\) directly.

We consider two cases based on whether \(\ell (f)\) holds. If \(\ell (f)\) holds, then \(f\) is a spacetime logical fault, constructed from the empty syndrome hypothesis and \(\ell (f)\). If \(\neg \ell (f)\), then \(f\) is a spacetime stabilizer, constructed from the empty syndrome hypothesis and \(\neg \ell (f)\).

Assume both hold. Then from the stabilizer property we have \(\neg \ell (f)\) (preserves logical info), and from the logical fault property we have \(\ell (f)\) (affects logical info). This is a contradiction.

By extensionality, it suffices to show membership equivalence for an arbitrary fault \(f\). We simplify using the definitions of the three sets. For the forward direction, if \(f\) is in the left-hand union, then \(f\) is either a stabilizer or a logical fault, and in both cases we extract the empty syndrome condition. For the reverse direction, if \(f\) has empty syndrome, we apply the partition theorem to conclude \(f\) is either a stabilizer or a logical fault.

We unfold the definition of fault equivalence. Since \(f^{-1} \cdot f = 1\) by \(\mathrm{inv\_ mul\_ cancel}\), it suffices to show that \(1\) is in the spacetime stabilizer subgroup. This follows from the identity membership property of the subgroup.

We unfold fault equivalence in both the hypothesis and the goal. We establish that \(g^{-1} \cdot f = (f^{-1} \cdot g)^{-1}\) by simplifying using \(\mathrm{mul\_ inv\_ rev}\) and \(\mathrm{inv\_ inv}\). Rewriting with this identity, the result follows from closure of the spacetime stabilizer subgroup under inverses.

We unfold fault equivalence in the hypotheses and the goal. We establish the key identity \(f^{-1} \cdot k = (f^{-1} \cdot g) \cdot (g^{-1} \cdot k)\) by simplifying with \(\mathrm{mul\_ assoc}\) and \(\mathrm{mul\_ inv\_ cancel\_ left}\). Rewriting with this identity, the result follows from closure of the spacetime stabilizer subgroup under multiplication.

The equivalence is constructed directly from the three component proofs: reflexivity from \(\mathrm{faultEquivalent\_ refl}\), symmetry from \(\mathrm{faultEquivalent\_ symm}\), and transitivity from \(\mathrm{faultEquivalent\_ trans}\).

We prove both directions. For the forward direction, assume \(f\) is a logical fault and suppose for contradiction that \(f\) is also a stabilizer. Then the stabilizer’s \(\mathrm{preservesLogical}\) property contradicts the logical fault’s \(\mathrm{affectsLogical}\) property. For the reverse direction, assume \(f\) is not a stabilizer. We construct a logical fault: the empty syndrome is given by hypothesis. For the logical effect, we argue by contradiction: if \(\neg \ell (f)\), then \(f\) would be a stabilizer (constructed from the empty syndrome and \(\neg \ell (f)\)), contradicting the assumption that \(f\) is not a stabilizer.