37 Rem 16: Boundary Rounds Overkill
The \(d\) rounds of error correction in the original code before and after the gauging measurement (Phases 1 and 3 in Def 10) are conservative and often unnecessary in practice.
Justification for \(d\) rounds: The \(d\) rounds ensure that any error process involving both the gauging measurement and the initial/final boundary has weight greater than \(d\), where \(d\) is the distance of the original \([\! [n,k,d]\! ]\) stabilizer code. This facilitates a clean proof of the fault-distance bound (Thm 2).
In practice:
When the gauging measurement is part of a larger fault-tolerant computation, the surrounding operations provide natural boundaries for the spacetime fault analysis.
A constant number of rounds before and after may suffice.
The optimal number depends on the specific computation and affects the effective distance and threshold.
Point 1: The All-or-None Property is Purely Phase 2
The critical all-or-none property states that for a syndrome-free fault, each vertex \(v\) has either ALL \(d\) Gauss \(A_v\) measurements faulted or NONE of them. This is enforced by the Phase 2 repeated Gauss detectors, which pair consecutive \(A_v\) measurements within Phase 2. Crucially, this property does NOT use Phase 1 or Phase 3 detectors at all.
The all-or-none property (each vertex has \(0\) or \(d\) Gauss faults) is enforced by Phase 2 repeated Gauss detectors. Given any syndrome-free fault \(F\), the Gauss fault count for each vertex \(v\) satisfies
This uses only Phase 2’s repeated Gauss detectors, not Phases 1 or 3.
This follows directly from gaussFaultCount_zero_or_d, which establishes the all-or-none dichotomy for any syndrome-free gauging fault using only the Phase 2 repeated Gauss detector structure.
The time-fault distance lower bound (pure-time logical faults have weight \(\geq d\)) follows from the all-or-none property and sign-flip analysis, both of which are Phase 2 phenomena. Specifically, if \(F\) is a pure-time fault that is syndrome-free and flips the gauging sign, and \(d\) is odd, then
This does not depend on the number of Phase 1 or Phase 3 rounds.
This follows directly from pureTime_logicalFault_weight_ge_d, which establishes that any pure-time logical fault (syndrome-free, sign-flipping) must have weight at least \(d\), using only the Phase 2 all-or-none structure.
Point 2: Boundary Detectors Connect Phases
The boundary detectors bridge Phase \(1 \leftrightarrow 2\) and Phase \(2 \leftrightarrow 3\) respectively. These detectors involve the LAST measurement of Phase 1 (or Phase 2), the FIRST measurement of Phase 2 (or Phase 3), and edge initialization or readout events. Only one round from each boundary phase participates in these detectors.
The boundary detector at \(t_i\) connects the last Phase 1 round to the first Phase 2 round for deformed checks. It includes exactly one measurement from Phase 1 (the last round \(r = d-1\)) and one from Phase 2 (the first round \(r = 0\)), plus edge initialization events. Specifically, for \(d \geq 2\) and any check index \(j\), the Phase 1 measurement at round \(r_{\mathrm{last}} = d-1\) belongs to the measurements of the deformed initialization detector.
This follows directly from deformedInitDetector_has_phase1, which witnesses that the Phase 1 measurement at the last round is contained in the boundary detector’s measurement set.
The boundary detector at \(t_o\) connects the last Phase 2 round to the first Phase 3 round for deformed checks. It includes exactly one measurement from Phase 2 (the last round \(r = d-1\)) and one from Phase 3 (the first round \(r = 0\)), plus edge \(Z\) readout events. Specifically, for \(d \geq 2\) and any check index \(j\), the Phase 3 measurement at round \(r_{\mathrm{first}} = 0\) belongs to the measurements of the deformed ungauge detector.
This follows directly from deformedUngaugeDetector_has_originalCheck, which witnesses that the Phase 3 measurement at the first round is contained in the boundary detector’s measurement set.
Point 3: Only One Boundary Round Needed for Boundary Coverage
The boundary detectors only use ONE measurement from Phase 1 (the last round \(r = d-1\)) and ONE from Phase 3 (the first round \(r = 0\)). The remaining \(d-1\) rounds in each phase form repeated-measurement detectors pairing consecutive rounds of the same check. A single boundary round (\(d_{\mathrm{boundary}} = 1\)) would suffice for the boundary detector coverage.
Within Phase 1, the repeated detectors pair consecutive rounds of the same check. These are independent of the Phase \(1 \leftrightarrow 2\) boundary detector and provide only standard error correction. For any check index \(j\) and consecutive rounds \(r, r'\) with \(r + 1 = r'\), both Phase 1 measurements at rounds \(r\) and \(r'\) belong to the parametric repeated detector’s measurement set.
We verify both membership conditions separately. For the first measurement at round \(r\): it is the left element of the insert, so membership follows from \(\operatorname {Or.inl}(\operatorname {rfl})\). For the second measurement at round \(r'\): it is the singleton element, so membership follows from \(\operatorname {Or.inr}(\operatorname {mem\_ singleton.mpr}(\operatorname {rfl}))\).
The full measurement coverage theorem requires \(d \geq 2\). With \(d = 1\), there are no repeated detectors within Phase 1 or Phase 3 (since there is only one round each), but the boundary detectors still cover the single boundary measurement. The condition \(d \geq 2\) comes from needing at least 2 rounds for the repeated Gauss detectors in Phase 2. Formally, for \(d \geq 2\) and assuming every edge is covered by some cycle, every measurement label \(m\) belongs to some detector:
This follows directly from every_measurement_covered, which establishes the complete measurement coverage property given \(d \geq 2\) and the edge coverage hypothesis.
Point 4: \(d\) Rounds Used in Theorem 2’s Clean Proof
The full \(d\) rounds in Phases 1 and 3 are used in Theorem 2 to ensure that ANY spacetime fault (not just pure-time faults) has weight \(\geq d\). The argument uses the space-time decoupling: \(F\) decomposes as \(F = F_S \cdot F_T \cdot S\). For time-faults, the lower bound uses the all-or-none property (Phase 2 only). For space-faults, the lower bound uses the space distance \(d^* \geq d\). The \(d\) boundary rounds ensure that the space-time decoupling can move all space-faults to time \(t_i\) using time-propagating generators that span all phases.
Theorem 2 uses the full \(d\)-round structure to establish \(d_{\mathrm{spacetime}} = d\). Under the hypotheses that the original code has distance \(d\), the graph \(G\) is connected with \(|V| \geq 2\), the cycle/boundary exactness conditions hold, the graph has sufficient expansion, the deformed code has logical operators, and a minimum-weight pure-\(X\) logical operator exists that does not become a deformed stabilizer, the gauging spacetime fault distance equals \(d\):
The \(d\) rounds in Phases 1 and 3 are conservative but yield a clean proof.
This follows directly from FaultTolerantGaugingDistance.spacetimeFaultDistance_eq_d, which combines the space distance bound (\(d^* \geq d\) from sufficient expansion and Cheeger constant), the time distance bound (from the all-or-none property), and the space-time decoupling to establish the exact equality \(d_{\mathrm{spacetime}} = d\).
Point 5: Space-Faults at \(t_i\) Caught by Phase 2
Space-faults concentrated at time \(t_i\) (the gauging time) are detected by the deformed code checks measured during Phase 2. The syndrome-free condition forces the Pauli error to be in the centralizer of the deformed code. This mechanism is purely Phase 2 and does not require Phases 1 or 3.
A pure-space fault with no time-faults is syndrome-free: space-faults do not flip measurement outcomes, so no detector is violated. Detection of space-faults relies on their Pauli-group effect on the code state, not on measurement faults. This is purely Phase 2 structure (deformed code checks at \(t_i\)). Formally, if \(F\) is a pure-space fault (i.e., \(F.\mathit{timeFaults} = \emptyset \)), then \(F\) is syndrome-free with respect to all gauging detectors.
Let \(\mathit{idx}\) be an arbitrary detector index. Since \(F\) is a pure-space fault, we have \(F.\mathit{timeFaults} = \emptyset \). Rewriting with this fact, the detector applied to an empty set of time-faults is not violated, which follows from Detector.not_isViolated_no_faults.
Pure-space faults preserve the gauging sign \(\sigma \): the sign is determined entirely by time-faults (measurement errors on Gauss’s law checks), so space-faults at \(t_i\) have no effect on \(\sigma \). Formally, if \(F\) is a pure-space fault, then \(F\) preserves the gauging sign.
Unfolding the definitions of \(\operatorname {PreservesGaugingSign}\) and \(\operatorname {gaussSignFlip}\), since \(F\) is a pure-space fault we have \(F.\mathit{timeFaults} = \emptyset \). Rewriting with this, the sum over the empty set is zero by \(\operatorname {Finset.sum\_ empty}\), and simplification completes the proof.
Summary
The key fault-distance mechanisms and their phase dependence are summarized as follows. For any vertex \(v\), check index \(j\), and syndrome-free fault \(F\):
All-or-none is Phase 2 only: \(\operatorname {gaussFaultCount}(v, F) = 0 \; \lor \; \operatorname {gaussFaultCount}(v, F) = d\).
Boundary detector uses 1 Phase 1 measurement: The Phase 1 measurement at round \(r = d-1\) belongs to the deformed initialization detector’s measurements.
Boundary detector uses 1 Phase 3 measurement: The Phase 3 measurement at round \(r = 0\) belongs to the deformed ungauge detector’s measurements.
The \(d\) boundary rounds are conservative: a constant number of boundary rounds would preserve the essential detector coverage structure.
We prove all three conjuncts using \(\operatorname {refine}\). For part (1), the all-or-none dichotomy follows directly from gaussFaultCount_zero_or_d applied to the syndrome-free hypothesis. For part (2), the Phase 1 membership follows from deformedInitDetector_has_phase1 applied to check \(j\) with the last round \(r = d-1\), the first round \(r' = 0\), and the cancellation proof \(d - 1 + 1 = d\). For part (3), the Phase 3 membership follows from deformedUngaugeDetector_has_originalCheck applied to check \(j\) with the corresponding round indices and cancellation proof.