25 Lem 3: Spacetime Code Detectors
The following form a generating set of local detectors in the fault-tolerant gauging measurement procedure. For times before and after code deformation (\(t {\lt} t_i\) and \(t {\gt} t_o\)), detectors are repeated measurements of the original checks \(s_j\) at consecutive half-integer times. During code deformation (\(t_i {\lt} t {\lt} t_o\)), detectors are repeated measurements of the Gauss law operators \(A_v\), flux operators \(B_p\), and deformed checks \(\tilde{s}_j\). At the boundaries \(t = t_i\) and \(t = t_o\), special detectors relate initialization/finalization to measurements.
A gauging region is a structure specifying the time boundaries of the gauging measurement procedure, consisting of:
A start time \(t_i\) (the start of code deformation),
An end time \(t_o\) (the end of code deformation),
The validity condition \(t_i {\lt} t_o\), ensuring the deformation has positive duration.
A time \(t\) is before code deformation if \(t {\lt} t_i\).
A time \(t\) is during code deformation if \(t_i {\lt} t\) and \(t {\lt} t_o\).
A time \(t\) is after code deformation if \(t {\gt} t_o\).
A time \(t\) is at the start boundary if \(t = t_i\).
A time \(t\) is at the end boundary if \(t = t_o\).
For any gauging region \(R\) and any time \(t\), exactly one of the following holds:
That is, the five time regions partition all times.
We unfold the definitions of isBefore, isStart, isDuring, isEnd, and isAfter. We consider cases on whether \(t {\lt} t_i\). If so, the first disjunct holds. Otherwise, \(t \geq t_i\). We then consider whether \(t = t_i\); if so, the second disjunct holds. Otherwise \(t {\gt} t_i\). We then consider whether \(t {\lt} t_o\); if so, \(t_i {\lt} t {\lt} t_o\) and the third disjunct holds. Otherwise \(t \geq t_o\). We consider whether \(t = t_o\); if so the fourth disjunct holds; otherwise \(t {\gt} t_o\) and the fifth disjunct holds.
The time regions are mutually exclusive. Specifically, for any time \(t\):
\(\neg (\mathrm{isBefore}(t) \land \mathrm{isStart}(t))\),
\(\neg (\mathrm{isBefore}(t) \land \mathrm{isDuring}(t))\),
\(\neg (\mathrm{isStart}(t) \land \mathrm{isDuring}(t))\),
\(\neg (\mathrm{isDuring}(t) \land \mathrm{isEnd}(t))\),
\(\neg (\mathrm{isDuring}(t) \land \mathrm{isAfter}(t))\).
We unfold all definitions and verify each conjunction separately. For (1), if \(t {\lt} t_i\) and \(t = t_i\), substituting gives \(t_i {\lt} t_i\), contradicting irreflexivity. For (2), if \(t {\lt} t_i\) and \(t_i {\lt} t\), this contradicts asymmetry of \({\lt}\). For (3), if \(t = t_i\) and \(t_i {\lt} t\), substituting gives \(t_i {\lt} t_i\), a contradiction. For (4), if \(t {\lt} t_o\) and \(t = t_o\), substituting gives \(t_o {\lt} t_o\), a contradiction. For (5), if \(t {\lt} t_o\) and \(t {\gt} t_o\), this contradicts asymmetry of \({\lt}\).
The type of parity values is \(\mathbb {Z}/2\mathbb {Z}\), where \(0\) represents \(+1\) (no flip) and \(1\) represents \(-1\) (flip).
A measurement outcome is an element of \(\mathbb {Z}/2\mathbb {Z}\), where \(0\) encodes the \(+1\) outcome and \(1\) encodes the \(-1\) outcome.
For any \(x \in \mathbb {Z}/2\mathbb {Z}\), \(x + x = 0\).
We case-split on \(x\): when \(x = 0\), \(0 + 0 = 0\); when \(x = 1\), \(1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\). Both cases are verified by computation.
The XOR parity of two measurement outcomes \(m_1, m_2\) is defined as \(m_1 + m_2 \in \mathbb {Z}/2\mathbb {Z}\).
For any measurement outcome \(m\), \(\mathrm{xorParity}(m, m) = 0\).
Unfolding the definition, \(\mathrm{xorParity}(m, m) = m + m = 0\) by the \(\mathbb {Z}/2\mathbb {Z}\) self-addition lemma.
The type of operator involved in a detector, given as an inductive type with constructors:
\(\mathrm{originalCheck}(j)\): the original stabilizer check \(s_j\),
\(\mathrm{gaussLaw}(v)\): the Gauss law operator \(A_v\),
\(\mathrm{flux}(p)\): the flux operator \(B_p\),
\(\mathrm{deformedCheck}(j)\): the deformed check \(\tilde{s}_j\),
\(\mathrm{edgeZ}(e)\): a single-qubit \(Z\) measurement on edge \(e\).
The time classification of a detector:
\(\mathrm{bulk}\): repeated measurement of the same observable at times \(t - \tfrac {1}{2}\) and \(t + \tfrac {1}{2}\),
\(\mathrm{initialBoundary}\): initialization at \(t_i - \tfrac {1}{2}\), first measurement at \(t_i + \tfrac {1}{2}\),
\(\mathrm{finalBoundary}\): last measurement at \(t_o - \tfrac {1}{2}\), readout at \(t_o + \tfrac {1}{2}\).
An elementary detector is one of the generators of the detector group, consisting of:
An operator type (original check, Gauss law, flux, deformed check, or edge \(Z\)),
A time step,
A time type (bulk or boundary).
A bulk detector specification for \(n\) qubits consists of:
A support set \(S \subseteq \mathrm{Fin}(n)\) (the observable being measured),
Two measurement times \(t_1\) and \(t_2\) with \(t_2 = t_1 + 1\) (consecutive times).
The bulk detector parity of two measurement outcomes \(m_1, m_2\) is \(\mathrm{xorParity}(m_1, m_2) = m_1 + m_2\).
In error-free projective measurement, measuring the same observable twice on the same state gives identical outcomes. Hence for any outcome \(m\), \(\mathrm{bulkDetectorParity}(m, m) = 0\).
This follows directly from \(\mathrm{xorParity}(m, m) = 0\).
The bulk detector parity is zero if and only if the two measurement outcomes are equal:
We unfold the definitions. For the forward direction, assume \(m_1 + m_2 = 0\). Adding \(m_2\) to both sides: \(m_1 + m_2 + m_2 = 0 + m_2\). By associativity, \(m_1 + (m_2 + m_2) = m_2\). By the \(\mathbb {Z}/2\mathbb {Z}\) self-addition lemma, \(m_2 + m_2 = 0\), so \(m_1 + 0 = m_2\), giving \(m_1 = m_2\). For the reverse direction, if \(m_1 = m_2\), then \(m_1 + m_2 = m_2 + m_2 = 0\) by the self-addition lemma.
The \(Z\) measurement on the \(|0\rangle \) state gives \(+1\), encoded as \(0 \in \mathbb {Z}/2\mathbb {Z}\).
For any finite set of edges, \(\bigl(\prod _{e} Z_e\bigr)|0\rangle ^{\otimes |E|} = (+1)|0\rangle ^{\otimes |E|}\). In \(\mathbb {Z}/2\mathbb {Z}\), \(\sum _{e \in \mathrm{edges}} 0 = 0\).
By simplification: each summand is \(0\) (since \(z\_ {\mathrm{eigenvalue\_ on\_ zero}} = 0\)), and the sum of zeros over any finite set is zero.
At \(t = t_i\), edge qubits are initialized in \(|0\rangle \). Since \(|0\rangle \) is a \(+1\) eigenstate of \(Z\), we have \(B_p = \prod _{e \in p} Z_e\) with eigenvalue \(\prod _{e \in p}(+1) = +1\). The detector at \(t_i\) compares the initialization outcome (\(+1\), encoded as \(0\)) with the \(B_p\) measurement (\(+1\), encoded as \(0\)). The parity is \(\mathrm{xorParity}(0, 0) = 0\).
Let \(\mathrm{init\_ value} = 0\) and \(\mathrm{bp\_ value} = 0\). By simplification, \(\mathrm{xorParity}(0, 0) = 0 + 0 = 0\).
At \(t_i - \tfrac {1}{2}\), we measure \(s_j\) with outcome \(m_{s_j}\). At \(t_i + \tfrac {1}{2}\), we measure \(\tilde{s}_j = s_j \cdot Z_\gamma \). Since \(Z_\gamma |0\rangle = |0\rangle \) (eigenvalue \(+1\), encoded as \(0\)), we have \(m_{\tilde{s}} = m_{s_j} + 0 = m_{s_j}\). Therefore \(\mathrm{xorParity}(m_{s_j}, m_{\tilde{s}}) = 0\).
Let \(z_\gamma = 0\) (the \(Z_\gamma \) eigenvalue on \(|0\rangle \)) and \(\mathrm{stilde} = m_{s_j} + 0\). By simplification, \(\mathrm{stilde} = m_{s_j}\), so \(\mathrm{xorParity}(m_{s_j}, \mathrm{stilde}) = m_{s_j} + m_{s_j} = 0\) by the \(\mathbb {Z}/2\mathbb {Z}\) self-addition lemma.
Since \(B_p = \prod _{e \in p} Z_e\) by definition, measuring \(B_p\) and measuring all \(Z_e\) individually then taking the product (XOR in \(\mathbb {Z}/2\mathbb {Z}\)) give the same result. If \(m_{B_p} = m_{Z_e\text{-product}}\), then \(\mathrm{xorParity}(m_{B_p}, m_{Z_e\text{-product}}) = 0\).
Rewriting with the hypothesis \(m_{B_p} = m_{Z_e\text{-product}}\), the goal becomes \(\mathrm{xorParity}(m_{Z_e\text{-product}}, m_{Z_e\text{-product}}) = 0\), which follows from the self-cancellation property.
The relation \(\tilde{s}_j = s_j \cdot Z_\gamma \) implies a three-way parity constraint: if \(m_{\tilde{s}} = m_{s_j} + m_{Z_\gamma }\) in \(\mathbb {Z}/2\mathbb {Z}\), then \(m_{\tilde{s}} + m_{s_j} + m_{Z_\gamma } = 0\).
Rewriting \(m_{\tilde{s}}\) with the relation \(m_{\tilde{s}} = m_{s_j} + m_{Z_\gamma }\), we compute:
where both self-additions vanish by the \(\mathbb {Z}/2\mathbb {Z}\) self-addition lemma.
A detector configuration specifies:
A gauging region \(R\) (time boundaries),
The number of original checks \(n_{\mathrm{checks}}\),
The number of vertices \(n_V\) (Gauss law operators),
The number of cycles/plaquettes \(n_C\) (flux operators).
The set of bulk detectors for original checks at time \(t\) (used for \(t {\lt} t_i\) and \(t {\gt} t_o\)) is
The set of bulk detectors during deformation at time \(t\) (used for \(t_i {\lt} t {\lt} t_o\)) is the union:
The initial boundary detectors at \(t = t_i\) are:
The final boundary detectors at \(t = t_o\) are:
For any detector configuration and time \(t\), and any check index \(j {\lt} n_{\mathrm{checks}}\), the elementary detector \(\langle \mathrm{originalCheck}(j), t, \mathrm{bulk} \rangle \) belongs to the set of bulk original check detectors.
By simplification of the image and range membership conditions, we provide the witness \(j\) with \(j {\lt} n_{\mathrm{checks}}\) and verify the constructor equality.
For any detector configuration, time \(t\), and vertex index \(v {\lt} n_V\), the elementary detector \(\langle \mathrm{gaussLaw}(v), t, \mathrm{bulk} \rangle \) belongs to the bulk deformation detectors.
By simplification of union and image membership, we take the left branch (Gauss law component) and provide \(v\) with \(v {\lt} n_V\).
For any detector configuration, time \(t\), and cycle index \(p {\lt} n_C\), the elementary detector \(\langle \mathrm{flux}(p), t, \mathrm{bulk} \rangle \) belongs to the bulk deformation detectors.
By simplification of union and image membership, we take the middle branch (flux component) and provide \(p\) with \(p {\lt} n_C\).
For any detector configuration, time \(t\), and check index \(j {\lt} n_{\mathrm{checks}}\), the elementary detector \(\langle \mathrm{deformedCheck}(j), t, \mathrm{bulk} \rangle \) belongs to the bulk deformation detectors.
By simplification of union and image membership, we take the right branch (deformed check component) and provide \(j\) with \(j {\lt} n_{\mathrm{checks}}\).
For any cycle index \(p {\lt} n_C\), the detector \(\langle \mathrm{flux}(p), t_i, \mathrm{initialBoundary} \rangle \) belongs to the initial boundary detectors.
By simplification of union and image membership, we take the left branch and provide \(p\) with \(p {\lt} n_C\).
For any check index \(j {\lt} n_{\mathrm{checks}}\), the detector \(\langle \mathrm{deformedCheck}(j), t_i, \mathrm{initialBoundary} \rangle \) belongs to the initial boundary detectors.
By simplification of union and image membership, we take the right branch and provide \(j\) with \(j {\lt} n_{\mathrm{checks}}\).
For any cycle index \(p {\lt} n_C\), the detector \(\langle \mathrm{flux}(p), t_o, \mathrm{finalBoundary} \rangle \) belongs to the final boundary detectors.
By simplification of union and image membership, we take the left branch and provide \(p\) with \(p {\lt} n_C\).
For any check index \(j {\lt} n_{\mathrm{checks}}\), the detector \(\langle \mathrm{deformedCheck}(j), t_o, \mathrm{finalBoundary} \rangle \) belongs to the final boundary detectors.
By simplification of union and image membership, we take the right branch and provide \(j\) with \(j {\lt} n_{\mathrm{checks}}\).
The elementary detector parities are all zero in the error-free case. Specifically, the following five conditions hold simultaneously:
Bulk detectors: For all \(m\), \(\mathrm{bulkDetectorParity}(m, m) = 0\).
Initial \(B_p\): \(\mathrm{xorParity}(0, 0) = 0\).
Initial \(\tilde{s}_j\): For all \(m_{s_j}\), with \(m_{\tilde{s}} = m_{s_j} + 0\), \(\mathrm{xorParity}(m_{s_j}, m_{\tilde{s}}) = 0\).
Final \(B_p\): For all \(m_{B_p}, m_{Z_e}\), if \(m_{B_p} = m_{Z_e}\) then \(\mathrm{xorParity}(m_{B_p}, m_{Z_e}) = 0\).
Final \(\tilde{s}_j\): For all \(m_{\tilde{s}}, m_{s_j}, m_{Z_\gamma }\), if \(m_{\tilde{s}} = m_{s_j} + m_{Z_\gamma }\) then \(m_{\tilde{s}} + m_{s_j} + m_{Z_\gamma } = 0\).
We verify each of the five conditions separately:
For bulk detectors, let \(m\) be arbitrary. This follows directly from bulk_detector_parity_zero.
For initial \(B_p\), this follows from initial_Bp_parity_from_zero_init.
For initial \(\tilde{s}_j\), let \(m_{s_j}\) be arbitrary. This follows from initial_stilde_from_zero_init.
For final \(B_p\), let \(m_{B_p}, m_{Z_e}\) be arbitrary and assume \(m_{B_p} = m_{Z_e}\). This follows from final_Bp_equals_product_Ze.
For final \(\tilde{s}_j\), let \(m_{\tilde{s}}, m_{s_j}, m_{Z_\gamma }\) be arbitrary and assume \(m_{\tilde{s}} = m_{s_j} + m_{Z_\gamma }\). This follows from final_stilde_parity.
For any time \(t {\lt} t_i\) and any check index \(j\), there exists a bulk original check detector for \(s_j\) at time \(t\).
We provide the witness \(\langle \mathrm{originalCheck}(j), t, \mathrm{bulk} \rangle \) and verify membership using bulk_detector_exists_originalCheck.
For any time \(t\) with \(t_i {\lt} t {\lt} t_o\), bulk detectors exist for all Gauss law operators \(A_v\), all flux operators \(B_p\), and all deformed checks \(\tilde{s}_j\).
We verify each of the three conjuncts. For Gauss law operators, given \(v\), we provide the witness and use bulk_detector_exists_gaussLaw. For flux operators, given \(p\), we use bulk_detector_exists_flux. For deformed checks, given \(j\), we use bulk_detector_exists_deformedCheck.
At \(t = t_i\), initial boundary detectors exist for all flux operators \(B_p\) and all deformed checks \(\tilde{s}_j\).
We verify both conjuncts. For flux operators, given \(p\), we provide the witness and use initial_boundary_detector_exists_flux. For deformed checks, given \(j\), we use initial_boundary_detector_exists_deformedCheck.
At \(t = t_o\), final boundary detectors exist for all flux operators \(B_p\) and all deformed checks \(\tilde{s}_j\).
We verify both conjuncts. For flux operators, given \(p\), we provide the witness and use final_boundary_detector_exists_flux. For deformed checks, given \(j\), we use final_boundary_detector_exists_deformedCheck.
For any time \(t {\gt} t_o\) and any check index \(j\), there exists a bulk original check detector for \(s_j\) at time \(t\).
We provide the witness \(\langle \mathrm{originalCheck}(j), t, \mathrm{bulk} \rangle \) and verify membership using bulk_detector_exists_originalCheck.
A fault location in spacetime consists of a time step and a qubit index.
If two consecutive measurement outcomes differ (\(m_{\mathrm{before}} \neq m_{\mathrm{after}}\)), then the bulk detector parity is nonzero: \(\mathrm{bulkDetectorParity}(m_{\mathrm{before}}, m_{\mathrm{after}}) \neq 0\).
Suppose for contradiction that the parity is zero. By bulk_parity_zero_iff_equal, this implies \(m_{\mathrm{before}} = m_{\mathrm{after}}\), contradicting the hypothesis \(m_{\mathrm{before}} \neq m_{\mathrm{after}}\).
If the initialization outcome and the \(B_p\) measurement outcome differ, then \(\mathrm{xorParity}(\mathrm{init}, m_{B_p}) \neq 0\).
Suppose for contradiction that \(\mathrm{xorParity}(\mathrm{init}, m_{B_p}) = 0\). By bulk_parity_zero_iff_equal (rewritten in terms of bulkDetectorParity and xorParity), this implies \(\mathrm{init} = m_{B_p}\), contradicting the hypothesis.
If the \(B_p\) measurement outcome and the product of \(Z_e\) measurements differ, then \(\mathrm{xorParity}(m_{B_p}, m_{Z_e\text{-product}}) \neq 0\).
Suppose for contradiction that \(\mathrm{xorParity}(m_{B_p}, m_{Z_e\text{-product}}) = 0\). By bulk_parity_zero_iff_equal, this implies \(m_{B_p} = m_{Z_e\text{-product}}\), contradicting the mismatch hypothesis.
The count of bulk detectors at a single time step before or after deformation is \(n_{\mathrm{checks}}\).
The count of bulk detectors at a single time step during deformation is \(n_V + n_C + n_{\mathrm{checks}}\).
The count of boundary detectors at \(t = t_i\) is \(n_C + n_{\mathrm{checks}}\).
The count of boundary detectors at \(t = t_o\) is \(n_C + n_{\mathrm{checks}}\).
If \(k \geq 1\), \(\mathrm{outcomes}(0) = m_0\), \(\mathrm{outcomes}(k) = m_k\), and all consecutive outcomes are equal (i.e., \(\mathrm{outcomes}(i) = \mathrm{outcomes}(i+1)\) for \(i {\lt} k\)), then \(m_0 = m_k\).
We chain all consecutive equalities by induction on \(i\) to show \(\mathrm{outcomes}(0) = \mathrm{outcomes}(i)\) for all \(i \leq k\). The base case \(i = 0\) is trivial by reflexivity. For the inductive step, assuming \(\mathrm{outcomes}(0) = \mathrm{outcomes}(j)\) and \(j {\lt} k\), we have \(\mathrm{outcomes}(j) = \mathrm{outcomes}(j+1)\) by hypothesis, so \(\mathrm{outcomes}(0) = \mathrm{outcomes}(j+1)\) by transitivity. Then \(m_0 = \mathrm{outcomes}(0) = \mathrm{outcomes}(k) = m_k\).
The XOR of consecutive bulk detector parities telescopes to the endpoints. For a sequence of outcomes \(a_0, a_1, \ldots , a_{n+1}\):
This is because in \(\mathbb {Z}/2\mathbb {Z}\), \((a_0 + a_1) + (a_1 + a_2) + \cdots + (a_n + a_{n+1}) = a_0 + a_{n+1}\), since middle terms appear twice and cancel.
We unfold the definitions and proceed by induction on \(n\). For the base case \(n = 0\), the range has a single element and the sum equals \(a_0 + a_1\) directly. For the inductive step, we use \(\sum _{i=0}^{m+1} = \sum _{i=0}^{m} + (a_{m+1} + a_{m+2})\). By the induction hypothesis, \(\sum _{i=0}^{m} = a_0 + a_{m+1}\). Thus the sum becomes \((a_0 + a_{m+1}) + (a_{m+1} + a_{m+2})\). By associativity and the \(\mathbb {Z}/2\mathbb {Z}\) cancellation \(a_{m+1} + a_{m+1} = 0\), this simplifies to \(a_0 + 0 + a_{m+2} = a_0 + a_{m+2}\).
Boundary times are distinct from interior times:
For the first part, assume \(\mathrm{isStart}(t_i)\) and \(\mathrm{isDuring}(t_i)\). Unfolding \(\mathrm{isDuring}\), we have \(t_i {\lt} t_i\), contradicting irreflexivity. For the second part, assume \(\mathrm{isEnd}(t_o)\) and \(\mathrm{isDuring}(t_o)\). Unfolding, we have \(t_o {\lt} t_o\), again a contradiction.
If \(t_o {\gt} t_i + 1\), then there exists a time \(t\) with \(\mathrm{isDuring}(t)\).
We take \(t = t_i + 1\). Then \(t_i {\lt} t_i + 1\) holds by the successor property, and \(t_i + 1 {\lt} t_o\) holds by hypothesis.
The elementary detectors form a generating set for the fault-tolerant gauging measurement procedure. This is established through eight conditions:
Part 1 — Verification:
For all \(m\), \(\mathrm{bulkDetectorParity}(m, m) = 0\).
\(\mathrm{xorParity}(0, 0) = 0\).
For all \(m_{s_j}\), \(\mathrm{xorParity}(m_{s_j}, m_{s_j} + 0) = 0\).
For all \(m_{B_p}, m_{Z_e}\) with \(m_{B_p} = m_{Z_e}\), \(\mathrm{xorParity}(m_{B_p}, m_{Z_e}) = 0\).
For all \(m_{\tilde{s}}, m_{s_j}, m_{Z_\gamma }\) with \(m_{\tilde{s}} = m_{s_j} + m_{Z_\gamma }\), \(m_{\tilde{s}} + m_{s_j} + m_{Z_\gamma } = 0\).
Part 2 — Completeness:
For all \(t {\lt} t_i\) and all check indices \(j\), there exists a bulk detector for \(s_j\) at \(t\).
For all cycle indices \(p\) and check indices \(j\), initial boundary detectors exist.
For all cycle indices \(p\) and check indices \(j\), final boundary detectors exist.
We verify each of the eight conditions:
For bulk detectors, this follows from bulk_detector_parity_zero.
By simplification, \(0 + 0 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\).
By simplification using the definition of xorParity and the \(\mathbb {Z}/2\mathbb {Z}\) self-addition lemma.
Rewriting with \(m_{B_p} = m_{Z_e}\), this reduces to \(\mathrm{xorParity}(m_{Z_e}, m_{Z_e}) = 0\).
This follows from final_stilde_parity.
Given \(t {\lt} t_i\) and check \(j\), we obtain the detector from detectors_exist_before and project out the operator type.
For the initial boundary, we apply each component of detectors_exist_initial_boundary and project.
For the final boundary, we apply each component of detectors_exist_final_boundary and project.