This follows directly from the commutativity of symmetric difference: \(s_1 \triangle s_2 = s_2 \triangle s_1\).

This follows directly from the associativity of symmetric difference: \((s_1 \triangle s_2) \triangle s_3 = s_1 \triangle (s_2 \triangle s_3)\).

By simplification using the definitions of \(\mathrm{add}\) and \(\mathrm{empty}\), we have \(s \triangle \emptyset = s\) since \(\emptyset \) is the bottom element under symmetric difference.

By simplification using the definitions of \(\mathrm{add}\) and \(\mathrm{empty}\), we have \(\emptyset \triangle s = s\) since \(\emptyset \) is the bottom element under symmetric difference.

By simplification: \(s \triangle s = \emptyset \) since the symmetric difference of a set with itself is empty.

By simplification using the definitions of \(\mathrm{card}\) and \(\mathrm{empty}\), this reduces to the standard fact that a finite set has cardinality zero if and only if it is empty.

We prove both directions. For the forward direction, assume \(\mathrm{syndromeVector}(\mathrm{DC}, \mathrm{base}, F)(D) = 1\). By the definition of \(\mathrm{syndromeVector}\) and \(\mathrm{syndrome}\), we split on whether \(D\) is a member of the syndrome (a filtered set). If \(D\) is in the filter, then by the filter condition \(D.\mathrm{isViolated}\) holds. If \(D\) is not in the filter, then the syndrome vector would be \(0\), contradicting the hypothesis via simplification. For the reverse direction, assume \(D.\mathrm{isViolated}(\mathrm{applyFaultToOutcomes'}(\mathrm{base}, F))\). Then directly applying the lemma syndromeVector_violated with hypotheses \(D \in \mathrm{DC}.\mathrm{detectors}\) and the violation condition yields the result.

By simplification, \(\mathrm{syndrome}\) is a filter, so it suffices to show that no detector in \(\mathrm{DC}.\mathrm{detectors}\) is violated. Let \(D \in \mathrm{DC}.\mathrm{detectors}\). We first establish that applying the identity fault to outcomes yields the base outcomes unchanged: for all \(m, t\), since \(\mathbf{1}.\mathrm{timeErrors}(m,t) = \mathrm{false}\), the if-branch is not taken, so \(\mathrm{applyFaultToOutcomes'}(\mathrm{base}, \mathbf{1}) = \mathrm{base}\). This holds by reflexivity. Rewriting with this equality and using the equivalence \(\mathrm{isSatisfied} \iff \neg \, \mathrm{isViolated}\), we need \(D.\mathrm{isSatisfied}(\mathrm{base})\). Rewriting the hypothesis \(\mathrm{DC}.\mathrm{allSatisfied}(\mathrm{base})\) using the characterization DetectorCollection.allSatisfied_iff, we obtain that all detectors in the collection are satisfied, and the result follows.

Unfolding the definitions of \(\mathrm{hasEmptySyndrome'}\) and \(\mathrm{syndrome}\), and rewriting using the characterization that a filter is empty iff the predicate holds for no element, we prove both directions. For the forward direction, assume the filter is empty and let \(D \in \mathrm{DC}.\mathrm{detectors}\). Rewriting \(\mathrm{isSatisfied}\) as \(\neg \, \mathrm{isViolated}\), this follows from the emptiness of the filter. For the reverse direction, assume all detectors are satisfied and let \(D \in \mathrm{DC}.\mathrm{detectors}\). Rewriting \(\neg \, \mathrm{isViolated}\) as \(\mathrm{isSatisfied}\), the result follows from the hypothesis.

By extensionality, it suffices to show that for each detector \(D\), membership in the left-hand side is equivalent to membership in the symmetric difference on the right.

By the definition of syndrome as a filter, \(D\) is in the left-hand side iff \(D \in \mathrm{DC}.\mathrm{detectors}\) and \(D\) is violated by \(f \cdot g\). By the symmetric difference characterization, \(D\) is on the right iff it is in exactly one of the two syndromes.

Forward direction. Assume \(D \in \mathrm{DC}.\mathrm{detectors}\) and \(D\) is violated by \(f \cdot g\). Using the parity-determines property of the linearity condition, \(D\) is violated by the composite iff the count of measurement events where \((f \cdot g)\) has a time-error is odd. Since \((f \cdot g).\mathrm{timeErrors}(m, t) = f.\mathrm{timeErrors}(m, t) \oplus g.\mathrm{timeErrors}(m, t)\) (XOR), the set of faulted events for the product is the symmetric difference of the individual faulted event sets. Using the helper lemma on symmetric difference cardinality (\(|A \triangle B| \equiv |A| + |B| \pmod{2}\)), the sum of the individual counts is odd. By integer arithmetic, this means exactly one of \(|A| \bmod 2 = 1\) and \(|B| \bmod 2 = 1\) holds. In each case, we construct membership in exactly one syndrome with non-membership in the other, using the parity-determines characterization.

Reverse direction. Assume \(D\) is in the symmetric difference. We consider two cases.

Case 1: \(D\) is in the syndrome of \(f\) but not \(g\). Then \(D \in \mathrm{DC}.\mathrm{detectors}\). Using parity-determines, the count for \(f\) is odd and the count for \(g\) is even. As in the forward direction, we establish that \((f \cdot g).\mathrm{timeErrors}\) corresponds to XOR, so the faulted event set for the product is the symmetric difference of the individual sets. Using the cardinality-mod-2 lemma, the product count has parity equal to the sum of parities. Since the \(f\)-count is odd and the \(g\)-count is even (by negation of the odd condition), by integer arithmetic the sum is odd, establishing the violation.

Case 2: \(D\) is in the syndrome of \(g\) but not \(f\). By a symmetric argument: \(D \in \mathrm{DC}.\mathrm{detectors}\), the \(g\)-count is odd and the \(f\)-count is even, and by the same XOR and symmetric difference cardinality reasoning, the product count is odd.

By extensionality on detector \(D\), membership in the syndrome is equivalent to \(D \in \mathrm{DC}.\mathrm{detectors}\) and \(D\) being violated. For the forward direction, assume \(D \in \mathrm{DC}.\mathrm{detectors}\) and \(D\) is violated by \(F^{-1}\). Using the parity-determines property for \(F^{-1}\) and then for \(F\), we convert both violation conditions to parity conditions on the filtered measurement events, and these are equal. The reverse direction follows by the same argument in the opposite direction.

We decide by cases on whether \(\mathrm{isTrivial}(F)\) holds. If \(\mathrm{isTrivial}(F)\), then the left disjunct holds by pairing the empty syndrome hypothesis with the triviality. If \(\neg \, \mathrm{isTrivial}(F)\), then the right disjunct holds by pairing the empty syndrome hypothesis with non-triviality.

Assume both hold. From the stabilizer hypothesis, \(\mathrm{isTrivial}(F)\) holds. From the logical fault hypothesis, \(\neg \, \mathrm{isTrivial}(F)\) holds. This is a contradiction.

This holds by reflexivity of the biconditional, since the left-hand side is definitionally equal to the right-hand side.

By simplification: the syndrome is defined as a filter of \(\mathrm{DC}.\mathrm{detectors}\) by the violation predicate. Since \(D \in \mathrm{DC}.\mathrm{detectors}\) is given, membership in the filter reduces to the violation condition.

Let \(D \in \mathrm{syndrome}(\mathrm{DC}, \mathrm{base}, F)\). By the definition of syndrome as a filter of \(\mathrm{DC}.\mathrm{detectors}\), membership in the filter implies membership in \(\mathrm{DC}.\mathrm{detectors}\), which is the first component of the conjunction.