The cost of each side condition in a gauged logical measurement

Technical Summary: The Cost of Side Conditions in Gauged Logical Measurements

Problem Statement
Fault-tolerant quantum computation relies on logical measurements to read out protected information. The robustness of this process is quantified by two metrics: the spatial distance of the code remaining after measurement and the temporal fault distance (the minimum weight of a fault that passes undetected and flips the readout). Williamson and Yoder [5] established a fault-tolerance guarantee for "gauging," a systematic method to measure logical operators by introducing an auxiliary graph and ancilla qubits. Their guarantee rests on four side conditions (hypotheses):

1. Expansion (C1): The auxiliary graph must have an expansion of at least one.
2. Round Count (C2): The interval between code deformation steps must span at least $d$ rounds (where $d$ is the code distance).
3. Boundary Perfection (C3): The first and last rounds of the measurement must be perfect (fault-free).
4. Locality (C4): No single round may contain a local detector (a set of checks with fixed parity in the absence of faults).

While the bound consumes C1 and C2 to establish spatial and temporal components respectively, the necessity and "cost" of C3 and C4 were previously unpriced. The paper addresses whether these conditions are equally critical and whether they are necessary for the fault-distance guarantee to hold.

Methodology
The authors employ a formal verification approach using the Lean proof assistant to audit the hypotheses of the gauging theorem. Rather than relying on asymptotic bounds, they compute exact fault distances for specific instances.

• Formalization: The development formalizes the check-matrix layer of gauging, treating the operation as an algebraic transformation on CSS code check matrices.
• Exact Computation: Two specific instances are analyzed within the proof assistant's trusted core:
  1. A gauged bivariate bicycle code ($[[18, 4, 4]]$) gauged along a weight-4 logical operator using a complete graph ($K_4$) auxiliary structure.
  2. A transversal measurement on a Bacon–Shor code ($[[9, 1, 3]]$).
• Modeling Variants: The authors compare two models:
  • The measurement-fault model: Data qubits are assumed fault-free; only measurement and ancilla faults are considered.
  • The full protocol model: Includes data, ancilla, and readout faults, along with a single-round boundary detector.
• Counterexample Generation: Exhaustive enumeration is used to test the necessity of conditions (e.g., varying auxiliary graph topologies on the same code support).

Key Contributions and Results

1. The Boundary Condition (C3) is Load-Bearing:
   The paper demonstrates that C3 (perfect first and last rounds), though adopted as a convention in the source literature, is a critical structural requirement.

   • Result: If C3 is dropped, the fault distance collapses to one for every code, every round count, and every readout that can return a logical '1'.
   • Mechanism: In a model where detectors compare adjacent rounds, a single data fault placed in the first round propagates through the accumulation of errors. Because the fault exists in every subsequent round, the difference between adjacent rounds remains zero, rendering the fault invisible to all comparisons while flipping the final readout.
   • Significance: This condition is "load-bearing" despite never entering the assembled statement; it acts as a modelling switch that prevents the temporal component from collapsing.

2. The Expansion Condition (C1) Does Not Decide the Outcome:
   Contrary to the intuition that expansion guarantees distance, the authors show it is not sufficient on its own to determine the specific fault distance.

   • Result: Two different auxiliary graphs (both paths on the same four support qubits) that both violate the expansion condition yield different Z-side distances (1 and 2) for the same underlying code.
   • Mechanism: The outcome is determined by specific columns in the deformed check matrix (specifically, whether a zero column exists outside the X-row space), not solely by the global expansion property.
   • Significance: C1 is a predicate that can be evaluated, but its failure does not uniformly dictate the distance; the distance depends on the specific graph structure and matching properties.

3. The Round Count Condition (C2) is Tight in Specific Models:

   • Result: In the measurement-fault model (where data qubits are perfect), the round count condition is exactly tight. Reducing the rounds by one ($T = d-1$) admits an undetectable logical fault of weight 2 (below the code distance $d=3$).
   • Result: In the full protocol model, the distance is restored one round earlier ($T = d-1$) because data faults accumulate, making it more expensive to hide a fault across rounds.
   • Significance: The necessity of C2 depends on the fault model; it is a hard constraint for the simplified model but less restrictive for the full protocol.

4. The Locality Condition (C4) Costs Nothing:

   • Result: The presence of a local detector (a linear dependency among checks in a single round) does not reduce the code distance. Appending a dependent check leaves the kernel and row space unchanged.
   • Significance: C4 is a decidable predicate that costs the code nothing in terms of distance, though it is required for the specific detector-generating lemmas in the source literature.

Significance and Claims
The paper claims to "price" the side conditions of the gauging theorem, transforming them from abstract assumptions into computable predicates for designers.

• Design Implications: A designer can now input an auxiliary graph and a schedule into the formal system. The system will compute the exact spatial and temporal fault distances, explicitly naming which conditions fail and what the resulting distance is, rather than relying on a bound that assumes all conditions hold.
• Formal Verification: The work provides the first exact computation of both spatial and temporal components for gauged measurements inside a proof assistant, auditing the hypothesis list of the assembled statement.
• Threshold Estimates: The authors note that threshold estimates rely on fault-distance bounds. By clarifying that the boundary condition (C3) is essential and that the round count (C2) is tight only in specific models, the paper argues that estimates built on these bounds inherit specific assumptions (e.g., fault-free boundary rounds) that must be accounted for.

The paper concludes that the four conditions are not of equal weight: C3 is the most critical structural element preventing collapse, C2 is tight in the measurement-fault model, C1 is insufficient to determine the outcome alone, and C4 is cost-free. The development stops short of formalizing the detector-generating lemma itself but clarifies the role of its restrictions.