29 Lem 4: Spacetime Code Detectors
This chapter establishes that the local detectors in the fault-tolerant gauging measurement procedure form a complete generating set. For the original code phases (\(t {\lt} t_i\) and \(t {\gt} t_o\)), detectors arise from repeated measurements of checks \(s_j\) at consecutive rounds. During the deformed code phase (\(t_i {\lt} t {\lt} t_o\)), detectors come from repeated measurements of deformed code checks \(A_v\), \(B_p\), and \(\tilde{s}_j\). At the gauging boundary \(t = t_i\), detectors combine edge qubit initializations with first measurements; at the ungauging boundary \(t = t_o\), detectors combine last measurements with \(Z_e\) readouts.
Let \(\alpha \) be a type with decidable equality and let \(\{ \text{generators}_i\} _{i \in \iota }\) be a family of finsets over \(\alpha \). A finset \(S\) is \(\mathbb {Z}_2\)-generated by the generators if \(S\) can be obtained from \(\emptyset \) by iterated symmetric differences with generators. Formally, this is defined inductively:
\(\emptyset \) is generated.
If \(S\) is generated, then \(S \mathbin {\triangle } \text{generators}_i\) is generated for any \(i \in \iota \).
Each generator \(\text{generators}_i\) is in the \(\mathbb {Z}_2\) span.
We have \(\text{generators}_i = \emptyset \mathbin {\triangle } \text{generators}_i\). Since \(\emptyset \) is generated (by the base case), the symmetric difference rule gives that \(\emptyset \mathbin {\triangle } \text{generators}_i\) is generated. By the identity \(\bot \mathbin {\triangle } x = x\) (where \(\bot = \emptyset \)), this equals \(\text{generators}_i\).
If \(S\) and \(T\) are both \(\mathbb {Z}_2\)-generated by the generators, then \(S \mathbin {\triangle } T\) is also generated.
We proceed by induction on the derivation that \(T\) is generated, generalizing over \(S\).
Base case (\(T = \emptyset \)): We have \(S \mathbin {\triangle } \emptyset = S \mathbin {\triangle } \bot = S\), which is generated by assumption.
Inductive step (\(T = U \mathbin {\triangle } \text{generators}_i\) where \(U\) is generated): By the induction hypothesis applied to \(S\), we know \(S \mathbin {\triangle } U\) is generated. By associativity of symmetric difference, \(S \mathbin {\triangle } (U \mathbin {\triangle } \text{generators}_i) = (S \mathbin {\triangle } U) \mathbin {\triangle } \text{generators}_i\). Since \(S \mathbin {\triangle } U\) is generated, the symmetric difference rule gives the result.
Given a fault-tolerant gauging procedure and a cycle \(p \in C\), the cycle edges of \(p\) is the finset of edges \(e \in G.\text{edgeSet}\) such that \(e \in \text{cycles}(p)\).
Given a fault-tolerant gauging procedure and a check index \(j \in J\), the edge-path edges of \(j\) is the finset of edges \(e \in G.\text{edgeSet}\) such that \(\text{edgePath}(j, e) \neq 0\) in \(\mathbb {Z}/2\mathbb {Z}\).
Given a fault-tolerant gauging procedure, a check index \(j \in J\), consecutive rounds \(r, r' \in \operatorname {Fin}(d)\) with \(r + 1 = r'\), and an outcome \(\sigma \in \mathbb {Z}/2\mathbb {Z}\), the Phase 1 repeated detector is the detector with:
Measurements: \(\{ \texttt{phase1}(j, r),\; \texttt{phase1}(j, r')\} \).
Ideal outcome: \(\sigma \) on both measurements, \(0\) otherwise.
Constraint: \(\sigma + \sigma = 0\) in \(\mathbb {Z}/2\mathbb {Z}\) (by characteristic 2).
The outcome \(\sigma \) represents the unknown but equal eigenvalue of both measurements of the self-inverse check \(s_j\).
Given a fault-tolerant gauging procedure, a check index \(j \in J\), consecutive rounds \(r, r' \in \operatorname {Fin}(d)\) with \(r + 1 = r'\), and an outcome \(\sigma \in \mathbb {Z}/2\mathbb {Z}\), the Phase 3 repeated detector is the detector with:
Measurements: \(\{ \texttt{phase3}(\texttt{originalCheck}(j, r)),\; \texttt{phase3}(\texttt{originalCheck}(j, r'))\} \).
Ideal outcome: \(\sigma \) on both measurements, \(0\) otherwise.
Constraint: \(\sigma + \sigma = 0\) in \(\mathbb {Z}/2\mathbb {Z}\).
Given a fault-tolerant gauging procedure, a cycle \(p \in C\), and the first round \(r_{\text{first}}\) with \(r_{\text{first}} = 0\), the flux initialization detector \(B_p^{t_i}\) is the detector with:
Measurements: \(\{ \texttt{edgeInit}(e) \mid e \in \text{cycles}(p)\} \cup \{ \texttt{phase2}(\texttt{flux}(p, r_{\text{first}}))\} \).
Ideal outcome: \(0\) for all measurements.
Constraint: \(\sum 0 = 0\).
Edge qubits initialized in \(|0\rangle \) are \(Z\)-eigenstates with eigenvalue \(+1\) (i.e., \(0\) in \(\mathbb {Z}/2\mathbb {Z}\)). Since \(B_p = \prod _{e \in p} Z_e\) is pure \(Z\)-type, \(B_p\) on these \(|0\rangle \) states gives outcome \(\sum 0 = 0\).
Given a fault-tolerant gauging procedure, a check index \(j \in J\), the last Phase 1 round \(r_{\text{last}}\) with \(r_{\text{last}} + 1 = d\), the first Phase 2 round \(r_{\text{first}} = 0\), and an outcome \(\sigma \in \mathbb {Z}/2\mathbb {Z}\), the deformed initialization detector \(\tilde{s}_j^{t_i}\) is the detector with:
Measurements: \(\{ \texttt{phase1}(j, r_{\text{last}}),\; \texttt{phase2}(\texttt{deformed}(j, r_{\text{first}}))\} \cup \{ \texttt{edgeInit}(e) \mid e \in \gamma _j\} \).
Ideal outcome: \(\sigma \) for the Phase 1 and Phase 2 deformed measurements, \(0\) for edge initializations.
Constraint: \(\sigma + \sigma + \sum 0 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\).
Since \(\tilde{s}_j = s_j \cdot \prod _{e \in \gamma _j} Z_e\) and edge qubits are initialized in \(|0\rangle \) (so \(Z_e \to +1\)), the outcomes of \(s_j\) and \(\tilde{s}_j\) agree. The parameter \(\sigma \) encodes this unknown shared eigenvalue.
Given a fault-tolerant gauging procedure, a cycle \(p \in C\), and the last round \(r_{\text{last}}\) with \(r_{\text{last}} + 1 = d\), the flux ungauging detector \(B_p^{t_o}\) is the detector with:
Measurements: \(\{ \texttt{phase2}(\texttt{flux}(p, r_{\text{last}}))\} \cup \{ \texttt{phase3}(\texttt{edgeZ}(e)) \mid e \in \text{cycles}(p)\} \).
Ideal outcome: \(0\) for all measurements.
Constraint: \(\beta _p + \sum z_e = 0\) in \(\mathbb {Z}/2\mathbb {Z}\), since \(B_p = \prod _{e \in p} Z_e\) means \(\beta _p = \sum z_e\).
Given a fault-tolerant gauging procedure, a check index \(j \in J\), the last Phase 2 round \(r_{\text{last}}\) with \(r_{\text{last}} + 1 = d\), and the first Phase 3 round \(r_{\text{first}} = 0\), the deformed ungauging detector \(\tilde{s}_j^{t_o}\) is the detector with:
Measurements: \(\{ \texttt{phase2}(\texttt{deformed}(j, r_{\text{last}})),\; \texttt{phase3}(\texttt{originalCheck}(j, r_{\text{first}}))\} \cup \{ \texttt{phase3}(\texttt{edgeZ}(e)) \mid e \in \gamma _j\} \).
Ideal outcome: \(0\) for all measurements.
Constraint: \(\tilde{\sigma }_j + \sum z_e + \sigma _j = 0\) in \(\mathbb {Z}/2\mathbb {Z}\), since \(\tilde{s}_j = s_j \cdot \prod _{e \in \gamma _j} Z_e\) implies \(\tilde{\sigma }_j = \sigma _j + \sum z_e\).
For any vertex \(v \in V\) and round \(r \in \operatorname {Fin}(d)\), the Phase 2 Gauss operator satisfies \(A_v \cdot A_v = 1\). This ensures consecutive measurements of \(A_v\) yield the same eigenvalue.
This follows directly from the general self-inverse property of Phase 2 operators applied to the Gauss law measurement \((\texttt{gaussLaw}\; v\; r)\).
For any cycle \(p \in C\) and round \(r \in \operatorname {Fin}(d)\), the Phase 2 flux operator satisfies \(B_p \cdot B_p = 1\).
This follows directly from the general self-inverse property of Phase 2 operators applied to the flux measurement \((\texttt{flux}\; p\; r)\).
For any check index \(j \in J\) and round \(r \in \operatorname {Fin}(d)\), the Phase 2 deformed operator satisfies \(\tilde{s}_j \cdot \tilde{s}_j = 1\).
This follows directly from the general self-inverse property of Phase 2 operators applied to the deformed measurement \((\texttt{deformed}\; j\; r)\).
For any cycle \(p \in C\) and round \(r \in \operatorname {Fin}(d)\), the Phase 2 flux operator \(B_p = \prod _{e \in p} Z_e\) satisfies \(\text{xVec}(B_p) = 0\). This underlies the flux boundary detector validity.
This follows directly from the Phase 2 flux pure-\(Z\) property.
For any check index \(j \in J\), round \(r \in \operatorname {Fin}(d)\), and edge \(e \in G.\text{edgeSet}\), the Phase 2 deformed operator \(\tilde{s}_j\) satisfies \(\text{xVec}(\tilde{s}_j)(\operatorname {inr}(e)) = 0\). This means \(\tilde{s}_j = s_j \cdot \prod _{e \in \gamma _j} Z_e\) has no \(X\)-support on edge qubits.
This follows directly from the Phase 2 deformed no-\(X\)-on-edges property.
For any vertex \(v \in V\) and rounds \(r, r' \in \operatorname {Fin}(d)\), the Phase 2 Gauss operator is round-independent: the same \(A_v\) is measured each round.
This holds by reflexivity: the operator definition does not depend on the round index.
For any cycle \(p \in C\) and rounds \(r, r' \in \operatorname {Fin}(d)\), the Phase 2 flux operator is round-independent: the same \(B_p\) is measured each round.
This holds by reflexivity: the operator definition does not depend on the round index.
For any check index \(j \in J\) and rounds \(r, r' \in \operatorname {Fin}(d)\), the Phase 2 deformed operator is round-independent: the same \(\tilde{s}_j\) is measured each round.
This holds by reflexivity: the operator definition does not depend on the round index.
The detector index type enumerates all detector generators in the spacetime code. Its constructors are:
\(\texttt{phase1Repeated}(j, r, r', h_r)\): repeated measurement of original check \(s_j\) in Phase 1, at consecutive rounds \(r, r'\) with \(r + 1 = r'\).
\(\texttt{phase2GaussRepeated}(v, r, r', h_r)\): repeated measurement of Gauss check \(A_v\) in Phase 2.
\(\texttt{phase2FluxRepeated}(p, r, r', h_r)\): repeated measurement of flux check \(B_p\) in Phase 2.
\(\texttt{phase2DeformedRepeated}(j, r, r', h_r)\): repeated measurement of deformed check \(\tilde{s}_j\) in Phase 2.
\(\texttt{phase3Repeated}(j, r, r', h_r)\): repeated measurement of original check \(s_j\) in Phase 3.
\(\texttt{fluxInit}(p)\): boundary detector \(B_p^{t_i}\) at gauging step.
\(\texttt{deformedInit}(j)\): boundary detector \(\tilde{s}_j^{t_i}\) at gauging step.
\(\texttt{fluxUngauge}(p)\): boundary detector \(B_p^{t_o}\) at ungauging step.
\(\texttt{deformedUngauge}(j)\): boundary detector \(\tilde{s}_j^{t_o}\) at ungauging step.
No standalone edge-initialization detectors are needed: edge initialization and readout events are covered by the composite boundary detectors.
The map from detector indices to actual detectors. Repeated measurement detectors take outcome \(0\) as a canonical choice (the constraint proof works for any outcome). The boundary detectors use the first/last rounds \(r = 0\) and \(r = d - 1\).
For every detector index, the corresponding detector is not violated without faults: \(\neg (\text{detectorOfIndex}(\text{idx})).\text{isViolated}(\emptyset )\).
By case analysis on the detector index; in each case, the result follows directly from the general theorem that no detector is violated when there are no faults.
For each detector index, the generator measurement set is the measurement set of the corresponding detector.
The flux initialization detector for cycle \(p\) contains the measurement \(\texttt{phase2}(\texttt{flux}(p, r_{\text{first}}))\).
The flux measurement is the singleton component of the union, so membership follows from \(\texttt{Finset.mem\_ union\_ right}\) and \(\texttt{Finset.mem\_ singleton.mpr}\) applied to reflexivity.
For any edge \(e\) in the cycle \(p\), the flux initialization detector contains the edge initialization measurement \(\texttt{edgeInit}(e)\).
The edge initialization is in the image part of the union. Since \(e \in \text{cycles}(p)\), we have \(e\) in the filtered finset, and its image under the \(\texttt{edgeInit}\) map gives the desired membership.
The flux ungauging detector for cycle \(p\) contains the measurement \(\texttt{phase2}(\texttt{flux}(p, r_{\text{last}}))\).
The flux measurement is the singleton in the left component of the union, so membership follows directly.
For any edge \(e\) in the cycle \(p\), the flux ungauging detector contains \(\texttt{phase3}(\texttt{edgeZ}(e))\).
Since \(e \in \text{cycles}(p)\), the edge is in the filtered finset, and its image under the \(\texttt{phase3} \circ \texttt{edgeZ}\) map gives membership in the right component of the union.
The deformed ungauging detector for check \(j\) contains \(\texttt{phase2}(\texttt{deformed}(j, r_{\text{last}}))\).
This is the first element of the insert pair in the left component of the union.
The deformed ungauging detector for check \(j\) contains \(\texttt{phase3}(\texttt{originalCheck}(j, r_{\text{first}}))\).
This is the second element (the singleton) in the insert pair of the left component of the union.
For any edge \(e\) with \(\text{edgePath}(j, e) \neq 0\), the deformed ungauging detector for check \(j\) contains \(\texttt{phase3}(\texttt{edgeZ}(e))\).
Since \(\text{edgePath}(j, e) \neq 0\), the edge \(e\) is in the filtered finset \(\text{edgePathEdges}(j)\), and its image under \(\texttt{phase3} \circ \texttt{edgeZ}\) lies in the right component of the union.
The deformed initialization detector for check \(j\) contains \(\texttt{phase1}(j, r_{\text{last}})\).
This is the first element of the insert pair in the left component of the union.
The deformed initialization detector for check \(j\) contains \(\texttt{phase2}(\texttt{deformed}(j, r_{\text{first}}))\).
This is the second element (the singleton) of the insert pair in the left component of the union.
For any edge \(e\) with \(\text{edgePath}(j, e) \neq 0\), the deformed initialization detector contains \(\texttt{edgeInit}(e)\).
Since \(\text{edgePath}(j, e) \neq 0\), the edge \(e\) is in the filtered finset \(\text{edgePathEdges}(j)\), and its image under \(\texttt{edgeInit}\) lies in the right component of the union.
Phase 1 measurements are covered by repeated or boundary detectors:
If \(r + 1 {\lt} d\), then \(\texttt{phase1}(j, r)\) is in the Phase 1 repeated detector for \((j, r, r+1)\).
If \(r + 1 = d\), then \(\texttt{phase1}(j, r)\) is in the deformed initialization detector for \(j\).
In the first case, \(\texttt{phase1}(j, r)\) is the first element inserted into the pair. In the second case, it is the first element of the insert pair in the left component of the union of the deformed init detector.
Phase 2 Gauss measurements are covered by Gauss repeated detectors (assuming \(d \geq 2\)):
If \(r + 1 {\lt} d\), then \(\texttt{phase2}(\texttt{gaussLaw}(v, r))\) is in the forward repeated detector.
If \(0 {\lt} r\), then it is in the backward repeated detector pairing round \(r-1\) with \(r\).
In the first case, the measurement is the first element inserted into the pair. In the second case, it is the second element (the singleton) of the pair.
Phase 2 flux measurements are covered by init, ungauge, or repeated detectors:
If \(r = 0\), the measurement is in the flux init detector.
If \(r + 1 = d\), the measurement is in the flux ungauge detector.
If \(r + 1 {\lt} d\), the measurement is in a flux repeated detector.
In the first case, the flux measurement is in the right component (singleton) of the flux init union. In the second case, it is in the left component (singleton) of the flux ungauge union. In the third case, it is the first element of the insert pair in the repeated detector.
Phase 2 deformed measurements are covered by init, ungauge, or repeated detectors:
If \(r = 0\), the measurement is in the deformed init detector.
If \(r + 1 = d\), the measurement is in the deformed ungauge detector.
If \(r + 1 {\lt} d\), the measurement is in a deformed repeated detector.
We prove each case separately. For \(r = 0\): the deformed measurement is the second element of the insert pair in the deformed init detector’s left union component. For \(r + 1 = d\): it is the first element of the insert pair in the deformed ungauge detector. For \(r + 1 {\lt} d\): it is the first element of the insert pair in the repeated detector.
Phase 3 original check measurements are covered:
If \(r = 0\), the measurement is in the deformed ungauge detector.
If \(0 {\lt} r\), the measurement is in a Phase 3 repeated detector pairing round \(r-1\) with \(r\).
For \(r = 0\): the original check measurement is the second element of the insert pair in the deformed ungauge detector’s left union component. For \(0 {\lt} r\): it is the second element (singleton) of the pair in the Phase 3 repeated detector.
For any cycle \(p\) containing edge \(e\), the measurement \(\texttt{phase3}(\texttt{edgeZ}(e))\) is in the flux ungauging detector for \(p\).
This follows directly from the membership lemma for the flux ungauge detector.
For any check \(j\) with \(\text{edgePath}(j, e) \neq 0\), the measurement \(\texttt{phase3}(\texttt{edgeZ}(e))\) is in the deformed ungauging detector for \(j\).
This follows directly from the membership lemma for the deformed ungauge detector.
For any cycle \(p\) containing edge \(e\), the edge initialization measurement \(\texttt{edgeInit}(e)\) is in the flux initialization detector for \(p\).
This follows directly from the membership lemma for the flux init detector.
For any check \(j\) with \(\text{edgePath}(j, e) \neq 0\), the edge initialization measurement \(\texttt{edgeInit}(e)\) is in the deformed initialization detector for \(j\).
This follows directly from the membership lemma for the deformed init detector.
Assuming \(d \geq 2\) and that every edge qubit is in at least one cycle, every measurement in the procedure participates in at least one of the listed detector generators. Formally: for every measurement label \(m\), there exists a detector index \(\text{idx}\) such that \(m \in (\text{detectorOfIndex}(\text{idx})).\text{measurements}\).
We proceed by case analysis on the measurement label \(m\).
Case \(m = \texttt{phase1}(j, r)\): If \(r + 1 {\lt} d\), we use the Phase 1 repeated detector pairing rounds \(r\) and \(r + 1\), which covers \(m\) by the Phase 1 coverage lemma. If \(r + 1 = d\) (so \(r = d - 1\)), we use the deformed init detector for \(j\), and the membership follows from the Phase 1 membership lemma.
Case \(m = \texttt{edgeInit}(e)\): By the edge coverage hypothesis, there exists a cycle \(p\) with \(e \in \text{cycles}(p)\). We use the flux init detector for \(p\).
Case \(m = \texttt{phase2}(\texttt{gaussLaw}(v, r))\): If \(r + 1 {\lt} d\), we use the forward Gauss repeated detector. Otherwise \(0 {\lt} r\) (since \(d \geq 2\)), and we use the backward Gauss repeated detector pairing \(r - 1\) with \(r\).
Case \(m = \texttt{phase2}(\texttt{flux}(p, r))\): If \(r = 0\), we use the flux init detector. If \(r + 1 = d\), we use the flux ungauge detector. Otherwise \(r + 1 {\lt} d\), and we use the flux repeated detector.
Case \(m = \texttt{phase2}(\texttt{deformed}(j, r))\): If \(r = 0\), we use the deformed init detector. If \(r + 1 = d\), we use the deformed ungauge detector. Otherwise \(r + 1 {\lt} d\), and we use the deformed repeated detector.
Case \(m = \texttt{phase3}(\texttt{edgeZ}(e))\): By the edge coverage hypothesis, there exists a cycle \(p\) with \(e \in \text{cycles}(p)\). We use the flux ungauge detector for \(p\).
Case \(m = \texttt{phase3}(\texttt{originalCheck}(j, r))\): If \(r = 0\), we use the deformed ungauge detector for \(j\). If \(0 {\lt} r\), we use the Phase 3 repeated detector pairing \(r - 1\) with \(r\).
red[UNPROVEN AXIOM]
For any fault-tolerant gauging procedure with \(d \geq 2\), any detector \(D\) satisfying \(\neg D.\text{isViolated}(\emptyset )\) has its measurement set \(\mathbb {Z}_2\)-generated by the generator measurement sets. That is, \(D.\text{measurements}\) can be expressed as a symmetric difference of generator measurement sets.
Note: This is stated as an axiom because the structural argument — that within each phase, the only sources of deterministic measurement constraints are repeated measurements of self-inverse stabilizers and boundary initialization/readout relations — relies on physical reasoning about eigenvalue outcomes that was not fully formalized.
Assuming \(d \geq 2\) and that every edge is in some cycle, the listed detectors form a complete generating set for the fault-tolerant gauging procedure. Specifically:
Validity: Every generator is a valid detector (not violated without faults).
Coverage: Every measurement participates in at least one generator.
\(\mathbb {Z}_2\) closure: The \(\mathbb {Z}_2\) span is closed under symmetric difference.
Generation: Every valid detector decomposes as a \(\mathbb {Z}_2\) combination of the generators.
orange[Uses unproven axiom: thm:FaultTolerantGaugingProcedure.generators_span_all_detectors]
The four parts are established as follows:
For validity, every generator detector is not violated without faults, by the theorem detectorOfIndex_no_fault.
For coverage, every measurement participates in some generator, by the theorem every_measurement_covered applied with the hypotheses \(d \geq 2\) and edge coverage.
For \(\mathbb {Z}_2\) closure, given \(S\) and \(T\) in the \(\mathbb {Z}_2\) span, \(S \mathbin {\triangle } T\) is also in the span by the symmetric difference closure lemma.
For generation, any valid detector \(D\) with \(\neg D.\text{isViolated}(\emptyset )\) has its measurement set generated by the generators, by the axiom generators_span_all_detectors.