27 Def 9: Syndrome
The syndrome of a spacetime fault (Def 7) is the set of detectors (Def 8) that are violated by the fault. A detector is violated if the product of its measurement outcomes is \(-1\) instead of the expected \(+1\). Equivalently, working over \(\mathbb {Z}_2\), if detectors are indexed as \(D_1, \ldots , D_m\), the syndrome can be identified with a binary vector \(s \in \mathbb {Z}_2^m\) where \(s_j = 1\) if and only if detector \(D_j\) is violated.
Let \(I\) be a finite type indexing a collection of detectors \(\{ D_i\} _{i \in I}\), and let \(F\) be a spacetime fault. The syndrome fault set of \(F\) with respect to the detectors is the finset of detector indices that are violated by \(F\):
Since detectors depend only on measurement outcomes and only time-faults flip outcomes, the syndrome is determined by the time-fault component of \(F\).
The syndrome vector of a spacetime fault \(F\) with respect to detectors \(\{ D_i\} _{i \in I}\) is the binary vector \(s \colon I \to \mathbb {Z}_2\) defined by
This is the \(\mathbb {Z}_2^m\) representation of the syndrome.
A detector index \(i\) is in the syndrome if and only if detector \(D_i\) is violated by the spacetime fault:
By the definition of \(\operatorname {syndromeFault}\) as a filter over the universal finset, the result follows by simplification.
The syndrome vector satisfies \(s(i) = 1\) if and only if detector \(D_i\) is violated:
Unfolding the definition of \(\operatorname {syndromeVec}\), we split on the conditional. If the detector is violated, then \(s(i) = 1\) by definition, and the forward direction is trivially satisfied. If the detector is not violated, then \(s(i) = 0\), so \(s(i) = 1\) is contradicted by \(0 \neq 1\), and the backward direction is contradicted by the assumption that the detector is not violated.
The syndrome vector satisfies \(s(i) = 0\) if and only if detector \(D_i\) is not violated:
Unfolding the definition of \(\operatorname {syndromeVec}\) and splitting on the conditional, in the case where the detector is violated we have \(s(i) = 1\) and must show \(1 = 0 \Leftrightarrow \bot \), which follows by simplification. In the case where the detector is not violated, \(s(i) = 0\) and the equivalence follows by simplification.
The spacetime syndrome equals the Def 8 syndrome applied to the time-fault component. This captures the key fact that detectors depend only on measurement outcomes, so only time-faults affect the syndrome:
By extensionality on the index \(i\), we simplify using the definitions of \(\operatorname {syndromeFault}\), \(\operatorname {Detector.syndrome}\), and \(\operatorname {Detector.isViolated}\). Both sides reduce to filtering the universal set by the same predicate.
The syndrome is empty for the fault-free spacetime configuration:
Simplifying using the definition of \(\operatorname {syndromeFault}\), the filter is empty if no detector is violated. For each detector index \(i\), the result follows from the fact that no detector is violated in the absence of faults (Detector.not_isViolated_no_faults).
The syndrome vector is zero for the fault-free configuration:
By extensionality on the index \(i\), we simplify the definition of \(\operatorname {syndromeVec}\) at the empty fault. We establish that no detector is violated in the absence of faults using Detector.not_isViolated_no_faults. Since the detector is not violated, the conditional evaluates to \(0\), which equals the zero function applied at \(i\).
The syndrome finset is exactly the support of the syndrome vector:
By extensionality on the index \(i\), we simplify using the membership characterization of the syndrome finset and the characterization of the syndrome vector being \(1\), which both reduce to the detector being violated.
Membership in the syndrome finset is equivalent to the syndrome vector entry being \(1\):
Rewriting using the membership characterization \(\operatorname {mem\_ syndromeFault\_ iff}\) and the syndrome vector characterization \(\operatorname {syndromeVec\_ eq\_ one\_ iff}\), the result follows directly.
Non-membership in the syndrome finset is equivalent to the syndrome vector entry being \(0\):
Rewriting using the membership characterization and the zero characterization of the syndrome vector, the result follows directly.
Space-faults do not affect the syndrome: two spacetime faults with the same time-fault component produce the same syndrome. If \(F_1.\mathrm{timeFaults} = F_2.\mathrm{timeFaults}\), then
By extensionality on the index \(i\), we simplify using the definitions of \(\operatorname {syndromeFault}\), \(\operatorname {Detector.isViolated}\), and \(\operatorname {Detector.observedParity}\), together with the hypothesis \(h\) that the time-fault components are equal. Both sides reduce to the same expression.
The syndrome vector is the same for faults with identical time-fault components. If \(F_1.\mathrm{timeFaults} = F_2.\mathrm{timeFaults}\), then
By extensionality on the index \(i\), we simplify using the definitions of \(\operatorname {syndromeVec}\), \(\operatorname {Detector.isViolated}\), and \(\operatorname {Detector.observedParity}\), together with the hypothesis that the time-fault components are equal.
A pure space-fault (no time-faults) has empty syndrome:
From the hypothesis that \(F\) is a pure space-fault, we obtain that \(F.\mathrm{timeFaults} = \emptyset \). We then show the filter is empty: for each detector index \(i\), unfolding \(\operatorname {Detector.isViolated}\) and rewriting the time-faults as empty, the observed parity with no faults is \(0\) by Detector.observedParity_no_faults. Since \(0 \neq 1\), the detector is not violated.
A pure space-fault has zero syndrome vector:
From the hypothesis that \(F\) is a pure space-fault, we obtain \(F.\mathrm{timeFaults} = \emptyset \). By extensionality on \(i\), we simplify the definition of \(\operatorname {syndromeVec}\). We establish that the detector is not violated by unfolding \(\operatorname {Detector.isViolated}\), rewriting with the empty time-faults, and using Detector.observedParity_no_faults to show the parity is \(0 \neq 1\). Since the detector is not violated, the conditional evaluates to \(0\).
The number of violated detectors equals the cardinality of the syndrome:
This holds by reflexivity, as both sides are definitionally equal.
The sum of the syndrome vector counts the number of violated detectors modulo \(2\):
Simplifying the definitions of \(\operatorname {syndromeVec}\) and \(\operatorname {syndromeFault}\), we rewrite the sum using the identity for summing an if-then-else function: the sum splits into a sum of \(1\)’s over the violated detectors (which equals the cardinality of the filtered set) plus a sum of \(0\)’s over the non-violated detectors. Adding zero and casting the cardinality to \(\mathbb {Z}_2\) yields the result.
The syndrome is equivalently described using flip parities of detectors:
By extensionality on \(i\), we simplify using the definition of \(\operatorname {syndromeFault}\), \(\operatorname {Detector.isViolated}\), and the equivalence between observed parity and flip parity (Detector.observedParity_eq_flipParity).
The syndrome vector can be computed via flip parities:
Simplifying the definition of \(\operatorname {syndromeVec}\) using \(\operatorname {Detector.isViolated}\) and the equivalence \(\operatorname {Detector.observedParity\_ eq\_ flipParity}\), we split on the conditional. If the flip parity equals \(1\), then by symmetry the result is \(1\). If not, we push the negation and case-split on whether the flip parity is \(0\) or \(1\) (since every element of \(\mathbb {Z}_2\) is \(0\) or \(1\)). In the \(0\) case the result follows by symmetry; the \(1\) case leads to a contradiction.
A pure space-fault embedded as a spacetime fault has empty syndrome, since space-faults do not violate detectors:
We apply the theorem that pure space-faults have empty syndrome (\(\operatorname {syndromeFault\_ pureSpace}\)). The hypothesis that \(\operatorname {ofSpaceFault}(f)\) is a pure space-fault follows from \(\operatorname {SpacetimeFault.isPureSpace\_ ofSpaceFault}\).
A detector not containing any faulted measurement is not violated. If for every measurement \(m\) in \(D.\mathrm{measurements}\), the time-fault \(\langle m \rangle \) is not in the fault set, then \(D\) is not violated:
Rewriting \(\operatorname {isViolated}\) in terms of \(\operatorname {flipParity}\) using \(\operatorname {Detector.isViolated\_ iff\_ flipParity}\), we show the flip parity is \(0\). Unfolding \(\operatorname {Detector.flipParity}\), the sum over measurements \(m\) in \(D.\mathrm{measurements}\) reduces to \(0\) because each term is \(0\): for each \(m\), since \(\langle m \rangle \notin \mathrm{faults}\), the indicator is \(0\) by simplification. Since the flip parity is \(0\) and \(0 \neq 1\), the detector is not violated.
The syndrome captures the error information revealed by detectors: two faults produce the same syndrome if and only if they violate the same detectors:
We prove both directions. For the forward direction, assume the syndrome sets are equal. For each \(i\), we use the membership characterization for both \(F_1\) and \(F_2\). Rewriting the hypothesis of equal sets into the membership for \(F_1\), we obtain the biconditional: if \(D_i\) is violated by \(F_1\) then the membership in the (rewritten) syndrome for \(F_2\) gives violation by \(F_2\), and vice versa. For the reverse direction, assume the pointwise biconditional. By extensionality on \(i\), we simplify the definition of \(\operatorname {syndromeFault}\) and apply the hypothesis for index \(i\).
Two faults have the same syndrome vector if and only if they have the same syndrome finset:
We prove both directions. For the forward direction, assume the syndrome vectors are equal. By extensionality on the syndrome finsets, for each \(i\) we extract the pointwise equality \(\operatorname {syndromeVec}(\{ D_k\} , F_1)(i) = \operatorname {syndromeVec}(\{ D_k\} , F_2)(i)\) using \(\operatorname {congr\_ fun}\). Then we simplify using the membership characterization and the syndrome vector characterization. For the reverse direction, assume the syndrome finsets are equal. By extensionality on \(i\), we establish that membership in the two syndromes is equivalent by rewriting with the hypothesis. We then rewrite membership in terms of the syndrome vector being \(1\). Case-splitting on whether each syndrome vector entry is \(0\) or \(1\) (using the fact that every element of \(\mathbb {Z}_2\) is \(0\) or \(1\)), the matching cases are immediate (\(0 = 0\) or \(1 = 1\)), and the mismatched cases lead to contradictions via \(0 \neq 1\).