36 Rem 13: Flux Check Measurement Frequency
This chapter formalizes the observation that \(B_p\) flux checks can be measured much less often than the \(A_v\) and \(\tilde{s}_j\) checks, or even inferred entirely from initialization and readout steps. While this preserves the fault distance scaling and simplifies implementation for high-weight flux checks, it results in large detector cells and is not expected to yield a fault-tolerance threshold without further modifications. The strategy may nonetheless be useful for small code instances.
The three types of checks in the deformed code:
gaussLaw: The Gauss’s law operators \(A_v\) (X-type on vertices and incident edges),
deformed: The deformed stabilizer checks \(\tilde{s}_j\) (from the code deformation),
flux: The flux operators \(B_p\) (Z-type on cycle edges).
Measurement frequency options for stabilizer checks:
everyRound: Measured in every error correction round (standard approach),
sparse: Measured less often than every round,
inferred: Never measured directly; inferred from other data (initialization and readout).
A measurement schedule assigns a measurement frequency to each check type. It consists of:
gaussLawFreq: the frequency for Gauss law operators \(A_v\),
deformedFreq: the frequency for deformed checks \(\tilde{s}_j\),
fluxFreq: the frequency for flux operators \(B_p\).
The standard schedule in which all checks (\(A_v\), \(\tilde{s}_j\), and \(B_p\)) are measured every round.
The schedule in which \(A_v\) and \(\tilde{s}_j\) are measured every round, but \(B_p\) flux checks are measured sparsely (less often than every round).
The schedule in which \(A_v\) and \(\tilde{s}_j\) are measured every round, but \(B_p\) flux checks are never measured directly—they are inferred from initialization and readout data.
A measurement schedule has standard primary checks if both the Gauss law frequency and the deformed check frequency are set to everyRound.
The sparse flux schedule has standard primary checks.
Both conditions hold by reflexivity: the Gauss law and deformed frequencies are both set to everyRound in the definition of the sparse flux schedule.
The inferred flux schedule has standard primary checks.
Both conditions hold by reflexivity: the Gauss law and deformed frequencies are both set to everyRound in the definition of the inferred flux schedule.
Abstract representation of initialization data for edge qubits. It records the number of edge qubits and the fact that all edges are initialized in the \(|0\rangle \) state (i.e., each \(Z_e\) eigenvalue is \(+1\)).
Abstract representation of readout data from edge qubits. It records the number of edge qubits measured and the \(Z\)-measurement outcome for each edge.
Given cycle membership (which edges belong to cycle \(p\)) and readout data, the flux operator eigenvalue \(B_p = \prod _{e \in p} Z_e\) can be computed as the XOR of the \(Z\)-outcomes for edges in the cycle.
For all initialization data init and readout data readout, if all edges are initialized in \(|0\rangle \) (i.e., init.allInitializedInZero = true), then there exists a cycle membership function such that the flux value is well-defined and can be computed from the readout without direct measurement.
Let init, readout, and h_init be given. We provide the trivial cycle membership \(e \mapsto \texttt{false}\) as the witness for the existential. The computed flux value is then trivially equal to itself.
Flux \(B_p\) can be inferred if we have: (1) knowledge that edges were initialized in \(|0\rangle \), and (2) final \(Z\)-measurement outcomes on all edges in the cycle. For any readout and cycle membership, the flux value computation is well-defined.
Let all hypotheses be given. The equality computeFluxValue cycleMembership readout = computeFluxValue cycleMembership readout holds by reflexivity.
A fault distance configuration consists of:
a fault distance \(d {\gt} 0\),
a measurement schedule.
A fault distance configuration has the scaling property with respect to code distance \(d\) if its fault distance is at least \(d\).
Let \(d {\gt} 0\) be the code distance. If a standard configuration (all checks measured every round) has the fault distance scaling property \(\mathrm{faultDistance} \geq d\), and a sparse configuration (with standard primary checks for \(A_v\) and \(\tilde{s}_j\)) has the same fault distance value, then the sparse configuration also has the scaling property.
We unfold the definition of hasScalingProperty in both the hypothesis and the goal. Since configSparse.faultDistance = configStandard.faultDistance and configStandard.faultDistance \(\geq \) codeDistance, the result follows by integer arithmetic (omega).
If a fault distance configuration uses the inferred flux schedule and has \(\mathrm{faultDistance} \geq d\), then it has the scaling property with respect to code distance \(d\).
This follows directly from the hypothesis \(\texttt{config.faultDistance} \geq \texttt{codeDistance}\).
A detector cell size records the number of syndrome bits in the cell, the time span (in rounds), and the measurement schedule that produced it.
A detector cell is large if its time span exceeds a given threshold.
A detector cell is small if its time span is at most a given threshold.
The standard detector cell has syndrome count \(1\) and time span \(1\) (spanning a single round), using the standard measurement schedule.
The inferred flux detector cell has syndrome count \(1\) but time span equal to the total number of rounds (spanning the entire procedure from initialization to readout), using the inferred flux schedule.
If the total number of rounds satisfies \(\texttt{totalRounds} {\gt} 1\), then the inferred flux detector cell is large (with threshold \(1\)).
We unfold the definitions of isLarge and inferredFluxDetectorCell. The time span of the inferred flux detector cell is totalRounds, and the hypothesis gives \(\texttt{totalRounds} {\gt} 1\).
The standard detector cell is small (with threshold \(1\)).
We unfold the definitions of isSmall and standardDetectorCell. The time span is \(1 \leq 1\), which is verified by computation (decide).
If \(\texttt{totalRounds} {\gt} 1\), then the time span of the inferred flux detector cell is strictly greater than that of the standard detector cell.
We unfold both definitions. The time span of the inferred flux cell is totalRounds and the standard cell’s time span is \(1\). The result follows from the hypothesis \(\texttt{totalRounds} {\gt} 1\).
Abstract representation of whether a code has a fault-tolerance threshold. It records whether a threshold exists, its value (if any), and a confidence level.
The threshold property for standard measurement: a threshold is expected to exist.
The threshold property for inferred flux measurement: no threshold is expected without further modifications.
The standard measurement schedule has a threshold (\(\texttt{hasThreshold} = \texttt{true}\)), while the inferred flux schedule does not (\(\texttt{hasThreshold} = \texttt{false}\)).
We prove both conjuncts. Each holds by reflexivity from the respective definitions.
If \(\texttt{totalRounds} {\gt} 1\) and the threshold is \(1\), then the inferred flux detector cell is large with respect to that threshold.
We unfold the definitions of isLarge and inferredFluxDetectorCell, and substitute \(\texttt{threshold} = 1\). The time span is totalRounds, and the hypothesis gives \(\texttt{totalRounds} {\gt} 1\).
A code instance specifies the number of physical qubits \(n\), the number of logical qubits \(k\), the code distance \(d\), and the maximum check weight.
A code instance is small if its number of physical qubits is at most a given threshold.
A practical utility assessment records whether a measurement strategy is useful, for what instance sizes, its primary benefit, and its primary drawback.
The utility assessment for the inferred flux strategy: it is useful for small instances, with the benefit of avoiding high-weight \(B_p\) measurements and the drawback of no threshold and large detector cells.
For a small code instance with high-weight flux checks (\(\texttt{maxCheckWeight} {\gt} \texttt{distance}\)), the inferred flux strategy is useful and applicable to small instances.
We prove both conjuncts. Each holds by reflexivity from the definition of inferredFluxUtility.
For a small code instance with very high-weight flux checks (\(\texttt{maxCheckWeight} {\gt} 2d\)), the trade-off is favorable: the code instance remains small (the benefit of avoiding high-weight measurements outweighs the lack of threshold for small instances).
This follows directly from the hypothesis that the code is small.
The type alias for flux check weight, represented as a natural number (the number of edges in the cycle).
Information about the weight of a flux check: its numerical weight, whether it is considered high weight, and the reason.
A flux check has high weight if its weight exceeds a given threshold.
If a flux check is high weight (i.e., \(\texttt{isHighWeightFlux}(\texttt{fluxWeight}, \texttt{threshold}) = \texttt{true}\)), then the inferred measurement strategy is appealing because it avoids measuring this high-weight operator.
This follows directly from the hypothesis.
The difficulty of measuring a check operator of weight \(w\) is modeled as \(w^2\) (quadratic in weight).
The measurement difficulty is positive if and only if the flux weight is positive: \(0 {\lt} w^2 \iff w {\gt} 0\).
We unfold the definition of measurementDifficulty. We prove both directions of the biconditional.
\((\Rightarrow )\): Assume \(0 {\lt} w \cdot w\). By contradiction, suppose \(w = 0\). Then \(w \cdot w = 0\), contradicting \(0 {\lt} w \cdot w\). Hence \(w {\gt} 0\).
\((\Leftarrow )\): Assume \(w {\gt} 0\). Then \(w \cdot w {\gt} 0\) follows from Nat.mul_pos.
A summary structure capturing the complete trade-off for flux measurement frequency. It records whether \(B_p\) can be measured less often, whether it can be inferred entirely, whether fault distance scaling is preserved, whether detector cells are large, whether a threshold is expected, and whether the strategy is useful for small instances.
The complete trade-off for the inferred flux measurement strategy:
\(B_p\) can be measured less often: true,
\(B_p\) can be inferred: true,
Fault distance preserved: true,
Large detector cells: true,
Threshold expected: false,
Useful for small instances: true.
The inferred flux trade-off satisfies: \(B_p\) can be inferred, fault distance is preserved, detector cells are large, no threshold is expected, and the strategy is useful for small instances.
We unfold the definition of inferredFluxTradeoff. All five conjuncts hold by simplification, as each field matches the claimed value.
Recommendations based on the trade-off:
useStandard: Use standard measurement for threshold guarantees,
useInferred: Use inferred flux for small instances with high-weight checks,
addModifications: Add further modifications to recover a threshold.
The recommendation function: if a threshold is needed, use the standard strategy; otherwise, if the instance is small (\(n \leq 100\)), use inferred flux; otherwise, add modifications.