MerLean-example

36 Rem 15: Flux Check Measurement Frequency

This remark explains why the fault-tolerance proof (Theorem 2) holds even if the flux checks \(B_p\) are measured much less frequently than every round, or even not directly measured at all. The key observations are:

  1. \(B_p\) can be inferred from initialization (\(|0\rangle _e\) at \(t_i\)) and final readout (\(Z_e\) at \(t_o\)) without direct measurement, since \(B_p = \prod _{e \in p} Z_e\) and \(|0\rangle _e\) is a \(+1\) eigenstate of \(Z_e\).

  2. The distance bound from Lemma 3 does not require \(B_p\) measurements; it only requires \(B_p\) to be stabilizers of the code.

  3. The time-fault analysis (Lemma 6) shows \(A_v\) measurement faults are the bottleneck for time-fault distance, not \(B_p\).

Caveats:

  1. Without frequent \(B_p\) measurements, detector cells become large (spanning \(t_i\) to \(t_o\)).

  2. Large detectors prevent achieving a threshold against random noise.

  3. For small fixed code instances, this approach may be practical.

Theorem 989 Flux Inferred from Init Readout

The flux init detector (\(B_p^{t_i}\)) captures the relationship between edge initialization and the first flux measurement. For every edge \(e \in p\) belonging to the cycle of plaquette \(p\), the edge initialization event for \(e\) is contained in the measurements of the flux init detector. This means \(B_p = \prod _{e \in p} Z_e\) is encoded via \(|0\rangle \) initialization.

Proof

Let \(e\) be an edge with \(e \in \mathrm{cycles}(p)\). This follows directly from the lemma fluxInitDetector_has_edgeInit, which states that the flux init detector for plaquette \(p\) contains the edge initialization measurement for each edge \(e\) in the cycle.

Theorem 990 Flux Inferred from Readout

The flux ungauge detector (\(B_p^{t_o}\)) captures the relationship between the last flux measurement and individual \(Z_e\) readouts for \(e \in p\). For every edge \(e\) in the cycle of plaquette \(p\), the Phase 3 edge-\(Z\) readout measurement for \(e\) is contained in the measurements of the flux ungauge detector.

Proof

Let \(e\) be an edge with \(e \in \mathrm{cycles}(p)\). This follows directly from the lemma fluxUngaugeDetector_has_edgeZ, which states that the flux ungauge detector for plaquette \(p\) at the last round contains the Phase 3 edge-\(Z\) measurement for each edge in the cycle.

Theorem 991 Flux Init Contains First Measurement

The flux init detector also contains the first \(B_p\) measurement in Phase 2. This single measurement, together with the edge initializations, suffices to capture \(B_p\) information — no repeated \(B_p\) measurements are needed.

Proof

This follows directly from fluxInitDetector_has_flux, which states that the flux init detector for plaquette \(p\) at round \(0\) contains the Phase 2 flux measurement at round \(0\).

Theorem 992 Flux Ungauge Contains Last Measurement

The flux ungauge detector contains the last \(B_p\) measurement in Phase 2.

Proof

This follows directly from fluxUngaugeDetector_has_flux, which states that the flux ungauge detector for plaquette \(p\) at the last round (\(d-1\)) contains the Phase 2 flux measurement at that round.

Lemma 3’s distance bound requires only that \(B_p\) operators are elements of the deformed stabilizer group, which is an algebraic fact. No measurement of \(B_p\) is needed for \(d^* \geq d\). Formally, given a stabilizer code \(C\) with checks, a deformed code data, connectivity, the exactness conditions, and sufficient expansion \(h(G) \geq 1\), we have

\[ d(C) \leq d(\text{deformed code}). \]
Proof

This follows directly from the space distance theorem deformed_distance_ge_d_sufficient_expansion, which establishes that when the graph \(G\) has sufficient expansion, the deformed code distance is at least the original code distance. The proof uses only algebraic properties of flux operators as stabilizers, connectivity, coboundary exactness, and the Cheeger expansion bound — no flux measurements are required.

Theorem 994 Time Fault Bottleneck Is Gauss

The time-fault distance is determined by \(A_v\) measurement strings, not \(B_p\). The canonical minimum-weight pure-time logical fault is a single \(A_v\) string of weight \(d\). For any vertex \(v\) and odd \(d\):

\[ d_{\mathrm{time}} \leq d. \]
Proof

This follows directly from timeFaultDistance_le_d, which provides the upper bound by exhibiting the Gauss string fault for vertex \(v\) as a syndrome-free, sign-flipping pure-time fault of weight \(d\).

Theorem 995 Gauss String Weight

The \(A_v\) measurement string has weight exactly \(d\):

\[ w(\mathrm{gaussStringFault}(v)) = d. \]
Proof

This follows directly from gaussStringFault_weight_eq_d.

Theorem 996 Gauss String Is Syndrome Free

The \(A_v\) string is syndrome-free: consecutive repeated Gauss detectors see paired flips that cancel. This does not involve any flux detectors.

Proof

This follows directly from gaussStringFault_syndromeFree.

Theorem 997 Gauss String Flips Sign

The \(A_v\) string flips the gauging sign when \(d\) is odd.

Proof

This follows directly from gaussStringFault_flipsSign_of_odd, applied to vertex \(v\) and the hypothesis that \(d\) is odd.

Theorem 998 Flux Fault Preserves Sign

\(B_p\) measurement faults cannot flip the gauging sign \(\sigma \). The sign \(\sigma = \sum _v \varepsilon _v\) is defined as a sum over Gauss measurement outcomes only. A fault \(F\) whose time faults contain only flux measurements contributes \(0\) to this sum: no \(A_v\) measurement is faulted. Formally, if every time fault \(\mathrm{tf} \in F.\mathrm{timeFaults}\) is of the form \(\mathrm{phase2}(\mathrm{flux}\; p\; r)\) for some plaquette \(p\) and round \(r\), then \(F\) preserves the gauging sign.

