28 Def 10: Fault-Tolerant Gauging Procedure
The three phases of the fault-tolerant gauging procedure form an inductive type with three constructors:
preDeformation: Phase 1, in which the original stabilizer checks are measured.
deformedCode: Phase 2, in which the deformed code checks (Gauss’s law, flux, and deformed original checks) are measured.
postDeformation: Phase 3, in which the edge qubits are ungauged and the original checks are resumed.
The type has decidable equality and is a finite type with exactly three elements.
A Phase 1 measurement label for a code with check index set \(J\) and code distance \(d\) is a pair
recording which original stabilizer check \(j \in J\) is measured in which round \(r \in \{ 0, \ldots , d-1\} \).
A Phase 2 measurement label for vertex set \(V\), cycle set \(C\), check set \(J\), and code distance \(d\) is one of:
\(\mathtt{gaussLaw}(v, r)\): Gauss’s law measurement at vertex \(v \in V\) in round \(r \in \operatorname {Fin}(d)\).
\(\mathtt{flux}(p, r)\): Flux measurement for cycle \(p \in C\) in round \(r \in \operatorname {Fin}(d)\).
\(\mathtt{deformed}(j, r)\): Deformed original check \(j \in J\) in round \(r \in \operatorname {Fin}(d)\).
A Phase 3 measurement label for check set \(J\), edge set \(E\), and code distance \(d\) is one of:
\(\mathtt{edgeZ}(e)\): The \(Z_e\) measurement on edge qubit \(e \in E\) to ungauge.
\(\mathtt{originalCheck}(j, r)\): Original check \(j \in J\) measured in round \(r \in \operatorname {Fin}(d)\).
An edge initialization label for edge set \(E\) is a structure recording a single edge \(e \in E\), representing initialization of the edge qubit in the \(|0\rangle \) state (treated as a measurement per Definition 7).
The type of all measurement labels across the entire fault-tolerant gauging procedure is the inductive type with four constructors:
\(\mathtt{phase1}(m)\): A Phase 1 measurement \(m\).
\(\mathtt{edgeInit}(\mathit{init})\): An edge initialization event.
\(\mathtt{phase2}(m)\): A Phase 2 measurement \(m\).
\(\mathtt{phase3}(m)\): A Phase 3 measurement \(m\).
Given code distance \(d\) and a time step \(t \in \mathbb {N}\), the function \(\operatorname {phaseOf}(d, t)\) determines which phase \(t\) belongs to:
If \(t {\lt} d\), then \(\operatorname {phaseOf}(d, t) = \text{preDeformation}\).
Unfolding the definition of \(\operatorname {phaseOf}\) and simplifying with the hypothesis \(t {\lt} d\) yields the result directly.
If \(d \le t\) and \(t {\lt} 2d\), then \(\operatorname {phaseOf}(d, t) = \text{deformedCode}\).
We simplify using the definition of \(\operatorname {phaseOf}\). Since \(d \le t\), we have \(\neg (t {\lt} d)\) by integer arithmetic, so the first branch is false. Since \(t {\lt} 2d\), the second branch is true, giving the result.
If \(2d \le t\), then \(\operatorname {phaseOf}(d, t) = \text{postDeformation}\).
We simplify using the definition of \(\operatorname {phaseOf}\). Since \(2d \le t\), we have \(\neg (t {\lt} d)\) and \(\neg (t {\lt} 2d)\) by integer arithmetic, so both conditional branches are false and the result is \(\text{postDeformation}\).
The fault-tolerant gauging measurement procedure for measuring a logical operator \(L\) in an \([\! [n,k,d]\! ]\) stabilizer code using a connected graph \(G = (V, E)\) with cycle set \(C\) and check set \(J\) is a structure consisting of:
\(d : \mathbb {N}\), the code distance (number of rounds per phase), with \(d \ge 1\).
A proof that the original stabilizer code checks pairwise commute: for all \(i, j \in J\), \(\operatorname {PauliCommute}(\mathit{checks}(i), \mathit{checks}(j))\).
A gauging input specifying the base vertex and connectivity data.
Deformed code data: edge-paths satisfying boundary conditions.
A cycle parity condition: for each cycle \(c \in C\) and vertex \(v \in V\), the number of edges in the cycle incident to \(v\) is even.
Phase 2 begins at time \(d\).
Phase 3 begins at time \(2d\).
The procedure ends at time \(3d\).
The duration of Phase 1 equals \(d\): \(\mathtt{phase2Start} = d\).
This holds by definition.
The duration of Phase 2 equals \(d\): \(\mathtt{phase3Start} - \mathtt{phase2Start} = d\).
Unfolding the definitions of \(\mathtt{phase3Start} = 2d\) and \(\mathtt{phase2Start} = d\), the result \(2d - d = d\) follows by integer arithmetic.
The duration of Phase 3 equals \(d\): \(\mathtt{procedureEnd} - \mathtt{phase3Start} = d\).
Unfolding the definitions of \(\mathtt{procedureEnd} = 3d\) and \(\mathtt{phase3Start} = 2d\), the result \(3d - 2d = d\) follows by integer arithmetic.
The total duration of the procedure is \(3d\): \(\mathtt{procedureEnd} = 3d\).
This holds by definition.
We have \(\mathtt{phase2Start} \le \mathtt{phase3Start}\), i.e., \(d \le 2d\).
Unfolding definitions, \(d \le 2d\) follows by integer arithmetic.
We have \(\mathtt{phase3Start} \le \mathtt{procedureEnd}\), i.e., \(2d \le 3d\).
Unfolding definitions, \(2d \le 3d\) follows by integer arithmetic.
The function \(\mathtt{measurementPhase}\) assigns a phase to each measurement label:
\(\mathtt{phase1}(\_ ) \mapsto \text{preDeformation}\),
\(\mathtt{edgeInit}(\_ ) \mapsto \text{deformedCode}\),
\(\mathtt{phase2}(\_ ) \mapsto \text{deformedCode}\),
\(\mathtt{phase3}(\_ ) \mapsto \text{postDeformation}\).
The function \(\mathtt{measurementTime}\) assigns an integer time step to each measurement label:
\(\mathtt{phase1}(\langle j, r \rangle ) \mapsto r\),
\(\mathtt{edgeInit}(\_ ) \mapsto d\),
\(\mathtt{phase2}(\mathtt{gaussLaw}\; v\; r) \mapsto d + r\); similarly for flux and deformed measurements,
\(\mathtt{phase3}(\mathtt{edgeZ}\; e) \mapsto 2d\); \(\mathtt{phase3}(\mathtt{originalCheck}\; j\; r) \mapsto 2d + r\).
For any Phase 1 measurement \(\mathit{pm}\), \(\mathtt{measurementTime}(\mathtt{phase1}(\mathit{pm})) {\lt} d\).
Unfolding the definition of \(\mathtt{measurementTime}\), this reduces to \(\mathit{pm}.\mathit{round}.\mathit{val} {\lt} d\), which holds because \(\mathit{pm}.\mathit{round}\) is an element of \(\operatorname {Fin}(d)\).
For any Phase 2 measurement \(\mathit{dm}\), \(d \le \mathtt{measurementTime}(\mathtt{phase2}(\mathit{dm}))\).
We case-split on the type of Phase 2 measurement (gaussLaw, flux, or deformed). In each case, the measurement time has the form \(d + r\) for some \(r \ge 0\), so \(d \le d + r\) follows by simplification.
For any Phase 2 measurement \(\mathit{dm}\), \(\mathtt{measurementTime}(\mathtt{phase2}(\mathit{dm})) {\lt} 2d\).
We case-split on the type of Phase 2 measurement. In each case, the measurement time is \(d + r\) where \(r {\lt} d\) (since \(r \in \operatorname {Fin}(d)\)), so \(d + r {\lt} 2d\) follows by simplification and integer arithmetic.
For any Phase 3 measurement \(\mathit{pm}\), \(2d \le \mathtt{measurementTime}(\mathtt{phase3}(\mathit{pm}))\).
We case-split on the type of Phase 3 measurement (edgeZ or originalCheck). In each case, the measurement time is \(2d + r\) for some \(r \ge 0\), so \(2d \le 2d + r\) follows by simplification.
For any Phase 3 measurement \(\mathit{pm}\), \(\mathtt{measurementTime}(\mathtt{phase3}(\mathit{pm})) {\lt} 3d\).
We case-split on the type of Phase 3 measurement. For \(\mathtt{edgeZ}(e)\), the time is \(2d\) and \(2d {\lt} 3d\) follows from \(d \ge 1\) by integer arithmetic. For \(\mathtt{originalCheck}(j, r)\), the time is \(2d + r\) where \(r {\lt} d\), so \(2d + r {\lt} 3d\) by integer arithmetic.
For any edge initialization \(\mathit{ei}\), \(\mathtt{measurementTime}(\mathtt{edgeInit}(\mathit{ei})) = d\).
Unfolding the definition of \(\mathtt{measurementTime}\), this holds by reflexivity.
For every measurement label \(m\),
We case-split on the measurement label \(m\):
Case \(m = \mathtt{phase1}(\mathit{pm})\): We simplify the measurement phase to \(\text{preDeformation}\). Since \(\mathtt{measurementTime}(\mathtt{phase1}(\mathit{pm})) {\lt} d\), we apply the lemma \(\mathtt{phaseOf\_ preDeformation}\).
Case \(m = \mathtt{edgeInit}(\mathit{ei})\): We simplify the measurement phase to \(\text{deformedCode}\). The measurement time is \(d\). We apply \(\mathtt{phaseOf\_ deformedCode}\) with \(d \le d\) (by reflexivity) and \(d {\lt} 2d\) (since \(d \ge 1\), by integer arithmetic).
Case \(m = \mathtt{phase2}(\mathit{dm})\): We simplify the measurement phase to \(\text{deformedCode}\). We apply \(\mathtt{phaseOf\_ deformedCode}\) using the bounds \(d \le \mathtt{measurementTime}\) and \(\mathtt{measurementTime} {\lt} 2d\).
Case \(m = \mathtt{phase3}(\mathit{pm})\): We simplify the measurement phase to \(\text{postDeformation}\). We apply \(\mathtt{phaseOf\_ postDeformation}\) using \(2d \le \mathtt{measurementTime}\).
The Boolean predicate \(\mathtt{isPhase1}\) returns true if and only if the measurement label is of the form \(\mathtt{phase1}(\_ )\).
The Boolean predicate \(\mathtt{isPhase2}\) returns true if and only if the measurement label is of the form \(\mathtt{phase2}(\_ )\) or \(\mathtt{edgeInit}(\_ )\).
The Boolean predicate \(\mathtt{isPhase3}\) returns true if and only if the measurement label is of the form \(\mathtt{phase3}(\_ )\).
The Pauli operator measured for a Phase 2 measurement \(\mathit{dm}\) is:
\(\mathtt{gaussLaw}(v, r) \mapsto \text{gaussLawChecks}(G, v)\),
\(\mathtt{flux}(p, r) \mapsto \text{fluxChecks}(G, \mathit{cycles}, p)\),
\(\mathtt{deformed}(j, r) \mapsto \text{deformedOriginalChecks}(G, \mathit{checks}, \mathit{deformedData}, j)\).
For every Phase 2 measurement \(\mathit{dm}\), there exists a check index \(\mathit{ci} \in \mathtt{CheckIndex}(V, C, J)\) such that
We match on \(\mathit{dm}\):
For \(\mathtt{gaussLaw}(v, \_ )\), we take \(\mathit{ci} = \mathtt{gaussLaw}(v)\) and the equality holds by reflexivity.
For \(\mathtt{flux}(p, \_ )\), we take \(\mathit{ci} = \mathtt{flux}(p)\) and the equality holds by reflexivity.
For \(\mathtt{deformed}(j, \_ )\), we take \(\mathit{ci} = \mathtt{deformed}(j)\) and the equality holds by reflexivity.
For any two Phase 2 measurements \(\mathit{dm}_1\) and \(\mathit{dm}_2\),
From the previous theorem, we obtain check indices \(\mathit{ci}_1\) and \(\mathit{ci}_2\) such that \(\mathtt{phase2Operator}(\mathit{dm}_i) = \mathtt{allChecks}(\mathit{ci}_i)\). Rewriting with these equalities, the result follows from \(\mathtt{allChecks\_ commute}\), which guarantees that all checks of the deformed code pairwise commute (using the cycle parity condition and the original checks’ commutativity).
For any Phase 2 measurement \(\mathit{dm}\),
From \(\mathtt{phase2Operator\_ is\_ allChecks}\), we obtain a check index \(\mathit{ci}\) with \(\mathtt{phase2Operator}(\mathit{dm}) = \mathtt{allChecks}(\mathit{ci})\). Rewriting, the result follows directly from \(\mathtt{allChecks\_ self\_ inverse}\).
For any \(v \in V\) and round \(r\), \(\mathtt{phase2Operator}(\mathtt{gaussLaw}(v, r)) = \text{gaussLawChecks}(G, v)\).
This holds by definition.
For any \(p \in C\) and round \(r\), \(\mathtt{phase2Operator}(\mathtt{flux}(p, r)) = \text{fluxChecks}(G, \mathit{cycles}, p)\).
This holds by definition.
For any \(j \in J\) and round \(r\), \(\mathtt{phase2Operator}(\mathtt{deformed}(j, r)) = \text{deformedOriginalChecks}(G, \mathit{checks}, \mathit{deformedData}, j)\).
This holds by definition.
The product of all Gauss’s law operators over \(V\) equals the logical operator \(L\):
Simplifying \(\mathtt{phase2Operator}\) on Gauss’s law measurements reduces each factor to \(\text{gaussLawChecks}(G, v)\). The result then follows directly from \(\mathtt{gaussLaw\_ product}\), which establishes that the product of all Gauss’s law operators is the logical operator.
For consecutive Phase 1 rounds \(r\) and \(r'\) (with \(r + 1 = r'\)), the repeated measurement detector for check \(j\) compares the outcomes of measuring check \(j\) in rounds \(r\) and \(r'\). It consists of the measurement set \(\{ \mathtt{phase1}(\langle j, r \rangle ), \mathtt{phase1}(\langle j, r' \rangle )\} \) with ideal outcome \(0\) for all measurements.
For consecutive Phase 2 rounds \(r\) and \(r'\), the repeated measurement detector for Gauss’s law at vertex \(v\) compares the outcomes of \(\mathtt{gaussLaw}(v, r)\) and \(\mathtt{gaussLaw}(v, r')\) with ideal outcome \(0\).
For consecutive Phase 2 rounds \(r\) and \(r'\), the repeated measurement detector for flux at cycle \(p\) compares the outcomes of \(\mathtt{flux}(p, r)\) and \(\mathtt{flux}(p, r')\) with ideal outcome \(0\).
For consecutive Phase 2 rounds \(r\) and \(r'\), the repeated measurement detector for deformed check \(j\) compares the outcomes of \(\mathtt{deformed}(j, r)\) and \(\mathtt{deformed}(j, r')\) with ideal outcome \(0\).
The edge initialization detector for edge \(e\) compares the initialization event \(\mathtt{edgeInit}(\langle e \rangle )\) with the Phase 3 measurement \(\mathtt{phase3}(\mathtt{edgeZ}(e))\), with ideal outcome \(0\).
The boundary detector from Phase 1 to Phase 2 for check \(j\) compares the last Phase 1 round measurement \(\mathtt{phase1}(\langle j, r_{\text{last}} \rangle )\) with the first Phase 2 deformed check measurement \(\mathtt{phase2}(\mathtt{deformed}(j, r_{\text{first}}))\), where \(r_{\text{last}} + 1 = d\) and \(r_{\text{first}} = 0\), with ideal outcome \(0\).
The boundary detector from Phase 2 to Phase 3 for check \(j\) compares the last Phase 2 deformed check measurement \(\mathtt{phase2}(\mathtt{deformed}(j, r_{\text{last}}))\) with the first Phase 3 original check measurement \(\mathtt{phase3}(\mathtt{originalCheck}(j, r_{\text{first}}))\), where \(r_{\text{last}} + 1 = d\) and \(r_{\text{first}} = 0\), with ideal outcome \(0\).
Phase 1 has \(|J| \cdot d\) measurements:
We establish a bijection between \(\text{PreDeformationMeasurement}(J, d)\) and \(J \times \operatorname {Fin}(d)\) via the maps \(\langle j, r \rangle \mapsto (j, r)\) and \((j, r) \mapsto \langle j, r \rangle \), both of which are inverses by reflexivity. We then rewrite using the cardinality of a product type: \(|J \times \operatorname {Fin}(d)| = |J| \cdot |\operatorname {Fin}(d)| = |J| \cdot d\).
Phase 2 has \((|V| + |C| + |J|) \cdot d\) measurements:
We establish a bijection between \(\text{DeformedCodeMeasurement}(V, C, J, d)\) and \((V \times \operatorname {Fin}(d)) \oplus (C \times \operatorname {Fin}(d)) \oplus (J \times \operatorname {Fin}(d))\) by mapping each constructor to the corresponding summand and verifying the two maps are inverses (by case analysis, each case holds by reflexivity). We then compute the cardinality using the sum and product type formulas and ring arithmetic to obtain \((|V| + |C| + |J|) \cdot d\).
The number of edge initializations equals the number of edges: \(|\text{EdgeInitialization}(E)| = |E|\).
We establish a bijection between \(\text{EdgeInitialization}(E)\) and \(E\) via \(\langle e \rangle \mapsto e\) and \(e \mapsto \langle e \rangle \), which are inverses by reflexivity.
The gauging measurement sign from Phase 2 Gauss outcomes is
For any Gauss outcomes, \(\mathtt{gaugingSign}(\mathit{gaussOutcomes}) = 0\) or \(\mathtt{gaugingSign}(\mathit{gaussOutcomes}) = 1\).
Every element of \(\mathbb {Z}/2\mathbb {Z}\) is either \(0\) or \(1\), as verified by case analysis on the finite type.
For any Gauss outcomes and edge outcomes,
Simplifying the definitions of \(\mathtt{gaugingSign}\) and \(\mathtt{measurementSign}\), both reduce to \(\sum _{v \in V} \mathit{gaussOutcomes}(v)\).
For any vertex \(v \in V\) and round \(r\), the Phase 2 Gauss’s law operator has zero \(Z\)-component:
This follows directly from \(\mathtt{gaussLawOp\_ zVec}\), which establishes that Gauss’s law operators are pure \(X\)-type.
For any cycle \(p \in C\) and round \(r\), the Phase 2 flux operator has zero \(X\)-component:
This follows directly from \(\mathtt{fluxOp\_ xVec}\), which establishes that flux operators are pure \(Z\)-type.
For any check \(j \in J\), round \(r\), and edge \(e \in E(G)\), the Phase 2 deformed check operator has zero \(X\)-component on edge qubit \(e\):
This follows directly from \(\mathtt{deformedOpExt\_ xVec\_ edge}\), which establishes that the deformed extension of an operator has no \(X\)-support on edge qubits.