39 Rem 16: Practical Measurement Rounds
This chapter formalizes the observation that the \(d\) rounds of quantum error correction in the original code before and after the gauging measurement are required for the proof of fault tolerance but are overkill in practice. In a full fault-tolerant computation, the number of rounds required before and after a gauging measurement depends on the surrounding operations: if the gauging measurement occurs in the middle of a large computation, a constant number of rounds before and after are expected to be sufficient. However, this choice affects the effective distance and threshold depending on the surrounding operations.
39.1 Round Requirements
An inductive type classifying round requirements:
theoretical: required for the formal proof of fault tolerance,
practical: sufficient in practice.
A round requirement specifies how many error correction rounds are needed before and after gauging. It consists of:
a code distance \(d \in \mathbb {N}\) with \(d {\gt} 0\),
the number of rounds before gauging, \(r_{\mathrm{before}} \in \mathbb {N}\),
the number of rounds after gauging, \(r_{\mathrm{after}} \in \mathbb {N}\),
a requirement type (theoretical or practical).
Given a code distance \(d {\gt} 0\), the theoretical round requirement sets both \(r_{\mathrm{before}} = d\) and \(r_{\mathrm{after}} = d\), with type theoretical.
Given a code distance \(d {\gt} 0\) and chosen values \(r_{\mathrm{before}}, r_{\mathrm{after}} \in \mathbb {N}\), the practical round requirement records these values with type practical.
A round requirement uses full rounds if \(r_{\mathrm{before}} = d\) and \(r_{\mathrm{after}} = d\).
A round requirement uses fewer rounds if \(r_{\mathrm{before}} {\lt} d\) or \(r_{\mathrm{after}} {\lt} d\).
For any code distance \(d {\gt} 0\), the theoretical round requirement uses full \(d\) rounds, i.e., \(r_{\mathrm{before}} = d\) and \(r_{\mathrm{after}} = d\).
Both equalities hold by reflexivity from the definition of the theoretical round requirement.
For any code distance \(d {\gt} 0\), the theoretical round requirement has \(r_{\mathrm{before}} = d\).
This holds by reflexivity (definitional equality).
For any code distance \(d {\gt} 0\), the theoretical round requirement has \(r_{\mathrm{after}} = d\).
This holds by reflexivity (definitional equality).
39.2 Computation Context
An inductive type describing where in a computation the gauging measurement occurs:
beginning: at the start of a computation,
middle: in the middle of a large computation,
end_: at the end of a computation,
isolated: a standalone gauging measurement.
The surrounding computation context for a gauging measurement, consisting of:
the position of the gauging measurement (beginning, middle, end, or isolated),
the total number of logical operations,
a Boolean indicating whether surrounding operations provide additional error correction,
the effective number of EC rounds provided by surrounding operations.
A mid-computation context where the position is middle, surrounding EC is present, and the given number of surrounding EC rounds is recorded.
An isolated context where the position is isolated, there is one total operation, no surrounding EC is present, and zero surrounding EC rounds.
A computation context has surrounding EC if \(\mathtt{surroundingECPresent} = \mathtt{true}\) and \(\mathtt{surroundingECRounds} {\gt} 0\).
39.3 Practical Round Configuration
A configuration for practical round counts based on context, consisting of:
a code distance \(d {\gt} 0\),
a computation context,
practical rounds before and after gauging,
proofs that both practical round counts are at most \(d\).
For any practical round configuration, the practical rounds before and after gauging are each at most \(d\).
This follows directly from the fields before_le_d and after_le_d of the configuration.
A practical configuration uses fewer rounds if \(r_{\mathrm{before}} {\lt} d\) or \(r_{\mathrm{after}} {\lt} d\).
A practical configuration uses constant rounds \(c\) if \(r_{\mathrm{before}} \leq c\) and \(r_{\mathrm{after}} \leq c\).
Given a code distance \(d {\gt} 0\), a constant \(c \leq d\), and a computation context, the constant round configuration sets both practical round counts to \(c\).
If a gauging measurement occurs in the middle of a large computation with surrounding error correction, then for any constant \(c\) with \(0 {\lt} c \leq d\), the constant round configuration satisfies: it uses constant rounds \(c\), and both the practical rounds before and after are positive.
By simplification using the definitions of constantRoundConfig and usesConstantRounds, the goal reduces to showing \(c \leq c\), \(c \leq c\), \(0 {\lt} c\), and \(0 {\lt} c\). The first two hold by reflexivity of \(\leq \), and the latter two follow from the hypothesis \(0 {\lt} c\).
If \(c {\lt} d\), then the constant round configuration with constant \(c\) uses strictly fewer rounds than \(d\).
By simplification using the definitions, the goal reduces to \(c {\lt} d \lor c {\lt} d\). We take the left disjunct, which holds by hypothesis.
39.4 Effective Code Parameters
Effective code parameters under a given round configuration, consisting of:
the original code distance \(d\),
the effective distance (which may be reduced with fewer rounds),
a Boolean indicating whether a fault-tolerance threshold exists,
the round configuration used.
With full \(d\) rounds, the effective distance equals the original distance \(d\), and a threshold exists.
With fewer rounds, the effective distance may be reduced to some given value.
With full \(d\) rounds, the effective distance equals \(d\).
This holds by reflexivity (definitional equality).
If the round configuration uses fewer rounds, and the effective distance is at most the original distance, and the original distance equals \(d\), then the effective distance is at most \(d\).
This follows by integer arithmetic (omega) from the hypotheses \(d_{\mathrm{eff}} \leq d_{\mathrm{orig}}\) and \(d_{\mathrm{orig}} = d\).
With full \(d\) rounds, the effective distance equals the original distance.
This holds by reflexivity (definitional equality).
39.5 Worst-Case vs Practical Guarantees
An inductive type classifying fault-tolerance guarantees:
worstCase: holds for any surrounding computation,
contextDependent: depends on the specific context.
A fault-tolerance guarantee with its type, code distance, round counts before and after, and a Boolean indicating validity.
The worst-case guarantee with \(d\) rounds before and after, of type worstCase, marked as valid.
A context-dependent guarantee with constant \(c\) rounds before and after, of type contextDependent, marked as valid for appropriate contexts.
The theoretical requirement of \(d\) rounds serves as a worst-case guarantee: the guarantee type is worstCase, the rounds before and after are both \(d\), and the guarantee is valid.
By simplification using the definition of worstCaseGuarantee, all four conjuncts hold trivially.
If \(c {\lt} d\), then the context-dependent guarantee uses fewer rounds before gauging than the worst-case guarantee.
By simplification using the definitions, the goal reduces to \(c {\lt} d\), which holds by hypothesis.
Both the worst-case and context-dependent guarantees are valid (for their respective contexts).
By simplification using both definitions, the validity fields are both true.
39.6 Practical Implementations
A practical implementation choice for round counts, consisting of:
a code distance \(d {\gt} 0\),
the surrounding context,
chosen rounds before and after gauging, both positive and at most \(d\).
A practical implementation uses fewer rounds if \(r_{\mathrm{before}} {\lt} d\) or \(r_{\mathrm{after}} {\lt} d\).
Given two practical implementations with the same code distance but different computation contexts and different chosen rounds before gauging, their chosen rounds before gauging are indeed different.
This follows directly from the hypothesis that the chosen rounds are different.
Let \(c {\lt} d\). If a mid-computation implementation uses \(c\) rounds before gauging and an isolated implementation uses \(d\) rounds before gauging (with the same code distance), then the mid-computation implementation uses strictly fewer rounds before gauging.
Rewriting the chosen rounds using the hypotheses \(r_{\mathrm{mid}} = c\) and \(r_{\mathrm{iso}} = d\), the goal becomes \(c {\lt} d\), which holds by hypothesis.
39.7 Connection to Boundary Conditions
Converts a PracticalRoundConfig to an ErrorCorrectionRounds structure (from the boundary conditions formalization), preserving the code distance and round counts.
With full \(d\) rounds (i.e., \(c = d\)), the conversion to ErrorCorrectionRounds provides full protection.
By simplification using the definitions of constantRoundConfig, toErrorCorrectionRounds, and providesFullProtection, both conditions (\(r_{\mathrm{before}} \geq d\) and \(r_{\mathrm{after}} \geq d\)) are trivially satisfied when \(c = d\).
If \(c {\lt} d\), then the constant round configuration with \(c\) rounds does not provide full protection.
By simplification using the definitions, the negation of full protection reduces to showing that \(c \geq d\) leads to a contradiction. Assuming \(c \geq d\) and using integer arithmetic with the hypothesis \(c {\lt} d\), we obtain the desired contradiction.
39.8 Summary
A summary structure capturing all aspects of the practical measurement rounds trade-off:
the theoretical requirement (number of rounds),
whether this is a worst-case guarantee,
whether practical implementations may use fewer rounds,
whether the choice affects distance,
whether the choice is context-dependent.
The summary capturing all aspects of the remark: the theoretical requirement is \(d\) rounds, it is a worst-case guarantee, practical implementations may use fewer rounds, the choice affects distance, and the choice is context-dependent.
The summary satisfies: the theoretical requirement is \(d\), and all Boolean flags (worst-case, practical may use fewer, affects distance, context-dependent) are true.
By simplification using the definition of practicalRoundsSummary, all five conjuncts hold trivially.
For any code distance \(d {\gt} 0\) and any mid-computation context with surrounding error correction, there exists a constant \(c \leq d\) with \(c {\gt} 0\) such that the constant round configuration uses constant rounds \(c\).
We take \(c = 1\). The condition \(1 \leq d\) follows from \(d {\gt} 0\) by integer arithmetic. Positivity \(0 {\lt} 1\) holds by Nat.one_pos. The constant rounds property \(1 \leq 1 \land 1 \leq 1\) holds by reflexivity.
I’ll read the Lean file first.