Proof

We unfold the definitions of PreservesGaugingSign and gaussSignFlip. The gauging sign flip is a double sum \(\sum _{v \in V} \sum _{r \in \mathrm{Fin}\, d}\) of indicators. We apply Finset.sum_eq_zero twice: for each vertex \(v\) and each round \(r\), it suffices to show the indicator is zero.

We split on the conditional. In the case where the indicator is \(1\), we have the hypothesis \(h\) that the Gauss measurement \(\langle \mathrm{phase2}(\mathrm{gaussLaw}\; v\; r) \rangle \) is in \(F.\mathrm{timeFaults}\). But by assumption, all time faults are flux measurements. We obtain a plaquette \(p\) and round \(r'\) such that \(\langle \mathrm{phase2}(\mathrm{gaussLaw}\; v\; r) \rangle = \langle \mathrm{phase2}(\mathrm{flux}\; p\; r') \rangle \). Extracting the measurement field equality, we get \(\mathrm{phase2}(\mathrm{gaussLaw}\; v\; r) = \mathrm{phase2}(\mathrm{flux}\; p\; r')\). Since phase2 is injective, this gives \(\mathrm{gaussLaw}\; v\; r = \mathrm{flux}\; p\; r'\), which is impossible by constructor disjointness. In the other case, the result holds by reflexivity.

Theorem 999 Gauss Sign Flip Ignores Flux

The gauging sign is determined entirely by \(A_v\) measurement faults. The gaussSignFlip for the Gauss string fault at vertex \(v\) equals

\[ \sum _{w \in V} \sum _{r \in \mathrm{Fin}\, d} \begin{cases} 1 & \text{if } \langle \mathrm{phase2}(\mathrm{gaussLaw}\; w\; r) \rangle \in (\mathrm{gaussStringFault}\; v).\mathrm{timeFaults} \\ 0 & \text{otherwise} \end{cases} \]

which sums indicators of \(A_v\) membership in time faults only, ignoring all non-Gauss faults.

Proof

This holds by reflexivity (definitional unfolding).

Theorem 1000 Time Fault Distance Equals \(d\)

The full time-fault distance result from Lemma 6: for any vertex \(v\), odd \(d\), and nonempty vertex set \(V\),

\[ d_{\mathrm{time}} = d. \]
Proof

This follows directly from timeFaultDistance_eq_d, which combines the upper bound (from the Gauss string fault of weight \(d\)) with the lower bound (any syndrome-free sign-flipping pure-time fault has weight \(\geq d\)).

Theorem 1001 Repeated vs Boundary Detector Weight

Repeated flux detectors have weight \(2\) (two consecutive \(B_p\) measurements). Formally, for any plaquette \(p\) and consecutive rounds \(r, r'\) with \(r + 1 = r'\):

\[ |\mathrm{phase2RepeatedDetector\_ flux}(p, r, r').\mathrm{measurements}| = 2. \]
Proof

We simplify using the definition of phase2RepeatedDetector_flux and compute the cardinality of the pair. To show the two measurements are distinct, we assume for contradiction that they are equal. Since phase2 is injective and flux is injective, this would imply \(r = r'\). Substituting, we obtain \(r + 1 = r\) from the hypothesis \(r + 1 = r'\), which is a contradiction by integer arithmetic.

Theorem 1002 Flux Boundary Detector Spans Full Duration

Without repeated flux detectors, the boundary detectors span the full Phase 2 duration \(d\). Formally:

\[ \mathrm{phase2Start} \leq \mathrm{phase3Start} \quad \text{and} \quad \mathrm{phase3Start} - \mathrm{phase2Start} = d. \]
Proof

The first conjunct follows from phase2Start_le_phase3Start and the second from phase2_duration.

Theorem 1003 Boundary Larger Than Repeated

Large detector cells: the number of measurements in a boundary detector (\(|p| + 1\) for flux init) is strictly greater than a repeated detector (\(2\)), as soon as the cycle has at least \(2\) edges. Formally, if \(|\{ e \in G.\mathrm{edgeSet} \mid e \in \mathrm{cycles}(p)\} | \geq 2\), then

\[ |\mathrm{phase2RepeatedDetector\_ flux}(p, r, r').\mathrm{measurements}| {\lt} |\{ e \mid e \in \mathrm{cycles}(p)\} | + 1. \]
Proof

We rewrite using the fact that the repeated detector has cardinality \(2\) (from repeated_vs_boundary_detector_weight). Then the inequality \(2 {\lt} |p| + 1\) follows by integer arithmetic from the hypothesis \(2 \leq |p|\).

The space-distance bound \(d^* \geq d\) (Lemma 3) requires \(h(G) \geq 1\) and exactness. No measurement of flux checks \(B_p\) is needed — only their algebraic presence as stabilizers of the deformed code. Formally, for any plaquette \(p\):

\[ \mathrm{fluxChecks}(G, \mathrm{cycles}, p) \in \mathrm{stabilizerGroup}(\text{deformed code}). \]
Proof

This follows directly from flux_mem_stabilizerGroup, which establishes algebraically that every flux operator belongs to the stabilizer group of the deformed code.

Theorem 1005 Flux in Centralizer Algebraically

Flux operators are also in the centralizer (commute with all checks), which is the property actually used in Lemma 3. For any plaquette \(p\):

\[ \mathrm{inCentralizer}(\text{deformed code}, \mathrm{fluxChecks}(G, \mathrm{cycles}, p)). \]
Proof

This follows directly from flux_inCentralizer, which establishes that flux checks commute with all checks of the deformed code.