Unfolding the definitions of \(\operatorname {IsSyndromeFree}\) and \(\operatorname {syndromeFault}\), the condition that the filter of violated detectors equals the empty set is equivalent, by simplification using the universal membership and true-implies rules, to the statement that no detector is violated.

We rewrite using the characterization that syndrome-free means every detector is not violated. For the forward direction, assume every detector is not violated. By extensionality, for each index \(i\), the syndrome vector at \(i\) is defined by an if-then-else on whether \(\delta _i\) is violated; since it is not, the value is \(0\), so the entire vector is \(0\). For the reverse direction, assume the syndrome vector equals \(0\). For any index \(i\), we extract the component at \(i\), which equals \(0\). Suppose for contradiction that \(\delta _i\) is violated; then the if-branch gives value \(1\), contradicting \(1 \neq 0\).

We consider two cases on whether \(\operatorname {outcomePreserving}(F)\) holds. If it does, then \(F\) is a spacetime stabilizer (the right disjunct), constructed from the syndrome-free hypothesis and the outcome-preserving property. If it does not, then \(F\) is a spacetime logical fault (the left disjunct), constructed from the syndrome-free hypothesis and the negation of outcome-preserving.

Assume \(F\) is a spacetime logical fault and suppose for contradiction it is also a stabilizer. Then \(F\) is outcome-preserving (from the stabilizer condition), but \(F\) is also outcome-changing (from the logical fault condition). The outcome-changing condition is the negation of outcome-preserving, giving a contradiction.

Assume \(F\) is a stabilizer and suppose for contradiction it is also a logical fault. Then the logical fault’s outcome-changing condition contradicts the stabilizer’s outcome-preserving condition.

This is the first component of the conjunction defining a spacetime logical fault.

This is the second component of the conjunction defining a spacetime logical fault.

This is the first component of the conjunction defining a spacetime stabilizer.

This is the second component of the conjunction defining a spacetime stabilizer.

Unfolding the definition of \(\operatorname {IsSyndromeFree}\), we rewrite using the fact that the syndrome of the empty fault is empty (\(\operatorname {syndromeFault\_ empty}\)).

The proof constructs the pair: the first component is \(\operatorname {empty\_ isSyndromeFree}\) applied to the detectors, and the second component is the hypothesis that the empty fault is outcome-preserving.

Rewriting the hypothesis \(F.\! \operatorname {weight} = 0\) using the lemma \(\operatorname {weight\_ zero\_ iff\_ empty}\), the result follows directly.

Suppose for contradiction that \(F.\! \operatorname {weight} \leq 0\). Pushing the negation, we get \(F.\! \operatorname {weight} = 0\) (since weight is a natural number). By the theorem \(\operatorname {syndromeFree\_ weight\_ zero\_ eq\_ empty}\) applied to \(F\)’s syndrome-free property, we conclude \(F = \operatorname {empty}\). Substituting, the logical fault condition requires \(\neg \, \operatorname {outcomePreserving}(\operatorname {empty})\), which contradicts the hypothesis that the empty fault is outcome-preserving.

This follows by applying the forward direction of \(\operatorname {isSyndromeFree\_ iff\_ syndromeVec}\) to the syndrome-free component of the logical fault hypothesis.

This follows by applying the forward direction of \(\operatorname {isSyndromeFree\_ iff\_ syndromeVec}\) to the syndrome-free component of the stabilizer hypothesis.

For the forward direction, we apply \(\operatorname {syndromeFree\_ dichotomy}\). For the reverse direction, we case-split on whether \(F\) is a logical fault or a stabilizer; in either case, the first component of the conjunction gives syndrome-freeness.

For the forward direction, we apply \(\operatorname {logicalFault\_ not\_ stabilizer}\). For the reverse direction, assume \(F\) is not a stabilizer. We construct the logical fault: the first component is the syndrome-free hypothesis. For the second component (outcome-changing), assume for contradiction that \(F\) is outcome-preserving. Then \(F\) would be a stabilizer (pairing syndrome-free with outcome-preserving), contradicting the hypothesis.

For the forward direction, assume \(F\) is a stabilizer and suppose \(F\) is also a logical fault; we apply \(\operatorname {logicalFault\_ not\_ stabilizer}\) to derive a contradiction. For the reverse direction, assume \(F\) is not a logical fault. We construct the stabilizer: the first component is syndrome-freeness. For the second (outcome-preserving), suppose for contradiction that \(F\) is not outcome-preserving; then \(F\) would be a logical fault, contradicting the hypothesis.

Every element \(x \in \mathbb {Z}/2\mathbb {Z}\) satisfies \(x = 0 \lor x = 1\). This is verified by case analysis on the two elements of \(\mathbb {Z}/2\mathbb {Z}\) followed by simplification. The result then follows by applying this fact to \(\operatorname {gaussSignFlip}(F)\).

We case-split on whether \(\operatorname {gaussSignFlip}(F)\) is \(0\) or \(1\) using \(\operatorname {gaussSignFlip\_ zero\_ or\_ one}\). If it is \(0\), then \(F\) preserves the gauging sign (the right disjunct). If it is \(1\), then \(F\) flips the gauging sign (the left disjunct).

Assume \(F\) flips the gauging sign, so \(\operatorname {gaussSignFlip}(F) = 1\). Suppose for contradiction that \(F\) also preserves the gauging sign, so \(\operatorname {gaussSignFlip}(F) = 0\). Rewriting, we get \(0 = 1\), which contradicts \(0 \neq 1\).

Assume \(F\) preserves the gauging sign and suppose for contradiction that \(F\) flips it. By \(\operatorname {flipsGaugingSign\_ not\_ preserves}\), flipping implies not preserving, contradicting our assumption.

We case-split on whether \(\operatorname {outcomePreserving}(F)\) holds. If yes, \(F\) is a gauging stabilizer (right disjunct). If no, \(F\) is a gauging logical fault (left disjunct).

Assume \(F\) is a gauging logical fault and suppose it is also a stabilizer. The logical fault condition gives \(\neg \, \operatorname {outcomePreserving}(F)\), while the stabilizer condition gives \(\operatorname {outcomePreserving}(F)\), a contradiction.

Assume \(F\) is a gauging stabilizer and suppose it is also a logical fault. The logical fault’s outcome-changing condition contradicts the stabilizer’s outcome-preserving condition.

For the forward direction, apply \(\operatorname {gaugingLogicalFault\_ not\_ stabilizer}\). For the reverse direction, assume \(F\) is syndrome-free but not a stabilizer. We construct the logical fault: the first component is syndrome-freeness. For the second, assume for contradiction that \(F\) is outcome-preserving; then pairing with syndrome-freeness gives a stabilizer, contradicting the hypothesis.

For the forward direction, assume \(F\) is a stabilizer and suppose it is also a logical fault; we apply \(\operatorname {gaugingLogicalFault\_ not\_ stabilizer}\) to derive a contradiction. For the reverse direction, assume \(F\) is syndrome-free but not a logical fault. We construct the stabilizer: the first component is syndrome-freeness. For the second, suppose for contradiction that \(F\) is not outcome-preserving; then pairing with syndrome-freeness gives a logical fault, contradicting the hypothesis.