Dependencies

Under the hypotheses of the Fault Tolerance Theorem, for any spacetime fault \(F\) with \(\mathrm{weight}(F) {\lt} d\):

That is, \(F\) either triggers a detector (is detectable) or does not affect logical information (is a stabilizer).

Under the hypotheses of the Fault Tolerance Theorem, for any \(t \in \mathbb {N}\) with \(2t + 1 \leq d\), the code can tolerate \(t\) faults:

In particular, the code can correct up to \(\lfloor (d-1)/2\rfloor \) faults.

Under the hypotheses of the Fault Tolerance Theorem,

When \(h(G) \ge 1\) (strong expander), \(d^* \ge d\).

Under the same conditions, if a spacetime fault \(F\) has \(|F| {\lt} d\), then either \(F\) does not have empty syndrome (it is detectable) or \(F\) does not affect the logical information (it is a stabilizer).

Under the same conditions, the code can tolerate up to \(t\) faults provided \(2t + 1 \leq d\). That is, \(\mathrm{canTolerateFaults}(\ldots , t)\) holds for any \(t\) with \(2t + 1 \leq d\).

Under the same conditions as the main theorem, \(d_{\mathrm{ST}} {\gt} 0\).

For any fault pattern \(p\) with empty syndrome and preserving logical information, there exists a list of generators \(\mathrm{gens}\) such that:

1. every generator in \(\mathrm{gens}\) has empty syndrome,

2. every generator in \(\mathrm{gens}\) preserves logical information, and

3. the \(\mathbb {Z}_2\)-sum of their logical effects is \(0\).

If \(\mathrm{intervalRounds}(I) \subseteq \mathrm{times}\), then:

An abstract predicate capturing whether a fault affects the logical information. Given a logical effect predicate \(\ell : \mathrm{SpacetimeFault} \to \mathrm{Prop}\) and a fault \(f\):

This captures changes to the gauging measurement outcome or introduction of logical Pauli errors.

The set of all half-integer times between integer times \(t_1\) and \(t_2\):

Given base measurement outcomes and a spacetime fault \(f\), the faulted outcomes are defined by:

Time-faults flip the corresponding measurement outcomes.

Given base measurement outcomes and a spacetime fault, the faulted outcomes are obtained by flipping the classical measurement outcome at each location where a time-fault is active:

A binary vector over an index set \(\alpha \) is a function \(\alpha \to \mathbb {Z}/2\mathbb {Z}\). This is the type of characteristic vectors.

Addition of binary vectors \(v, w : \alpha \to \mathbb {Z}/2\mathbb {Z}\) is defined componentwise:

The all-ones vector is the binary vector that is \(1\) at every coordinate:

The zero vector is the binary vector that is \(0\) at every coordinate:

A Bivariate Bicycle (BB) code with parameters \(\ell , m\) is specified by two polynomials \(A, B \in \mathbb {F}_2[M]\). The structure consists of:

• \(\mathrm{polyA} : \mathbb {F}_2[M]\) — the first polynomial \(A\),

• \(\mathrm{polyB} : \mathbb {F}_2[M]\) — the second polynomial \(B\).

The CSS orthogonality condition states that

over \(\mathbb {F}_2\). This ensures that the X and Z stabilizers commute, which is necessary for the code to be a valid CSS code.

The matrix representation of polynomial \(A\), defined as \(\mathrm{toMatrix}(A)\), where the \((\alpha , \beta )\)-entry is \(A(\alpha - \beta )\).

The matrix representation of \(A^\top = A(x^{-1}, y^{-1})\), defined as \(\mathrm{toMatrix}(\mathrm{transposeAlg}(A))\).

The matrix representation of polynomial \(B\), defined as \(\mathrm{toMatrix}(B)\), where the \((\alpha , \beta )\)-entry is \(B(\alpha - \beta )\).

The matrix representation of \(B^\top = B(x^{-1}, y^{-1})\), defined as \(\mathrm{toMatrix}(\mathrm{transposeAlg}(B))\).

The number of left qubits is \(\ell m\).

The number of physical qubits is \(n = 2\ell m\).

The number of right qubits is \(\ell m\).

The number of X-type stabilizer checks is \(\ell m\).

The number of Z-type stabilizer checks is \(\ell m\).

The X parity check matrix is

an \(\ell m \times 2\ell m\) matrix over \(\mathbb {F}_2\) with rows indexed by \(M\) (X checks) and columns indexed by \(M \oplus M\) (left \(\oplus \) right qubits), formed by horizontally concatenating the matrix representations of \(A\) and \(B\).

The Z parity check matrix is

an \(\ell m \times 2\ell m\) matrix over \(\mathbb {F}_2\) with rows indexed by \(M\) (Z checks) and columns indexed by \(M \oplus M\) (left \(\oplus \) right qubits), formed by horizontally concatenating the matrix representations of \(B^\top \) and \(A^\top \).

An X-type Pauli operator \(X(p, q)\) is specified by two polynomials:

• \(\mathrm{leftPoly} \in \mathbb {F}_2[M]\): the pattern on left qubits,

• \(\mathrm{rightPoly} \in \mathbb {F}_2[M]\): the pattern on right qubits.

The support of a Pauli operator \(X(p, q)\) as a binary vector over \(M \oplus M\) (left \(\oplus \) right qubits) is defined as:

A Z-type Pauli operator \(Z(p, q)\) is specified by two polynomials:

• \(\mathrm{leftPoly} \in \mathbb {F}_2[M]\): the pattern on left qubits,

• \(\mathrm{rightPoly} \in \mathbb {F}_2[M]\): the pattern on right qubits.

The support of a Pauli operator \(Z(p, q)\) as a binary vector over \(M \oplus M\) (left \(\oplus \) right qubits) is defined as:

The cyclic permutation on \(\mathbb {Z}/r\mathbb {Z}\) is the bijection \(i \mapsto i + 1\) with inverse \(i \mapsto i - 1\).

The generator \(x = C_\ell \otimes I_m\) as an element of the group algebra is defined as the single monomial supported at \((1, 0) \in M\) with coefficient \(1\):

The generator \(y = I_\ell \otimes C_m\) as an element of the group algebra is defined as the single monomial supported at \((0, 1) \in M\) with coefficient \(1\):

The group algebra \(\mathbb {F}_2[x, y]/(x^\ell - 1, y^m - 1)\) is defined as

i.e., the set of finitely-supported functions \(M \to \mathbb {F}_2\) with convolution multiplication.

A labeled element is a pair \((\alpha , T)\) where \(\alpha \in M\) is a monomial and \(T \in \{ X, Z, L, R\} \) is a label type. X checks, Z checks, left qubits, and right qubits are each in one-to-one correspondence with elements of \(M\).

The four label types for checks and qubits of a BB code are:

• \(X\): X-type check

• \(Z\): Z-type check

• \(L\): Left qubit

• \(R\): Right qubit

The monomial set is defined as

This is an additive abelian group where addition represents multiplication of monomials.

A monomial \(x^a y^b\) is represented as the group algebra element \(\delta _{(a,b)} \in \mathbb {F}_2[M]\), i.e., the finitely-supported function that is \(1\) at \((a,b)\) and \(0\) elsewhere.

The generator \(x\) as a permutation on \(M = \mathbb {Z}/\ell \mathbb {Z} \times \mathbb {Z}/m\mathbb {Z}\) is defined by \((a, b) \mapsto (a + 1, b)\), with inverse \((a, b) \mapsto (a - 1, b)\).

The generator \(y\) as a permutation on \(M = \mathbb {Z}/\ell \mathbb {Z} \times \mathbb {Z}/m\mathbb {Z}\) is defined by \((a, b) \mapsto (a, b + 1)\), with inverse \((a, b) \mapsto (a, b - 1)\).

The matrix representation of a group algebra element \(p \in \mathbb {F}_2[M]\) is the \(|M| \times |M|\) matrix over \(\mathbb {F}_2\) whose \((\alpha , \beta )\)-entry is \(p(\alpha - \beta )\):

This gives a circulant-like structure on the product group.

The transpose of a group algebra element \(p \in \mathbb {F}_2[M]\) is defined as \(p^\top = p(x^{-1}, y^{-1})\), computed by applying the monomial transpose to the domain:

This maps each monomial \((a, b)\) to \((-a, -b)\) while preserving coefficients.

The transpose operation on monomials maps \((a, b) \mapsto (-a, -b)\) in \(M\). This corresponds to the substitution \(x \mapsto x^{-1}\), \(y \mapsto y^{-1}\).

A structure capturing the full boundary condition convention:

• a perfect boundary assumption,

• an error correction configuration,

• a proof that the configuration provides full protection,

• a flag indicating this is a simplification (default: true).

The theoretical convention can be replaced by realistic conditions: given a boundary condition convention and a realistic boundary context, the realistic context is returned unchanged (since in practice, the surrounding computation determines the conditions).

An inductive type describing the quality of measurements at the boundary:

• perfect: idealized, error-free measurements,

• realistic: measurements subject to noise and errors.

An inductive type representing the boundary of the gauging procedure, with two constructors:

• initial: the initial round of stabilizer measurements,

• final: the final round of stabilizer measurements.

A set of logical operators \(\mathcal{L}\) satisfies the bounded overlap condition with bound \(k\) if for every qubit \(i\), the overlap degree is at most \(k\):

This condition is required to maintain the LDPC property during code deformation.

A code can tolerate weight-\(t\) faults if \(t {\lt} d_{\mathrm{ST}}\):

The characteristic vector of a finset \(S \subseteq \alpha \) is the binary vector \(\chi _S : \alpha \to \mathbb {Z}/2\mathbb {Z}\) defined by

The characteristic vector map as a type equivalence \(\mathrm{Finset}(\alpha ) \simeq \mathrm{BinaryVector}(\alpha )\), with forward map \(\chi \) and inverse map \(\mathrm{fromBinaryVector}\). Theleft and right inverses are given by the two round-trip properties.

The characteristic vector map is a linear equivalence

with forward map \(\chi = \mathrm{characteristicVector}\), inverse map \(\mathrm{fromBinaryVector}\), additivity \(\chi (S + T) = \chi (S) + \chi (T)\), and scalar compatibility \(\chi (c \cdot S) = c \cdot \chi (S)\).

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).

The Cheeger constant of a simple graph \(G = (V, E)\) is defined as

where \(\partial S\) is the edge boundary of \(S\). The infimum is taken over all nonempty subsets \(S\) of \(V\) satisfying \(2|S| \leq |V|\).

A Cheeger regime classifies the Cheeger constant \(h(G)\) into one of three cases:

• Optimal: \(h(G) = 1\),

• Above one: \(h(G) {\gt} 1\),

• Below one: \(0 {\lt} h(G) {\lt} 1\).

The circuit phases of the gauging circuit are defined as the inductive type with five constructors:

1. InitializeEdges: Initialize edge qubits in \(\ket {0}\).

2. FirstEntangling: Apply the first entangling circuit \(\prod _v \prod _{e \ni v} \mathrm{CX}_{v \to e}\).

3. MeasureXVertices: Measure \(X_v\) on all vertices.

4. SecondEntangling: Apply the second entangling circuit (identical to the first).

5. MeasureZEdges: Measure \(Z_e\) on all edges and discard.

The natural ordering of circuit phases is given by the function \(\mathrm{toNat} : \mathrm{CircuitPhase} \to \mathbb {N}\) defined by:

The circuit sequence is the ordered list of circuit phases:

The cleaned operator \(\bar{L}\) obtained from \(L\) by multiplying by \(\prod _{v \in S} A_v\) is defined by:

where \(\triangle \) denotes the symmetric difference.

The cleaned-to-original operator extracts the vertex restriction of the cleaned operator as an original code operator:

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.

The Cohen overhead as a function of \(W\):

The Cohen et al. overhead for measuring a weight-\(W\) logical operator with code distance \(d\):

The all-layers logical vector is the all-ones vector on the full layered vertex set:

This represents the full product of \(L\) across all layers.

The base layer vertices are the vertices \((l, i)\) with \(l = 0\):

These correspond to the original qubits in \(\mathrm{supp}(L)\).

The base logical vector is all-ones on the base layer and zeros elsewhere:

A bridge edge configuration consists of:

• A finset of bridge connections \(\mathrm{bridges} \subseteq \mathrm{Fin}(W_1) \times \mathrm{Fin}(W_2)\), specifying which pairs of vertices to connect between the two systems.

• A proof that at least one bridge edge exists (\(\mathrm{bridges}\) is nonempty).

The Cohen hypergraph \(\mathrm{CohenHypergraph}(W, \mathrm{numChecks})\) is a hypergraph with vertex set \(\mathrm{Fin}(W)\) and hyperedge set \(\mathrm{Fin}(\mathrm{numChecks})\). The vertices represent the \(W\) qubits in \(\mathrm{supp}(L)\), and the hyperedges are the restricted Z-type checks.

The Cohen kernel property for a Cohen hypergraph \(HG\) states that the operator kernel of \(HG\) is exactly \(\{ 0, L\} \):

This is the defining property of the Cohen scheme: the restriction of Z-type checks to \(\mathrm{supp}(L)\) has kernel spanned by the logical operator \(L\) (i.e., \(L\) is irreducible).

The Cross et al. construction with \(m {\lt} d\) layers is defined as \(\mathrm{LayeredCohenConstruction}(W, m, \mathrm{numChecks}, HG)\), i.e., the same layered construction but with parameter \(m\) instead of \(d\).

The Cross et al. vertex type uses \(m\) layers (where \(m {\lt} d\)) instead of \(d\): the vertex set is \(\mathrm{Fin}(m+1) \times \mathrm{Fin}(W)\).

The dummy layer vertices are the vertices \((l, i)\) with \(l \neq 0\):

The layered Cohen construction builds a hypergraph from the original Cohen hypergraph \(HG\). The incidence function is defined by:

• For a chain edge \(\mathrm{chain}(l, i)\): the incidence set is \(\{ (l, i),\, (l+1, i)\} \).

• For a hypergraph copy \(\mathrm{hypergraphCopy}(\ell , c)\): the incidence set is the image of \(HG\)’s incidence of check \(c\) under the embedding \(v \mapsto (\ell , v)\).

The layered hyperedge type combines two kinds of edges:

• Chain edge \(\mathrm{chain}(l, i)\): connects vertex \((l, i)\) to \((l+1, i)\) for \(l \in \mathrm{Fin}(d)\) and \(i \in \mathrm{Fin}(W)\).

• Hypergraph copy \(\mathrm{hypergraphCopy}(\ell , c)\): a copy of check \(c\) in layer \(\ell \), for \(\ell \in \mathrm{Fin}(d+1)\) and \(c \in \mathrm{Fin}(\mathrm{numChecks})\).

The logical vector \(\mathbf{L} \in (\mathrm{Fin}(W) \to \mathbb {Z}/2\mathbb {Z})\) is the all-ones vector, defined by \(\mathbf{L}(v) = 1\) for all \(v\). This represents the logical operator \(L = \prod _{v \in \mathrm{supp}(L)} X_v\).

The product hyperedge type has three constructors:

• \(\mathrm{left}(h)\): a check from the first ancilla system, indexed by \(h \in \mathrm{Fin}(nc_1)\).

• \(\mathrm{right}(h)\): a check from the second ancilla system, indexed by \(h \in \mathrm{Fin}(nc_2)\).

• \(\mathrm{bridge}(i, j)\): a bridge edge connecting vertex \(i \in \mathrm{Fin}(W_1)\) to vertex \(j \in \mathrm{Fin}(W_2)\).

The product logical vector is the all-ones vector on the combined vertex set \(\mathrm{Fin}(W_1) \oplus \mathrm{Fin}(W_2)\):

The product measurement hypergraph combines two hypergraphs \(HG_1\) and \(HG_2\) with bridge edges. Its incidence function is:

• For \(\mathrm{left}(h)\): the image of \(HG_1.\mathrm{incidence}(h)\) under \(\mathrm{inl}\).

• For \(\mathrm{right}(h)\): the image of \(HG_2.\mathrm{incidence}(h)\) under \(\mathrm{inr}\).

• For \(\mathrm{bridge}(i, j)\): the set \(\{ \mathrm{inl}(i), \mathrm{inr}(j)\} \).

The product vertex type for combining two ancilla systems is the disjoint union \(\mathrm{Fin}(W_1) \oplus \mathrm{Fin}(W_2)\).

Let \(C\) be a stabilizer code. A finite set of logical operators \(\mathcal{L} \subseteq \mathrm{LogicalOp}(C)\) satisfies the commutativity condition if every pair of operators in \(\mathcal{L}\) is Pauli-compatible:

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 computation context has surrounding EC if \(\mathtt{surroundingECPresent} = \mathtt{true}\) and \(\mathtt{surroundingECRounds} {\gt} 0\).

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.

The syndrome of a spacetime fault \(f\) with respect to a detector collection \(\mathrm{DC}\) and base outcomes is the set of detectors violated by \(f\):

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\).

A context-dependent guarantee with constant \(c\) rounds before and after, of type contextDependent, marked as valid for appropriate contexts.

A CSS code (Calderbank–Shor–Steane code) is a structure consisting of:

• A positive integer \(n\) (the number of physical qubits), with \(n {\gt} 0\).

• A number \(n_X\) of \(X\)-type check generators and \(n_Z\) of \(Z\)-type check generators.

• For each \(i \in \mathrm{Fin}(n_X)\), a nonempty support set \(\mathrm{xCheckSupport}(i) \subseteq \mathrm{Fin}(n)\) indicating the qubits on which \(X\) acts.

• For each \(j \in \mathrm{Fin}(n_Z)\), a nonempty support set \(\mathrm{zCheckSupport}(j) \subseteq \mathrm{Fin}(n)\) indicating the qubits on which \(Z\) acts.

• The CSS orthogonality condition: for all \(i \in \mathrm{Fin}(n_X)\) and \(j \in \mathrm{Fin}(n_Z)\),

  \[ |\mathrm{xCheckSupport}(i) \cap \mathrm{zCheckSupport}(j)| \equiv 0 \pmod{2}. \]

The initialization hypergraph of a CSS code \(C\) is the hypergraph with vertex set \(\mathrm{Fin}(n)\) (physical qubits) and hyperedge set \(\mathrm{Fin}(n_Z)\) (one hyperedge per \(Z\)-type check), where the incidence function maps each \(Z\)-check index \(j\) to the support \(\mathrm{zCheckSupport}(j)\).

The \(i\)-th \(X\)-check vector of a CSS code \(C\) is the binary vector \(\mathbf{x}_i \in (\mathbb {Z}/2\mathbb {Z})^n\) defined by

The weight of the \(i\)-th \(X\)-type check of a CSS code \(C\) is \(|\mathrm{xCheckSupport}(i)|\).

The weight of the \(j\)-th \(Z\)-type check of a CSS code \(C\) is \(|\mathrm{zCheckSupport}(j)|\).

The CSS initialization vertex type for a CSS code \(C\) is the disjoint union of physical qubits and dummy vertices:

where:

• \(\mathrm{qubit}(i)\) for \(i \in \mathrm{Fin}(n)\) represents physical qubit \(i\),

• \(\mathrm{dummy}(j)\) for \(j \in \mathrm{Fin}(n_X)\) represents the dummy vertex for the \(j\)-th \(X\)-check.

A predicate on initialization vertices that returns \(\mathrm{true}\) for dummy vertices and \(\mathrm{false}\) for qubit vertices.

The pairwise \(XX\) operator support for qubit index \(i \in \mathrm{Fin}(n)\) is the function \(\mathrm{SteaneVertex}(n) \to \mathbb {Z}/2\mathbb {Z}\) given by:

This represents the \(X_i^{\mathrm{data}} \otimes X_i^{\mathrm{ancilla}}\) operator acting on matching qubit pairs.

The readout support function assigns \(1 \in \mathbb {Z}/2\mathbb {Z}\) to ancilla vertices and \(0\) to data vertices:

This represents the fact that the readout step measures \(Z\) on ancilla qubits only.

The Steane gauging steps are the three phases of Steane-style measurement via gauging:

1. State preparation: Initialize ancilla code block via CSS gauging.

2. Entangling measurement: Pairwise \(XX\) gauging between data and ancilla blocks.

3. Readout: \(Z\) measurement on ancilla qubits (ungauging).

The Steane gauging hypergraph for \(n\) qubits is the hypergraph with vertex set \(\mathrm{SteaneVertex}(n)\) and hyperedge set \(\mathrm{Fin}(n)\), where each hyperedge \(i\) consists of the pair \(\{ \mathrm{data}(i), \mathrm{ancilla}(i)\} \).

The Steane vertex type for \(n\) qubits is the disjoint union of a data block and an ancilla block:

where \(\mathrm{data}(i)\) represents qubit \(i\) in the data block and \(\mathrm{ancilla}(i)\) represents qubit \(i\) in the ancilla block.

A controlled-\(X\) gate specification for a qubit type \(Q\) consists of:

• a control qubit \(c \in Q\),

• a target qubit \(t \in Q\),

• a proof that \(c \neq t\).

The cycle degree of an edge \(e\) with respect to a set of cycles \(C\) (each given as a finset of edges) is the number of cycles in the generating set that contain \(e\):

A cycle-layer assignment for a set of cycles \(C\) and \(R+1\) layers assigns each cycle to exactly one layer. Formally, it is a function \(\mathrm{assign} : C \to \mathrm{Fin}(R+1)\).

The set of cycles assigned to a particular layer \(\ell \) is:

A cycle-sparsification of a graph \(G\) with cycles \(C\) is a structure consisting of:

• a base graph \(G\) with its chosen generating set of cycles (of type \(\mathrm{GraphWithCycles}\; V\; E\; C\)),

• a number of additional layers \(R\) (total layers \(= R + 1\)),

• a cycle-degree bound \(c \in \mathbb {N}\),

• a cycle-layer assignment \(\mathrm{cycleAssignment} : C \to \mathrm{Fin}(R+1)\),

• for each cycle, a list of vertices representing the cycle in order,

• the cycle-degree constraint: for every edge \(e \in E\), \(\mathrm{cycleDegree}(\mathrm{cycles}, e) \leq c\).

The dummy layers of the sparsified graph consist of all layered vertices with nonzero layer index:

The embedding \(V \hookrightarrow \mathrm{SparsifiedVertex}(S)\) that sends each vertex \(v\) to its layer-\(0\) copy \(\mathrm{ofOriginal}(v)\). This is injective: if \(\mathrm{ofOriginal}(v) = \mathrm{ofOriginal}(w)\), then \(v = w\) by the second component of the equality.

An inter-layer edge connects a vertex to its copy in an adjacent layer. Formally, \((\ell v_1, \ell v_2)\) is an inter-layer edge if:

An intra-layer edge in the sparsified graph connects two vertices in the same layer that are adjacent in the original graph. Formally, \((\ell v_1, \ell v_2)\) is an intra-layer edge if:

A triangulation edge \((\ell v_1, \ell v_2)\) is an edge added to cellulate a cycle. Formally:

The set of vertices in layer \(i\) of the sparsified graph:

The original layer (layer \(0\)) of the sparsified graph is the set of all layered vertices with layer index \(0\):

The adjacency relation in the sparsified graph is defined as: two layered vertices \(\ell v_1, \ell v_2\) are adjacent if \(\ell v_1 \neq \ell v_2\) and at least one of the following holds:

1. \((\ell v_1, \ell v_2)\) is an intra-layer edge,

2. \((\ell v_1, \ell v_2)\) is an inter-layer edge,

3. \((\ell v_1, \ell v_2)\) is a triangulation edge.

The vertex type of the sparsified graph is \(\mathrm{LayeredVertex}\; V\; S.\mathrm{numLayers}\), i.e., pairs of (layer index, original vertex).

The cycle-sparsified graph as a \(\mathrm{SimpleGraph}\) on the sparsified vertex type, with adjacency given by \(\mathrm{sparsifiedAdj}\), symmetry from the symmetry theorem, and irreflexivity from the irreflexivity theorem.

The set of triangulation edge pairs for a cycle \(c\) in layer \(\ell \) is:

• If the cycle \(c\) is assigned to layer \(\ell \): the image of \(\mathrm{triangulationEdgePairs}(\mathrm{cycleVertices}(c))\) under the embedding into layer \(\ell \).

• Otherwise: the empty list.

The deformed code distance is

A logical operator of the deformed code extends a deformed Pauli operator with:

1. Nontrivial: \(L\) is not the identity.

2. Cocycle: \(S_X^E\) is a \(1\)-cocycle (commutes with all flux operators \(B_p\)).

3. Cleaned vertex nontrivial: for any \(S\) with \(S_X^E = \partial S\), the cleaned vertex restriction \(\bar{L}|_V\) is nontrivial. This follows from \(L'\) being a logical (not a stabilizer): if \(\bar{L}|_V\) were trivial, then \(\bar{L}\) would be pure edge \(Z\)-support, hence a stabilizer, contradicting that \(L'\) is a logical.

4. Cleaned is original logical: for any \(S\) with \(S_X^E = \partial S\), the cleaned vertex restriction is a logical of the original code.

A Pauli operator on the deformed system (vertices \(+\) edges) is a structure

where \(S_X^V, S_Z^V \subseteq V\) are the \(X\)- and \(Z\)-supports on vertex qubits, \(S_X^E, S_Z^E \subseteq E\) are the \(X\)- and \(Z\)-supports on edge qubits, and \(\phi \in \mathbb {Z}/4\mathbb {Z}\) is a phase.

A deformed Pauli operator \(L\) is nontrivial if at least one of the four support sets is nonempty, i.e.,

The total weight of a deformed Pauli operator \(L\) is

The vertex weight of a deformed Pauli operator \(L\) is

A detector for types \(V\), \(E\), \(M\) (with decidable equality) is a structure consisting of:

• \(\mathrm{events} : \mathrm{Finset}(\mathrm{DetectorEvent}(V, E, M))\) — the set of events in the detector,

• \(\mathrm{expectedParity} \in \mathbb {Z}/2\mathbb {Z}\) — the expected parity in fault-free execution (\(0\) for \(+1\), \(1\) for \(-1\)).

Given an outcome assignment and a time fault \(f\), the faulted outcomes are:

The combination of two detectors \(D_1\) and \(D_2\) is defined by taking the symmetric difference of their event sets and the XOR (sum mod \(2\)) of their expected parities:

This corresponds to multiplying the parity checks.

The empty detector has \(\mathrm{events} = \emptyset \) and \(\mathrm{expectedParity} = 0\).

The fault-free outcomes given expected measurement outcomes is simply the identity function on the expected outcomes: \(\mathrm{faultFreeOutcomes}(f) := f\).

The fault syndrome of a detector \(D\) with respect to a set of faulted measurements is:

The set of all initialization events in a detector \(D\), obtained by filtering \(D.\mathrm{events}\) through \(\mathrm{getInit}\).

The contribution from initialization events:

A detector \(D\) is satisfied by outcomes if \(\mathrm{observedParity}(D, \mathrm{outcomes}) = D.\mathrm{expectedParity}\).

A detector \(D\) is violated by outcomes if \(\mathrm{observedParity}(D, \mathrm{outcomes}) \neq D.\mathrm{expectedParity}\).

The set of all measurement events in a detector \(D\), obtained by filtering \(D.\mathrm{events}\) through \(\mathrm{getMeas}\).

The observed parity given an outcome assignment:

A detector consisting of a single initialization event \(e\), with \(\mathrm{events} = \{ \ \mathrm{init}(e)\ \} \) and \(\mathrm{expectedParity} = e.\mathrm{expectedParity}\).

A detector consisting of a single measurement event \(e\) with expected outcome \(p\), with \(\mathrm{events} = \{ \ \mathrm{meas}(e)\ \} \) and \(\mathrm{expectedParity} = p\).

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.

A detector collection is a finite set of detectors:

All detectors are satisfied if the syndrome is empty:

The syndrome of a detector collection given outcomes is the set of violated detectors:

The count of violated detectors: \(\mathrm{violatedCount}(DC, \mathrm{outcomes}) := |\mathrm{syndrome}(DC, \mathrm{outcomes})|\).

A detector event is an element of the inductive type with two constructors:

• \(\mathrm{init}(e)\): an initialization event \(e\),

• \(\mathrm{meas}(e)\): a measurement event \(e\).

Returns \(\mathrm{some}(e)\) if the detector event is \(\mathrm{init}(e)\), and \(\mathrm{none}\) if it is a measurement event.

Returns \(\mathrm{some}(e)\) if the detector event is \(\mathrm{meas}(e)\), and \(\mathrm{none}\) if it is an initialization event.

Checks whether a detector event is an initialization event. Returns \(\mathrm{true}\) for \(\mathrm{init}\) and \(\mathrm{false}\) for \(\mathrm{meas}\).

Checks whether a detector event is a measurement event. Returns \(\mathrm{false}\) for \(\mathrm{init}\) and \(\mathrm{true}\) for \(\mathrm{meas}\).

Extracts the time step of a detector event: for \(\mathrm{init}(e)\) it returns \(e.\mathrm{time}\), and for \(\mathrm{meas}(e)\) it returns \(e.\mathrm{time}\).

A structure capturing the deterministic outcome property of measuring \(X\) on \(\ket {+}\). It consists of:

• A state \(\mathrm{is\_ plus\_ state}\) of type \(\mathrm{InitialState}\),

• A proof that \(\mathrm{is\_ plus\_ state} = \mathrm{plus}\),

• An outcome of type \(\mathrm{GraphMeasurementOutcome}\),

• A proof that \(\mathrm{outcome} = \mathrm{plus}\).

Two logical operators \(L_1\) and \(L_2\) have disjoint support if their operator supports are disjoint:

The set of dummy vertices in the subdivided graph is \(\mathrm{dummyVerticesOfSubdivision}'(G) := \{ \mathrm{inr}(e) \mid e \in E(G)\} \subseteq \texttt{SubdividedVertex'}(V, \mathrm{Sym2}(V))\), defined as the image of \(G.\mathrm{edgeFinset}\) under \(\mathrm{inr}\).

The edge boundary \(\partial S\) of a vertex set \(S\) in a simple graph \(G = (V, E)\) is the set of edges with exactly one endpoint in \(S\):

Formally, \(\partial S\) is computed by filtering the edge set of \(G\) to those edges that cross the boundary of \(S\).

Given a vertex set \(S \subseteq V\) and an edge \(e = \{ u, v\} \in \mathrm{Sym}_2(V)\), we say that \(e\) crosses the boundary of \(S\) if exactly one of its endpoints lies in \(S\), i.e., \((u \in S \land v \notin S) \lor (u \notin S \land v \in S)\).

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.

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.

The set of faults with empty syndrome:

Given a simple graph \(G = (V, E)\) with decidable adjacency, the entangling circuit \(\prod _v \prod _{e \ni v} \mathrm{CX}_{v \to e}\) is a structure consisting of:

• the underlying graph \(G\),

• a gate specification: for each vertex \(v \in V\) and each edge \(e\) in the incidence set of \(v\), a \(\mathrm{CX}\) gate with control \(\mathrm{inl}(v) \in V \oplus \mathrm{Sym}_2(V)\) and target \(\mathrm{inr}(e) \in V \oplus \mathrm{Sym}_2(V)\).

A structure capturing the configuration of error correction rounds around the gauging measurement. It consists of:

• \(d\): the code distance (a positive natural number),

• roundsBefore: the number of EC rounds before gauging,

• roundsAfter: the number of EC rounds after gauging.

An error correction configuration provides full protection if

An abstract error process in the fault-tolerant procedure, consisting of:

• weight: the total number of faults,

• involvesGauging: whether the process involves the gauging measurement,

• involvesInitialBoundary: whether the process involves the initial boundary,

• involvesFinalBoundary: whether the process involves the final boundary.

An error process spans to the boundary if it involves the gauging measurement and at least one boundary (initial or final):

An error process spans to the final boundary if it involves both the gauging measurement and the final boundary.

An error process spans to the initial boundary if it involves both the gauging measurement and the initial boundary.

The exactness condition for a graph with cycles \(G\) consists of:

1. Cycles valid: every cycle \(c \in C\) is a valid cycle edge set (every vertex has even degree in \(c\)).

2. Cuts generate: every element of \(\ker (\delta _2)\) lies in \(\operatorname {im}(\delta )\), i.e., every \(1\)-cocycle is a coboundary.

The expander existence specification is the proposition that for all \(W \ge 2\), there exists a simple graph \(G\) on \(\mathrm{Fin}(W)\) with decidable adjacency such that:

1. \(G\) has bounded degree: \(\exists \, d \in \mathbb {N}\) such that \(\forall \, v,\; \deg _G(v) \le d\);

2. \(G\) is a strong expander: \(\mathrm{IsStrongExpander}(G)\) holds (i.e., the Cheeger constant \(h(G) \ge 1\)).

This is a cited result from the expander graph literature (probabilistic method on random regular graphs, or explicit constructions such as Ramanujan graphs or Margulis–Gabber–Galil graphs).

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\).

Two faults \(f\) and \(g\) are fault equivalent if they differ by a spacetime stabilizer:

The fault quotient is the quotient of \(\mathrm{SpacetimeFault}(V, E, M)\) by the spacetime stabilizer subgroup:

The fault setoid is the setoid on \(\mathrm{SpacetimeFault}(V, E, M)\) induced by the fault equivalence relation.

A record bundling the data required to apply the fault tolerance theorem to Algorithm 1:

• A proof that every spacetime logical fault admits a lower bound case decomposition.

• A witness: a spacetime logical fault of weight exactly \(d\).

A fault tolerance configuration is a structure bundling all preconditions needed to establish \(d_{ST} = d\). It consists of:

• A code distance \(d \in \mathbb {N}\) with \(d {\gt} 0\).

• An initial time \(t_i\) and final time \(t_o\) with \(t_i {\lt} t_o\) (the deformation interval is nonempty).

• The condition \((t_o - t_i) \geq d\) (sufficient measurement rounds).

• A Cheeger constant \(h(G) \in \mathbb {R}\) with \(h(G) \geq 1\) (strong expansion).

Given a fault tolerance configuration \(\mathrm{cfg}\), the number of measurement rounds is defined as

A spacetime fault \(F\) has a spacetime decomposition with respect to a detector collection \(DC\), base outcomes, logical effect predicate, and configuration \(\mathrm{cfg}\) if there exist spacetime faults \(F_{\mathrm{space}}\) and \(F_{\mathrm{time}}\) such that:

1. \(F\) is equivalent modulo stabilizers to \(F_{\mathrm{space}} \cdot F_{\mathrm{time}}\),

2. \(F_{\mathrm{space}}\) is a pure space fault at a single time step \(t_i\), and

3. \(F_{\mathrm{time}}\) is a pure time fault.

The interval of measurement rounds for a fault tolerance configuration \(\mathrm{cfg}\) is the finite set \([t_i, t_o) := \mathrm{Ico}(t_i, t_o)\).

The lower bound case enumeration for a spacetime fault \(F\) consists of two cases:

• Case 1 (timeNontrivial): There exists a pure time fault \(F_{\mathrm{time}}\) with \(\mathrm{weight}(F_{\mathrm{time}}) \geq \mathrm{numRounds}\) and \(\mathrm{weight}(F) \geq \mathrm{weight}(F_{\mathrm{time}})\).

• Case 2 (spaceLogical): There exists a pure space fault \(F_{\mathrm{space}}\) at time \(t_i\) with \(\mathrm{weight}(F_{\mathrm{space}}) \geq d\) and \(\mathrm{weight}(F) \geq \mathrm{weight}(F_{\mathrm{space}})\).

An original code logical operator consists of:

• A time step \(t\) of application (should be \({\lt} t_i\) or \({\gt} t_o\)).

• A map \(\mathrm{vertexPaulis} : V \to \mathrm{PauliType}\) assigning Pauli operators to each vertex qubit.

• A weight \(w \in \mathbb {N}\).

The conversion of an original logical operator \(L\) to a spacetime fault assigns:

• Space errors: For a vertex qubit \(v\) at time \(t\), the error is \(L.\mathrm{vertexPaulis}(v)\) if \(t = L.\mathrm{time}\), and \(I\) otherwise. For edge qubits, the error is always \(I\).

• Time errors: All time errors are \(\mathrm{false}\) (no measurement errors).

A fault-tolerance guarantee with its type, code distance, round counts before and after, and a Boolean indicating validity.

The time separation between the end of gauging and the final boundary. Since the final boundary is at \(t_{\mathrm{final}}\), this is defined to be \(0\).

The final boundary occurs at time \(t_{\mathrm{final}} = \texttt{config.t\_ final}\).

Addition on \(\mathrm{Finset}(\alpha )\) is defined via symmetric difference:

The type \(\mathrm{Finset}(\alpha )\) forms an additive commutative group with symmetric difference as addition, \(\emptyset \) as the zero element, and identity as negation (since every element is its own inverse in \(\mathbb {Z}/2\mathbb {Z}\)). The group axioms hold because:

• Associativity: \((S \mathbin {\triangle } T) \mathbin {\triangle } U = S \mathbin {\triangle } (T \mathbin {\triangle } U)\).

• Identity: \(\emptyset \mathbin {\triangle } S = S\) and \(S \mathbin {\triangle } \emptyset = S\).

• Inverse: \(S \mathbin {\triangle } S = \emptyset \).

• Commutativity: \(S \mathbin {\triangle } T = T \mathbin {\triangle } S\).

The type \(\mathrm{Finset}(\alpha )\) forms a module (vector space) over \(\mathbb {Z}/2\mathbb {Z}\), where addition is symmetric difference and scalar multiplication is as defined above. The module axioms are verified by case analysis on elements of \(\mathbb {Z}/2\mathbb {Z}\) (which are either \(0\) or \(1\)).

Scalar multiplication by \(\mathbb {Z}/2\mathbb {Z}\) on \(\mathrm{Finset}(\alpha )\) is defined as:

The type alias for flux check weight, represented as a natural number (the number of edges in the cycle).

The flux commutation count of an edge support set \(S_X^E \subseteq E\) with a cycle \(p \in C\) is the parity

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.

Information about the weight of a flux check: its numerical weight, whether it is considered high weight, and the reason.

The Freedman–Hastings decongestion specification asserts that there exists a constant \(C {\gt} 0\) such that for all \(W \ge 2\) and \(d \ge 1\) (representing any constant-degree-\(d\) graph on \(W\) vertices), there exist natural numbers \(R\) and \(\mathrm{cycleWeightBound}\) satisfying:

1. \(R \le C \cdot (\log _2 W)^2 + C\)  (i.e., \(R = O(\log ^2 W)\));

2. \(\mathrm{cycleWeightBound} \le 3\)  (all generating cycles have weight at most \(3\), achieved by triangulation).

This is a cited result from Freedman–Hastings requiring topological methods.

Given a binary vector \(v : \alpha \to \mathbb {Z}/2\mathbb {Z}\), we define the corresponding finset as the support of \(v\):

With full \(d\) rounds, the effective distance equals the original distance \(d\), and a threshold exists.

The complete gauging circuit for a simple graph \(G = (V,E)\) is a structure consisting of:

• the underlying graph \(G\),

• a first entangling circuit \(\mathcal{E}_1\) of type \(\mathrm{EntanglingCircuit}(G)\),

• an \(X\)-measurement specification on the vertices \(V\),

• a second entangling circuit \(\mathcal{E}_2\) of type \(\mathrm{EntanglingCircuit}(G)\),

• a \(Z\)-measurement specification on the edge set \(\mathrm{Sym}_2(V)\),

subject to the following conditions:

1. \(\mathcal{E}_1 = \mathcal{E}_2\) (the two entangling circuits are identical),

2. the \(X\)-measurement covers all vertices: \(\mathrm{qubits} = V\),

3. the \(X\)-measurement keeps all qubits: \(\mathrm{keep}(v) = \mathrm{true}\) for all \(v\),

4. the \(Z\)-measurement covers all edges: \(\mathrm{qubits} = E_G\),

5. the \(Z\)-measurement discards all qubits: \(\mathrm{keep}(e) = \mathrm{false}\) for all \(e\).

The set of all qubits used in a gauging circuit \(C\) for graph \(G\) is

The circuit qubit type for a graph \(G = (V,E)\) is an inductive type with two constructors:

• \(\mathrm{vertex}(v)\) for \(v \in V\): an original code (vertex) qubit,

• \(\mathrm{edge}(e)\) for \(e \in \mathrm{Sym}_2(V)\): an auxiliary (edge) qubit.

A circuit qubit \(q\) is an edge qubit if it has the form \(\mathrm{edge}(e)\) for some \(e\). Formally,

A gauging graph convention specifies how a connected graph \(G\) relates to the logical operator \(L\) being measured. It consists of:

• A vertex type \(V\) with a \(\mathrm{Fintype}\) instance and decidable equality,

• A simple graph structure on \(V\) with decidable adjacency,

• A proof that the graph is connected,

• A finite set \(\mathrm{logicalSupport} \subseteq V\) representing the support of \(L\),

• A proof that \(\mathrm{logicalSupport}\) is nonempty (i.e., \(L\) is nontrivial).

This captures the conventions: (1) vertices of \(G\) are identified with qubits in \(\operatorname {supp}(L)\), (2) each edge \(e \in E_G\) gets an auxiliary gauge qubit in \(\ket {0}\), (3) dummy vertices (\(V_G \setminus \operatorname {supp}(L)\)) get auxiliary qubits in \(\ket {+}\), and (4) dummy vertices have no effect on the measurement outcome.

The measurement outcome for a dummy vertex is defined to be \(\mathrm{plus}\) (i.e., \(+1\)), since the dummy qubit is in \(\ket {+}\), which is the \(+1\) eigenstate of \(X\).

The set of dummy vertices of a gauging graph \(G\) is defined as

The initial state for an edge qubit is always \(\ket {0}\):

All edges are assigned the \(\mathrm{EdgeQubit}\) type: for any edge \(e \in E_G\),

The effective logical support when gauging \(L\) with dummy vertices is the entire vertex set \(V_G\). This captures the convention that we gauge the operator \(L \cdot \prod _{v \in \mathrm{dummy}} X_v\):

A vertex \(v\) of a gauging graph \(G\) is a dummy vertex if \(v \notin \mathrm{logicalSupport}(G)\).

A vertex \(v\) of a gauging graph \(G\) is a support vertex if \(v \in \mathrm{logicalSupport}(G)\).

The total number of auxiliary qubits is the sum of edge qubits and dummy qubits:

The number of dummy vertices is \(|\mathrm{dummyVertices}(G)|\).

The number of edges \(|E_G|\) in the gauging graph, which equals the number of gauge qubits.

The total number of qubits involved in the gauging protocol is the sum of logical support qubits and auxiliary qubits:

The initial state for a vertex qubit \(v\) is determined by its qubit type:

The qubit type assigned to each vertex \(v\) of a gauging graph \(G\):

The Three Desiderata for Gauging Graph \(G\).

A graph \(G\) (equipped with a cycle structure) satisfies the gauging graph desiderata with respect to a collection of \(Z\)-type supports \(\mathcal{Z}\), path bound \(k\), and cycle bound \(w\) if the following three conditions hold simultaneously:

1. Short paths: \(\mathrm{ShortPaths}(G.\mathrm{graph}, \mathcal{Z}, k)\) — there exist paths of length at most \(k\) between any two vertices in the same \(Z\)-type support set.

2. Sufficient expansion: \(\mathrm{SufficientExpansion}(G.\mathrm{graph})\) — the Cheeger constant satisfies \(h(G) \geq 1\).

3. Low-weight cycles: \(\mathrm{LowWeightCycles}(G, w)\) — all generating cycles have weight at most \(w\).

The informal justifications from the remark are:

• Short paths \(\Longrightarrow \) deformed checks have bounded weight.

• \(h(G) \geq 1\) \(\Longrightarrow \) deformed code distance \(\geq \) original code distance.

• Low-weight cycles \(\Longrightarrow \) \(B_p\) flux operators have bounded weight.

• All three together \(\Longrightarrow \) constant qubit overhead.

Given \(z \in (\mathbb {Z}/2\mathbb {Z})^E\) in the image of \(\delta \) (i.e., there exists \(c\) with \(\delta c = z\)), the byproduct cochain \(c' = \mathrm{byproductCochain}(G, z)\) is a chosen \(0\)-cochain satisfying \(\delta c' = z\), obtained by the axiom of choice.

For a \(0\)-cochain \(c \in (\mathbb {Z}/2\mathbb {Z})^V\) and outcomes \(\varepsilon \), define

This represents \(\prod _{v : c_v = 1} \varepsilon _v^{c_v}\) in additive notation.

The Gauss law measurement outcomes assign to each vertex \(v \in V\) a value in \(\mathbb {Z}/2\mathbb {Z}\), where \(0\) represents the outcome \(+1\) and \(1\) represents the outcome \(-1\). Formally, \(\mathrm{GaussLawOutcomes}(V) = V \to \mathbb {Z}/2\mathbb {Z}\).

The logical operator \(L = \prod _v X_v\) has support equal to the all-ones vector \(\mathbf{1} \in (\mathbb {Z}/2\mathbb {Z})^V\).

The measured outcome \(\sigma \) is the product of all Gauss law outcomes, represented in \(\mathbb {Z}/2\mathbb {Z}\) as

Here \(\sigma = 0\) means \(+1\) (even number of \(-1\) outcomes) and \(\sigma = 1\) means \(-1\) (odd number).

For a \(0\)-cochain \(c \in (\mathbb {Z}/2\mathbb {Z})^V\), the operator \(X_V(c) = \prod _{v : c_v = 1} X_v\) is represented by its support vector, which is simply \(c\) itself.

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.

A configuration of key time points in the gauging procedure, consisting of:

• \(t_{\mathrm{start}}\): the start of the procedure,

• \(t_{\mathrm{initial}}\): the time of the initial gauging code deformation,

• \(t_{\mathrm{final}}\): the time of the final ungauging code deformation,

subject to the ordering constraint \(t_{\mathrm{start}} \le t_{\mathrm{initial}} \le t_{\mathrm{final}}\).

The total duration of the gauging measurement procedure:

The final \(A_v\) measurement time \(t_{\mathrm{final}} + \tfrac {1}{2}\), represented as measurement time step \(t_{\mathrm{final}}\).

The first \(A_v\) measurement time \(t_{\mathrm{initial}} - \tfrac {1}{2}\), represented as measurement time step \(t_{\mathrm{initial}} - 1\).

The duration of the gauged phase, from \(t_{\mathrm{initial}}\) to \(t_{\mathrm{final}}\):

The last \(A_v\) measurement time before the final time \(t_{\mathrm{final}} - \tfrac {1}{2}\), represented as measurement time step \(t_{\mathrm{final}} - 1\).

The second \(A_v\) measurement time \(t_{\mathrm{initial}} + \tfrac {1}{2}\), represented as measurement time step \(t_{\mathrm{initial}}\).

The gauging measurement occurs at times in the range

The four directions of generalization for the gauging procedure form an inductive type with constructors:

• finiteGroupReps: Any finite group representation with tensor product factorization.

• nonPauliOperators: Non-Pauli operators (which can produce magic states).

• quditSystems: Qudit systems with \(d {\gt} 2\) levels per site.

• nonabelianGroups: Nonabelian groups (with a local-vs-global caveat).

The function \(\mathrm{hasLocalGlobalCaveat} : \mathrm{GeneralizationDirection} \to \mathrm{Bool}\) returns true only for the nonabelian groups direction, indicating that only in this case do local measurements fail to determine the global charge.

The function \(\mathrm{procedureApplies} : \mathrm{GeneralizationDirection} \to \mathrm{Bool}\) returns true for all four generalization directions, indicating that the gauging procedure applies in each case.

A qudit system with local dimension \(d\) and \(n\) sites has total Hilbert space dimension

An inductive type representing possible measurement outcomes for \(X\)-basis measurements:

• plus: Outcome \(+1\).

• minus: Outcome \(-1\).

Multiplication of measurement outcomes, corresponding to the product of signs:

A function converting a measurement outcome to a sign \((\pm 1)\) as an integer: \(\mathrm{plus} \mapsto 1\) and \(\mathrm{minus} \mapsto -1\).

A graph with cycles is a structure \((G, V, E, C)\) where:

• \(V\), \(E\), \(C\) are finite types with decidable equality,

• \(G\) is a simple graph on \(V\) with decidable adjacency,

• \(\mathrm{edgeEndpoints} : E \to V \times V\) assigns to each edge its two endpoints,

• for each edge \(e\), the endpoints are adjacent: \(G.\mathrm{Adj}(\mathrm{edgeEndpoints}(e)_1, \mathrm{edgeEndpoints}(e)_2)\),

• edges are symmetric: adjacency holds in both directions,

• \(\mathrm{cycles} : C \to \mathrm{Finset}(E)\) assigns to each cycle index its set of edges.

The all-ones vector \(\mathbf{1} \in \mathbb {F}_2^V\) is defined by \(\mathbf{1}(v) = 1\) for all \(v \in V\).

A Pauli operator \(P\) (represented by its \(Z\)-support on \(V\)) anticommutes with \(L\) if its \(Z\)-support has odd cardinality:

Two vertices \(v, w \in V\) are adjacent (written \(v \sim w\)) if there exists an edge \(e \in E\) whose endpoints are \(\{ v, w\} \).

The standard basis vectors are defined as:

• \(\mathrm{basisV}(v) = \mathbf{e}_v \in \mathbb {Z}_2^V\): the vector with \(1\) at position \(v\) and \(0\) elsewhere,

• \(\mathrm{basisE}(e) = \mathbf{e}_e \in \mathbb {Z}_2^E\): the vector with \(1\) at position \(e\) and \(0\) elsewhere,

• \(\mathrm{basisC}(c) = \mathbf{e}_c \in \mathbb {Z}_2^C\): the vector with \(1\) at position \(c\) and \(0\) elsewhere.

Formally, \(\mathrm{basisV}(v) = \pi _{\mathrm{single}}(v, 1)\) (and similarly for edges and cycles).

The second boundary map \(\partial _2 : \mathbb {Z}_2^C \to \mathbb {Z}_2^E\) is the \(\mathbb {Z}_2\)-linear map defined by:

where \(\partial _2 c\) is the characteristic vector of edges in cycle \(c\).

The boundary of a single cycle \(c\) is the characteristic vector of its edges:

The boundary map \(\partial : \mathbb {Z}_2^E \to \mathbb {Z}_2^V\) is the \(\mathbb {Z}_2\)-linear map defined by:

where \(\partial e = \mathbf{e}_v + \mathbf{e}_{v'}\) for edge \(e = \{ v, v'\} \).

The boundary of a single edge \(e\) with endpoints \((v, v')\) is:

the binary vector with \(1\)s at positions \(v\) and \(v'\).

The boundary support of an edge-path \(\gamma \) is the set of vertices where the boundary is nonzero:

The second coboundary map \(\delta _2 : \mathbb {Z}_2^E \to \mathbb {Z}_2^C\) is the \(\mathbb {Z}_2\)-linear map defined by:

where \(\delta _2 e\) is the characteristic vector of cycles containing \(e\).

The second coboundary of a single edge \(e\) is the characteristic vector of cycles containing \(e\):

The coboundary map \(\delta : \mathbb {Z}_2^V \to \mathbb {Z}_2^E\) is the \(\mathbb {Z}_2\)-linear map defined by:

where \(\delta v\) is the characteristic vector of edges incident to \(v\).

The coboundary of a single vertex \(v\) is the characteristic vector of edges incident to \(v\):

The parameters of an \([[n, k, d]]\) stabilizer code consist of:

• \(n\): the number of physical qubits,

• \(k\): the number of logical qubits,

• a proof that \(n \geq k\).

The dimension of an \([[n, k]]\) code is \(2^k\).

The number of independent stabilizers in an \([[n, k]]\) code is \(n - k\).

A Pauli operator \(P\) (represented by its \(Z\)-support on \(V\)) commutes with \(L\) if its \(Z\)-support has even cardinality:

After applying the Pauli corrections, the corrected outcomes are the constant function \(v \mapsto 0\) for all \(v \in V\), representing that every \(A_v\) now has eigenvalue \(+1\).

The cuts of \(G\) generate all cocycles if every edge-chain \(f\) in \(\ker (\delta _2)\) is in \(\operatorname {im}(\delta )\):

A cycle \(c\) contains an edge \(e\) if \(e \in \mathrm{cycles}(c)\).

The cycle-edge incidence matrix \(N : C \times E \to \mathbb {Z}_2\) is defined by:

The set of edges that are both in cycle \(p\) and incident to vertex \(v\):

The set of cycles containing a given edge \(e\) is:

The cycles of \(G\) generate all cycles if every edge-chain \(f\) with zero boundary can be written as a sum of cycle boundaries:

A deformable Pauli operator on a graph \(G = (V, E, C)\) is a structure consisting of:

• \(S_X^V \subseteq V\): the \(X\)-type support on vertices,

• \(S_Z^V \subseteq V\): the \(Z\)-type support on vertices,

• \(S_X^E \subseteq E\): the \(X\)-type support on edges,

• \(S_Z^E \subseteq E\): the \(Z\)-type support on edges,

• \(\sigma \in \mathbb {Z}_4\): the global phase (\(0 = +1\), \(1 = +i\), \(2 = -1\), \(3 = -i\)),

• The deformability condition: \(|S_Z^V| \equiv 0 \pmod{2}\).

The deformability condition is equivalent to \(P\) commuting with the logical operator \(L = \prod _{v \in V} X_v\).

The symplectic form between the deformed operator \(\tilde{P}\) and the Gauss law operator \(A_v\) is defined as the count of anticommuting pairs:

where \(\mathrm{inc}(v)\) denotes the set of edges incident to \(v\).

When \(P\) originally has no \(Z\)-support on edges (i.e., \(S_Z^E(P) = \emptyset \)), the symplectic form simplifies to:

The deformed check of a stabilizer check \(s\) along an edge-path \(\gamma \) is defined as

which is an alias for the DeformedOperator construction applied to a stabilizer check.

A valid deformed code setup for a graph \(G\) and code parameters \(\mathrm{code}\) consists of:

• The original stabilizer checks: \(\mathrm{checks} : \mathrm{Fin}(n-k) \to \mathrm{StabilizerCheck}(G)\).

• Valid deforming paths for each check: \(\mathrm{paths}(j)\) is an edge path for each \(j\).

• Original checks have no Z-support on edges: \(\forall j,\; \mathrm{checks}(j).\mathrm{zSupportOnE} = \emptyset \).

• Paths satisfy the boundary condition: \(\forall j,\; \partial (\mathrm{paths}(j)) = \mathcal{S}_Z(\mathrm{checks}(j)) \cap V_G\).

• All cycles in \(C\) are valid (geometric constraint).

• \(|V| \geq 1\).

• Euler’s formula holds: \(|C| = |E| - |V| + 1\).

• Graph is connected: \(|V| \leq |E|\).

• The original code has at least one logical qubit: \(k \geq 1\).

Given a deformable Pauli operator \(P\) on graph \(G\) and an edge-path \(\gamma \subseteq E\), the deformed operator \(\tilde{P} = P \cdot \prod _{e \in \gamma } Z_e\) is defined as the deformable Pauli operator with:

• \(S_X^V(\tilde{P}) = S_X^V(P)\) (X-support on vertices unchanged),

• \(S_Z^V(\tilde{P}) = S_Z^V(P)\) (Z-support on vertices unchanged),

• \(S_X^E(\tilde{P}) = S_X^E(P)\) (X-support on edges unchanged),

• \(S_Z^E(\tilde{P}) = S_Z^E(P) \oplus \gamma \) (Z-support on edges is the symmetric difference with \(\gamma \)),

• \(\sigma (\tilde{P}) = \sigma (P)\) (phase unchanged).

The deformability condition \(|S_Z^V(\tilde{P})| \equiv 0 \pmod{2}\) is inherited from \(P\).

An edge-path in a graph \(G\) is a subset \(\gamma \subseteq E\) of edges, represented as a finite set.

The boundary of an edge-path \(\gamma \) is defined as \(\partial \gamma = \partial _1(\boldsymbol {\gamma })\), where \(\partial _1\) is the boundary map and \(\boldsymbol {\gamma }\) is the binary vector representation of \(\gamma \). This gives a vector in \(\mathbb {Z}_2^V\) whose value at each vertex \(v\) counts (modulo 2) the number of edges in \(\gamma \) incident to \(v\).

Given a graph \(G\) and an edge-path \(\gamma \subseteq E\), the edge-path vector is the binary vector \(\boldsymbol {\gamma } \in \mathbb {Z}_2^E\) defined by

The weight of an edge-path \(\gamma \) is its cardinality:

The set of vertices incident to an edge \(e\) (its two endpoints) is:

The edge \(Z\)-operator support of a path \(\gamma \) is simply the edge-set \(\gamma \) itself, representing the set of edges on which \(Z\)-operators are applied:

The intersection of the \(Z\)-support of \(B_p\) and the \(X\)-support of \(A_v\):

The symplectic form between a flux operator \(B_p\) and a Gauss law operator \(A_v\):

i.e., the number of edges in cycle \(p\) that are incident to vertex \(v\).

The symplectic form between two flux operators. For \(Z\)-type operators:

Formally:

The \(X\)-support of a flux operator on edges is also empty:

The \(X\)-support of a flux operator on vertices is empty (\(Z\)-type operators have no \(X\) component):

The \(Z\)-support of \(B_p\) on edges (edges in cycle \(p\)):

The edge support of flux operator \(B_p\): \(1\) at edges in cycle \(p\), \(0\) elsewhere. This represents \(B_p = \prod _{e \in p} Z_e\). For a graph \(G\) and cycle \(p\):

i.e., the image of cycle \(p\) under the second boundary map.

The vertex support of flux operator \(B_p\): zero everywhere. Since \(B_p\) is a \(Z\)-type operator, it has no \(X\) component on vertices. For any graph \(G\) and cycle \(p\):

The weight of flux operator \(B_p\), defined as the number of edges in cycle \(p\):

A gauging measurement for a graph \(G\) consists of a measurement outcome function \(\varepsilon : V \to \mathbb {Z}/2\mathbb {Z}\), recording the outcome \(\varepsilon _v \in \{ +1, -1\} \) for each Gauss law operator \(A_v\) (where \(0\) encodes \(+1\) and \(1\) encodes \(-1\)).

The number of constraints among Gauss law operators is \(1\) (the single product constraint \(\prod _v A_v = L\)).

The number of Gauss law operators equals the number of vertices:

The abelian group generated by \(\{ A_v\} \) has order

The number of independent Gauss law generators is

The sum of all edge supports of Gauss law operators:

The sum of all vertex supports of Gauss law operators:

The symplectic form between two Gauss law operators \(A_v\) and \(A_w\) is defined as

For \(X\)-type operators, this equals \(|\emptyset | + |\emptyset | = 0\).

The \(X\)-support of \(A_v\) on edges (edges incident to \(v\)):

The \(Z\)-support of a Gauss law operator on edge qubits is also empty:

The \(Z\)-support of a Gauss law operator on vertex qubits is the empty set, since Gauss law operators are purely \(X\)-type:

The edge support of Gauss law operator \(A_v\) is \(1\) at edges incident to \(v\) and \(0\) elsewhere. Formally,

the coboundary of vertex \(v\). This represents \(\prod _{e \ni v} X_e\) in the product \(A_v = X_v \prod _{e \ni v} X_e\).

The total support size of \(A_v\) is \(1\) (for the vertex qubit) plus \(\deg (v)\) (for the edge qubits):

The vertex support of Gauss law operator \(A_v\) is a binary vector with \(1\) at position \(v\) and \(0\) elsewhere. Formally,

the basis vector at \(v\). This represents \(X_v\) in the product \(A_v = X_v \prod _{e \ni v} X_e\).

A graph with valid cycles extends a GraphWithCycles structure with the additional property that every cycle \(c \in C\) satisfies the valid cycle condition: \(\operatorname {cycles}(c)\) is a valid cycle edge set.

A graph \(G\) has valid paths if for any even-cardinality subset \(S \subseteq V\), there exists an edge-path \(\gamma \) such that \(\gamma \) is a valid deforming path for \(S\):

This follows from graph connectivity: for two vertices, take any path between them; for larger even-cardinality sets, pair up vertices and connect each pair.

The incidence matrix \(M : V \times E \to \mathbb {Z}_2\) is defined by:

The set of edges incident to a vertex \(v\) is:

The number of independent cycles in a connected graph according to Euler’s formula. For a connected graph with vertex set \(V\) and edge set \(E\):

We represent this as an integer to handle the subtraction correctly:

The initial stabilizer condition: each edge qubit in state \(\lvert 0\rangle \) is stabilized by \(Z_e\). Represented as \(Z\lvert 0\rangle = +\lvert 0\rangle \), so the measurement outcome is \(0\) (for \(+1\)) in \(\mathbb {Z}/2\mathbb {Z}\):

A stabilizer check \(s\) is in Set \(\mathcal{C}\) if it has no \(Z\)-support on graph vertices:

For these checks, no deformation is needed.

A stabilizer check \(s\) is in Set \(\mathcal{S}\) if it has nontrivial \(Z\)-support on graph vertices:

These checks are genuinely deformed by the gauging procedure.

A graph \(G\) is connected if for any two vertices \(v, w \in V\), \(w\) is reachable from \(v\) by the reflexive-transitive closure of the adjacency relation.

An edge \(e\) is incident to a vertex \(v\) if \(v\) is one of its endpoints:

An edge-path \(\gamma \) is a minimum-weight valid deforming path for \(S_Z^V\) if:

1. \(\gamma \) is a valid deforming path: \(\partial \gamma = \mathbf{s}_{S_Z^V}\), and

2. \(\gamma \) has minimum weight among all valid paths: for all valid paths \(\gamma '\), \(w(\gamma ) \leq w(\gamma ')\).

A cycle \(p\) is valid if every vertex has \(0\) or \(2\) incident edges from the cycle:

A set of edges \(S \subseteq E\) is a valid cycle edge set in a graph \(G\) if every vertex \(v \in V\) has even degree in \(S\), i.e.,

An edge-path \(\gamma \) is a valid deforming path for a \(Z\)-support \(S \subseteq V\) if the boundary of \(\gamma \) equals the \(Z\)-support vector:

where \(\mathbf{s}_S\) is the binary vector representation of \(S\). Equivalently, \(\partial \gamma = S\) as subsets of \(V\) (via their characteristic functions in \(\mathbb {Z}_2^V\)).

The product of measurement outcomes as a \(\mathbb {Z}/2\mathbb {Z}\) sum:

Convert a measurement outcome to \(\mathbb {Z}/2\mathbb {Z}\):

The original stabilizer \(s_j\) has eigenvalue \(+1\) on the code state \(|\psi \rangle \). This is encoded as \(0 \in \mathbb {Z}/2\mathbb {Z}\) (representing \(+1\)).

An original code state encodes the input assumption that the original code state \(|\psi \rangle \) is in the \(+1\) eigenspace of all stabilizer generators. This is the defining property of stabilizer codes: the code space is the simultaneous \(+1\) eigenspace of all stabilizer generators.

Given a gauging measurement \(m\), a Pauli correction \(X_v\) is needed at vertex \(v\) if and only if \(m.\mathrm{outcome}(v) = 1\) in \(\mathbb {Z}/2\mathbb {Z}\) (i.e., the measurement outcome was \(-1\)).

A stabilizer check from the original code is a DeformablePauliOperator on the graph \(G\). It carries the additional semantic meaning that it represents a generator of the original code’s stabilizer group. The key inherited property is that \(|\mathcal{S}_Z \cap V_G|\) is even (the check commutes with \(L\)).

The total qubit count in the deformed system is \(n + |E|\), where \(n\) is the number of original physical qubits and \(|E|\) is the number of edge qubits.

The total number of independent stabilizers in the deformed system is

arising from \(|V|\) Gauss law stabilizers, \(|E| - |V| + 1\) flux stabilizers, and \(n - k\) deformed checks.

The support of a binary vector \(f : V' = V \to \mathbb {Z}_2\) is the set of vertices where \(f\) is nonzero:

We define the binary vector spaces:

• \(\mathbb {Z}_2^V := V \to \mathbb {Z}_2\) (binary vectors over vertices),

• \(\mathbb {Z}_2^E := E \to \mathbb {Z}_2\) (binary vectors over edges),

• \(\mathbb {Z}_2^C := C \to \mathbb {Z}_2\) (binary vectors over cycles).

Each carries a natural \(\mathbb {Z}_2\)-module structure.

The degree of vertex \(v\) in the graph \(G\) is the number of edges incident to \(v\):

The degree of vertex \(v\) modulo 2 in an edge-vector \(f \in \mathbb {F}_2^E\) is

The \(X\)-type support of a stabilizer check \(s\) restricted to the graph vertices is defined as \(s.\mathrm{xSupportOnV}\).

The zero vector \(\mathbf{0} \in \mathbb {F}_2^V\) is defined by \(\mathbf{0}(v) = 0\) for all \(v \in V\).

The \(Z\)-support cardinality of a stabilizer check \(s\) is defined as

The \(Z\)-type support of a stabilizer check \(s\) restricted to the graph vertices \(V_G\) is defined as

This corresponds to \(\mathcal{S}_Z \cap V_G\) in the paper notation.

Given a graph \(G = (V, E, C)\) and a Pauli operator with \(Z\)-type support \(S_Z \subseteq V\), the \(Z\)-type support restricted to the graph vertices is \(S_Z \cap V_G\). Since \(S_Z\) is already given as a subset of \(V\), this is simply \(S_Z\) itself.

Given a graph \(G\) and a subset \(S \subseteq V\), the \(Z\)-support vector is the binary vector \(\mathbf{s} \in \mathbb {Z}_2^V\) defined by

A structure recording the code parameters \([[n, k, d]]\) of a quantum error-correcting code, where \(n\) is the number of physical qubits, \(k\) is the number of logical qubits, and \(d\) is the code distance.

The parameter \(\ell = 12\) for the Gross code.

The group algebra for the Gross code, \(\mathrm{GGroupAlg} = \mathrm{GroupAlg}(12, 6)\).

The monomial set for the Gross code, \(\mathrm{GM} = M(\ell , m) = M(12, 6)\).

The Gross code is a \([[144, 12, 12]]\) Bivariate Bicycle code with parameters \(\ell = 12\), \(m = 6\), and polynomials \(A = x^3 + y^2 + y\), \(B = y^3 + x^2 + x\).

The claimed parameters of the Gross code: \([[144, 12, 12]]\), i.e., \(n = 144\), \(k = 12\), \(d = 12\).

For a monomial \(\alpha \in M\), the \(X\)-type logical operator \(\bar{X}_\alpha = X(\alpha f, 0)\), which has weight \(12\).

For a monomial \(\beta \in M\), the \(X\)-type logical operator \(\bar{X}'_\beta = X(\beta g, \beta h)\).

For a monomial \(\beta \in M\), the \(Z\)-type logical operator \(\bar{Z}_\beta = Z(\beta h^T, \beta g^T)\).

For a monomial \(\alpha \in M\), the \(Z\)-type logical operator \(\bar{Z}'_\alpha = Z(0, \alpha f^T)\).

The parameter \(m = 6\) for the Gross code.

Shorthand for monomials \(x^a y^b\) in the Gross code group algebra:

where \(a \in \mathbb {Z}/\ell \mathbb {Z}\) and \(b \in \mathbb {Z}/m\mathbb {Z}\).

The multiplication of a monomial \(\alpha \) by a group algebra element \(p\) (left multiplication). The map \(\alpha \cdot p\) shifts all monomials in \(p\) by \(\alpha \), defined as \(\mathrm{mapDomain}(\cdot + \alpha , p)\).

The polynomial \(A\) for the Gross code:

The polynomial \(B\) for the Gross code:

The polynomial \(f\) for \(X\)-type logical operators:

The polynomial \(g\) for logical operators:

The polynomial \(h\) for logical operators:

The code distance of the Gross code:

Expansion edge 1 connects \(x^2\) and \(x^5 y^3\):

Expansion edge 2 connects \(x^2\) and \(x^6\):

Expansion edge 3 connects \(x^5 y^3\) and \(x^{11} y^3\):

Expansion edge 4 connects \(x^7 y^3\) and \(x^{11} y^3\):

The concrete gauging graph for \(\bar{X}_\alpha \) in the Gross code, with parameters:

• \(|V| = 12\) vertices,

• \(18\) initial edges from \(Z\)-check connectivity,

• \(4\) expansion edges,

• \(4\) redundant cycles,

• maximum new degree \(6\),

• maximum affected degree \(7\).

The structure recording the parameters of the gauging graph for \(\bar{X}_\alpha \) in the Gross code. It consists of:

• numVertices : the number of vertices (monomials in \(f\)),

• numInitialEdges : the number of initial edges from \(Z\)-check connectivity,

• numExpansionEdges : the number of additional expansion edges,

• numRedundantCycles : the number of redundant cycles from the BB code’s \(Z\)-check structure,

• maxNewDegree : the maximum Tanner graph degree for new elements,

• maxAffectedDegree : the maximum Tanner graph degree for affected existing elements.

The type alias for monomials in the Gross code group:

The weight of the logical operator \(\bar{X}_\alpha = X(\alpha f, 0)\), equal to the number of monomials in \(f\):

The \(12\) monomials appearing in \(f\), represented as elements of \(\mathbb {Z}/12\mathbb {Z} \times \mathbb {Z}/6\mathbb {Z}\):

These correspond to the monomials of \(f = 1 + x + x^2 + x^3 + x^6 + x^7 + x^8 + x^9 + (x + x^5 + x^7 + x^{11})y^3\).

The number of \(Z\) checks adjacent to \(\bar{X}_\alpha \):

These arise from the connectivity condition: vertices \(\gamma , \delta \in f\) are connected if \(\gamma = B_i^T B_j \delta \) for some \(i, j \in \{ 1,2,3\} \).

The number of independent cycles in the gauging graph, computed via Euler’s formula for connected graphs:

The number of needed \(B_p\) flux checks, after accounting for redundancy from the BB code’s \(Z\) checks:

The number of new qubits equals the total number of edges (one gauge qubit per edge):

The number of new \(X\) checks equals the number of vertices (one Gauss’s law operator \(A_v\) per vertex):

The number of new \(Z\) checks equals the number of needed flux checks:

The total number of edges in the gauging graph:

The overhead of previous schemes, which scales as \(O(Wd)\) where \(W\) is the logical operator weight and \(d\) is the code distance:

The target distance for the gauging graph, set to match the Gross code distance:

The total overhead of the gauging approach:

An inductive type classifying fault-tolerance guarantees:

• worstCase: holds for any surrounding computation,

• contextDependent: depends on the specific context.

A half-integer time representation, defined as an inductive type with two constructors:

• \(\mathtt{integer}(n)\) represents the integer time step \(n \in \mathbb {Z}\),

• \(\mathtt{halfInteger}(n)\) represents the half-integer time step \(n + \tfrac {1}{2}\) for \(n \in \mathbb {Z}\).

The ceiling (rounded-up integer part) of a half-integer time:

The floor (integer part) of a half-integer time:

A predicate that checks whether a half-integer time is a half-integer time:

A predicate that checks whether a half-integer time is an integer time:

The predecessor function on half-integer times, retreating by \(\tfrac {1}{2}\):

That is, \(n \mapsto n - \tfrac {1}{2}\) and \(n + \tfrac {1}{2} \mapsto n\).

The successor function on half-integer times, advancing by \(\tfrac {1}{2}\):

That is, \(n \mapsto n + \tfrac {1}{2}\) and \(n + \tfrac {1}{2} \mapsto n + 1\).

Convert a half-integer time to a rational number for comparison:

A class asserting that a graph \(G\) satisfies the Freedman–Hastings decongestion bound. This states:

1. There exists a layer bound \(\mathrm{lb}\) with \(\mathrm{lb}.\mathrm{numLayers} \leq (\log _2 |V| + 1)^2 \cdot (\mathrm{maxDegree} + 1)\).

2. The cycle-degree bound \(c {\gt} 0\).

3. The graph has bounded degree: for all \(v \in V\), \(|G.\mathrm{incidentEdges}(v)| \leq \mathrm{maxDegree}\).

A fault \(f\) has empty syndrome if it violates no detectors:

A fault \(F\) has empty syndrome if it violates no detectors:

The predicate \(\mathrm{hasLogicalFault}(\mathit{DC}, \mathit{logicalEffect})\) holds if there exists at least one spacetime fault \(F\) such that \(F\) is a spacetime logical fault:

A graph \(G\) with cycles has a valid assignment with cycle-degree bound \(c\) and \(R\) layers if there exists a cycle-layer assignment such that for every edge \(e\), \(\mathrm{cycleDegree}(G.\mathrm{cycles}, e) \leq c\).

A hypergraph on vertices \(V\) with hyperedges indexed by \(H\) is a structure consisting of an incidence function

mapping each hyperedge to the set of its incident vertices. This generalizes a graph, where each edge connects exactly two vertices, to the case where each hyperedge may connect an arbitrary subset of vertices.

The all-ones vector on \(V\) is the constant function \(\mathbf{1}_V : V \to \mathbb {Z}_2\) defined by \(\mathbf{1}_V(v) = 1\) for all \(v \in V\). This represents the logical operator \(L = \prod _v X_v\).

The hyperedge support of \(A_v\) is a binary vector on \(H\) with \(1\) at each hyperedge containing \(v\):

The vertex support of the generalized Gauss law operator \(A_v\) is a binary vector on \(V\) with \(1\) at position \(v\) and \(0\) elsewhere, representing the \(X_v\) factor:

The \(Z\)-type hyperedge support of \(A_v\) is also the zero vector:

The \(Z\)-type support of \(A_v\) on vertex qubits is the zero vector, since \(A_v\) is a purely \(X\)-type operator:

The generalized coboundary map \(\delta : \mathbb {Z}_2^V \to \mathbb {Z}_2^H\) for the hypergraph is the \(\mathbb {Z}_2\)-linear map defined by

This is the transpose of the incidence matrix.

The incidence entry of a hypergraph \(\mathrm{HG}\) at hyperedge \(h\) and vertex \(v\) is defined as

where the values are taken in \(\mathbb {Z}/2\mathbb {Z}\).

The set of hyperedges incident to vertex \(v\) is

A hypergraph is graph-like if every hyperedge has exactly \(2\) vertices:

A hyperedge \(h\) is \(k\)-local if it contains at most \(k\) vertices:

A hypergraph is \(k\)-local if all of its hyperedges are \(k\)-local:

The number of new checks equals the number of vertices (one \(A_v\) per vertex):

The number of new qubits introduced in the generalized gauging procedure equals the number of hyperedges:

Given a \(\mathrm{GraphWithCycles}\) \(G\) on vertices \(V\), edges \(E\), and cycles \(C\), we construct a hypergraph on vertices \(V\) with hyperedges indexed by \(E\) by setting

for each edge \(e \in E\). This embeds ordinary graphs into the hypergraph framework.

The operator kernel of a hypergraph \(\mathrm{HG}\) is the kernel of the parity-check map:

This is a \(\mathbb {Z}_2\)-submodule of \(\mathbb {Z}_2^V\) that characterizes the abelian group of commuting \(X\)-type operators.

The parity-check map \(H_Z : \mathbb {Z}_2^V \to \mathbb {Z}_2^H\) of a hypergraph \(\mathrm{HG}\) is the \(\mathbb {Z}_2\)-linear map defined by

for each hyperedge \(h \in H\). The kernel of this map characterizes the abelian group of commuting \(X\)-type operators.

The symplectic inner product on hyperedge qubits is defined analogously:

The symplectic inner product on vertex qubits for two Pauli operators with \(X\)-type supports \(xS_1, xS_2\) and \(Z\)-type supports \(zS_1, zS_2\) is

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.

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.

The threshold property for inferred flux measurement: no threshold is expected without further modifications.

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 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.

An initialization fault record for vertex type \(V\) and edge type \(E\) is a function \(\mathrm{QubitLoc}(V, E) \to \mathrm{TimeStep} \to \mathrm{Bool}\), indicating whether each initialization is faulty.

The time separation between the initial boundary and the start of gauging, defined as \((t_{\mathrm{initial}} - t_{\mathrm{start}})\) converted to a natural number.

The initial boundary occurs at time \(t_0 = \texttt{config.t\_ start}\), the start of the procedure.

An initialization event for vertex type \(V\) and edge type \(E\) consists of:

• A qubit location \(\mathrm{qubit} : \mathrm{QubitLoc}(V, E)\),

• A time step \(\mathrm{time} : \mathrm{TimeStep}\),

• An expected parity \(\mathrm{expectedParity} \in \mathbb {Z}/2\mathbb {Z}\).

A standard initialization event for qubit \(q\) at time \(t\) is the initialization event \(\langle q, t, 0 \rangle \), i.e., with expected parity \(0\) (\(+1\) outcome).

An initialization fault over qubit types \(V, E\) is a structure consisting of:

• qubit : \(\texttt{QubitLoc}(V, E)\) — the qubit being initialized,

• time : \(\mathbb {N}\) — the time step of initialization,

• effectiveError : \(\texttt{PauliType}\) — the effective Pauli error applied after perfect initialization.

A faulty initialization of state \(|\psi \rangle \) is modeled as perfect initialization followed by an immediate space-fault.

The identity initialization fault at qubit \(q\) and time \(t\) is \(\langle q, t, I \rangle \), representing no error during initialization.

An initialization fault \(f\) represents an actual error if \(\operatorname {isError}(f.\texttt{effectiveError}) = \text{true}\).

An initialization fault \(f\) is converted to an equivalent space-fault:

The space-fault occurs at the same qubit and time as the initialization.

A detector \(D\) is in the syndrome of a fault \(f\) if \(D \in \mathrm{computeSyndrome}(\mathrm{DC}, \mathrm{base}, f)\).

The set of integer time steps in a range \([t_1, t_2]\):

The measurement time immediately after integer time \(t\) is \(t + \tfrac {1}{2}\), represented by the measurement time step \(t\).

The measurement time immediately before integer time \(t\) is \(t - \tfrac {1}{2}\), represented by the measurement time step \(t - 1\).

Converts an integer time step \(t\) to the half-integer time \(\mathtt{integer}(t)\).

A simple graph \(G\) is an expander if there exists a constant \(c {\gt} 0\) such that \(h(G) \geq c\):

A flux check has high weight if its weight exceeds a given threshold.

A stabilizer code \(C\) is Low-Density Parity-Check (LDPC) if there exist constants bounding:

• Maximum check weight \(w_{\max } \in \mathbb {N}\): for every generator \(s \in C.\texttt{stabilizers}.\texttt{generators}\), \(|\operatorname {supp}(s)| \leq w_{\max }\).

• Maximum qubit degree \(\Delta _{\max } \in \mathbb {N}\): for every qubit \(i \in \operatorname {Fin}(C.n)\), the number of generators whose support contains \(i\) is at most \(\Delta _{\max }\).

A spacetime fault \(F\) is a logical fault if it has empty syndrome but is non-trivial:

An isolated context where the position is isolated, there is one total operation, no surrounding EC is present, and zero surrounding EC rounds.

An edge support set \(S_X^E \subseteq E\) is a \(1\)-cocycle if it has even intersection with every cycle:

A fault \(f\) is a spacetime logical fault with respect to a detector collection \(\mathrm{DC}\), base outcomes, and logical effect predicate \(\ell \) if:

1. \(f\) has empty syndrome: \(\mathrm{hasEmptySyndrome}(\mathrm{DC}, \mathrm{base}, f)\), and

2. \(f\) affects logical information: \(\mathrm{affectsLogicalInfo}(\ell , f)\).

A fault \(f\) is a spacetime stabilizer with respect to a detector collection \(\mathrm{DC}\), base outcomes, and logical effect predicate \(\ell \) if:

1. \(f\) has empty syndrome: \(\mathrm{hasEmptySyndrome}(\mathrm{DC}, \mathrm{base}, f)\), and

2. \(f\) preserves logical information: \(\mathrm{preservesLogicalInfo}(\ell , f)\).

A spacetime fault \(F\) is a spacetime stabilizer if it has empty syndrome and is trivial:

A simple graph \(G\) is a strong expander if its Cheeger constant is at least \(1\):

This is the condition required in this work to preserve the distance of the original code.

A dummy grid bridges non-adjacent patches. It is a structure consisting of:

• \(\mathrm{rows} : \mathbb {N}\) with \(\mathrm{rows} \geq 2\),

• \(\mathrm{gap\_ width} : \mathbb {N}\) with \(\mathrm{gap\_ width} \geq 1\).

The adjacency relation for the combined graph used in generalized lattice surgery: two copies of a graph \(G\) on vertex set \(V\) with a set of bridge edges. Two vertices \(x, y \in \mathrm{Bool} \times V\) are adjacent if:

1. \(x_1 = y_1\) and \(G.\mathrm{Adj}\; x_2\; y_2\) (intra-copy adjacency), or

2. \(x_1 \neq y_1\) and \(((x_2, y_2) \in \mathrm{bridges}\) or \((y_2, x_2) \in \mathrm{bridges})\) (cross-copy bridge).

The combined graph for generalized lattice surgery: two copies of \(G\) with bridge edges, forming a valid simple graph on \(\mathrm{Bool} \times V\).

Grid graph adjacency on \(\mathrm{Fin}(\mathrm{rows}) \times \mathrm{Fin}(\mathrm{gap\_ width} + 2)\): two vertices \(x, y\) are adjacent if they are unit-distance neighbors, i.e.,

The grid graph on \(\mathrm{Fin}(\mathrm{rows}) \times \mathrm{Fin}(\mathrm{gap\_ width} + 2)\) as a simple graph with adjacency \(\mathrm{gridAdj}\).

The adjacency relation for the ladder graph on \(n\) rungs. Two vertices \(x, y \in \mathrm{Bool} \times \mathrm{Fin}(n)\) are adjacent if:

1. \(x_1 \neq y_1\) and \(x_2 = y_2\) (horizontal rung), or

2. \(x_1 = y_1\) and \(x_2 + 1 = y_2\) (vertical rail going up), or

3. \(x_1 = y_1\) and \(y_2 + 1 = x_2\) (vertical rail going down).

The cycle type for the ladder: one square face for each pair of consecutive rungs. Formally, \(\mathrm{LadderCycle}(n) := \mathrm{Fin}(n-1)\).

The edges forming cycle \(c\) of the ladder: each square face consists of

The edge type for the ladder graph on \(n\) rungs is an inductive type with three constructors:

1. \(\mathrm{rung}(i)\) for \(i \in \mathrm{Fin}(n)\): horizontal rung connecting \((\mathrm{false}, i)\) to \((\mathrm{true}, i)\).

2. \(\mathrm{leftRail}(i)\) for \(i \in \mathrm{Fin}(n-1)\): left vertical rail connecting \((\mathrm{false}, i)\) to \((\mathrm{false}, i+1)\).

3. \(\mathrm{rightRail}(i)\) for \(i \in \mathrm{Fin}(n-1)\): right vertical rail connecting \((\mathrm{true}, i)\) to \((\mathrm{true}, i+1)\).

The endpoint function for each ladder edge:

• \(\mathrm{rung}(i) \mapsto ((\mathrm{false}, i), (\mathrm{true}, i))\),

• \(\mathrm{leftRail}(i) \mapsto ((\mathrm{false}, i), (\mathrm{false}, i+1))\),

• \(\mathrm{rightRail}(i) \mapsto ((\mathrm{true}, i), (\mathrm{true}, i+1))\).

The ladder graph on \(n\) rungs as a simple graph on vertex set \(\mathrm{Bool} \times \mathrm{Fin}(n)\), with adjacency given by \(\mathrm{ladderAdj}\).

The ladder graph on \(n \geq 2\) rungs, built as a \(\mathrm{GraphWithCycles}\) instance to connect to the gauging framework (Gauss’s law operators from Def 2, flux operators from Def 3). The graph is the ladder graph, with edge endpoints and cycle structure as defined above.

Relaxed expansion: the condition \(|\partial S| \geq |S|\) is required only for subsets \(S \subseteq V\) satisfying \(0 {\lt} |S|\), \(2|S| \leq |V|\), and \((S \cap \mathrm{logicalSupport}) \neq \emptyset \). Formally,

A layer bound for a graph \(G\) with cycle-degree bound \(c\) consists of:

• a number of layers \(R \in \mathbb {N}\),

• a proof that a valid cycle-layer assignment exists with \(R\) layers and cycle-degree bound \(c\).

This represents the value \(R_G^c\) from the paper.

A layered vertex in a graph with \(R+1\) layers is a pair \((i, v)\) where \(i \in \{ 0, 1, \ldots , R\} \) is the layer index and \(v \in V\) is the original vertex. Layer \(0\) contains the original vertices; layers \(1, \ldots , R\) contain dummy copies.

Formally, given a type \(V\) and a natural number \(R\), a layered vertex is a structure consisting of:

• a layer index \(\mathrm{layer} \in \mathrm{Fin}(R+1)\),

• an original vertex \(\mathrm{vertex} \in V\).

The embedding of a vertex \(v \in V\) into layer \(i\) is defined by \(\mathrm{inLayer}(i, v) = (i, v)\).

A layered vertex \(\ell v\) is dummy if its layer index is nonzero, i.e., \(\ell v.\mathrm{layer} \neq 0\).

A layered vertex \(\ell v\) is original if its layer index equals \(0\), i.e., \(\ell v.\mathrm{layer} = 0\).

The embedding of an original vertex \(v \in V\) into layer \(0\) of the layered graph is defined by \(\mathrm{ofOriginal}(v) = (0, v)\).

An LDPCProperty consists of a maximum degree bound \(\mathtt{maxDegree} {\gt} 0\), expressing that each vertex participates in at most \(\mathtt{maxDegree}\) edges.

Alogical effect predicate \(\ell \) is group-like if:

1. The identity preserves logical info: \(\neg \ell (1)\).

2. Closure under multiplication: for all \(f, g\), if \(\neg \ell (f)\) and \(\neg \ell (g)\), then \(\neg \ell (f \cdot g)\).

3. Closure under inverse: for all \(f\), if \(\neg \ell (f)\), then \(\neg \ell (f^{-1})\).

Given a detector collection \(\mathit{DC}\), base outcomes, a logical effect predicate, and a set of time steps \(\mathit{times}\), the set of logical fault weights is

A logical operator for a stabilizer code \(C\) is a structure consisting of:

• an underlying Pauli operator \(\texttt{op} : \texttt{PauliOp}(C.n)\),

• a proof that \(\texttt{op}\) commutes with all stabilizers,

• a proof that \(\texttt{op}\) is not in the stabilizer group.

The support of a logical operator \(L\) is \(\operatorname {supp}(L) := \operatorname {supp}(L.\texttt{op})\).

The \(X\)-type support of a logical operator \(L\) is \(\operatorname {xSupp}(L) := \operatorname {xSupp}(L.\texttt{op})\).

The \(Z\)-type support of a logical operator \(L\) is \(\operatorname {zSupp}(L) := \operatorname {zSupp}(L.\texttt{op})\).

Desideratum 3: Low-Weight Cycles Property.

Let \(G\) be a graph with a chosen collection of cycles (a \(\mathrm{GraphWithCycles}\) structure over vertex type \(V\), edge type \(E\), and cycle type \(C\)), and let \(w \in \mathbb {N}\) be a constant weight bound.

The low-weight cycles property \(\mathrm{LowWeightCycles}(G, w)\) holds if every cycle \(c \in C\) has at most \(w\) edges:

This ensures that the \(B_p\) flux operators \(B_p = \prod _{e \in p} Z_e\) have bounded weight.

The maximum cycle degree over all edges is:

For an LDPC graph with \(W\) vertices and maximum degree \(d\), the number of edges is at most:

The difficulty of measuring a check operator of weight \(w\) is modeled as \(w^2\) (quadratic in weight).

A measurement event for measurement type \(M\) consists of:

• A measurement index \(\mathrm{measurement} : M\),

• A time step \(\mathrm{time} : \mathrm{TimeStep}\).

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 outcome is an element of \(\mathbb {Z}/2\mathbb {Z}\), where \(0\) represents the \(+1\) outcome and \(1\) represents the \(-1\) outcome.

Convert from \(\mathrm{Bool}\): \(\mathrm{false} \mapsto +1\) (i.e., \(0\)), \(\mathrm{true} \mapsto -1\) (i.e., \(1\)).

The \(-1\) outcome (error detected), defined as \(1 \in \mathbb {Z}/2\mathbb {Z}\).

The \(+1\) outcome (no error detected), defined as \(0 \in \mathbb {Z}/2\mathbb {Z}\).

The product of two measurement outcomes is their addition modulo \(2\):

Convert to \(\mathrm{Bool}\): \(0 \mapsto \mathrm{false}\) (\(+1\)), \(1 \mapsto \mathrm{true}\) (\(-1\)). Formally, \(\mathrm{toBool}(m) := (m \neq 0)\).

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\).

A measurement schedule has standard primary checks if both the Gauss law frequency and the deformed check frequency are set to everyRound.

The set of measurement time steps in a range \([t_1 + \tfrac {1}{2}, t_2 - \tfrac {1}{2}]\):

The integer time immediately after measurement time \(t + \tfrac {1}{2}\) is \(t + 1\).

The integer time immediately before measurement time \(t + \tfrac {1}{2}\) is \(t\).

Converts a measurement time step \(t\) (representing \(t + \tfrac {1}{2}\)) to the half-integer time \(\mathtt{halfInteger}(t)\).

A mid-computation context where the position is middle, surrounding EC is present, and the given number of surrounding EC rounds is recorded.

For a real number \(h_G\), define \(\min (h_G, 1)\).

Given a simple graph \(G = (V,E)\), the default gauging circuit \(\mathrm{mkGaugingCircuit}(G)\) is the gauging circuit where:

• both entangling circuits use \(\mathrm{CX}\) gates with \(\mathrm{control} = \mathrm{inl}(v)\) and \(\mathrm{target} = \mathrm{inr}(e)\) for each vertex-edge incidence pair,

• the \(X\)-measurement covers all vertices with \(\mathrm{keep} = \mathrm{true}\),

• the \(Z\)-measurement covers all edges of \(G\) with \(\mathrm{keep} = \mathrm{false}\).

All required conditions (identical entangling circuits, full coverage, keep/discard properties) hold by reflexivity.

The number of CX gates in one round of the entangling circuit for a graph \(G = (V,E)\) is

The original code distance structure captures:

1. A positive integer \(d {\gt} 0\) (the distance).

2. A predicate \(\mathrm{isLogical}\) identifying logical operators of the original code.

3. The distance property: for every nontrivial logical operator \(\mathrm{op}\),

   \[ \mathrm{op}.\mathrm{weight} \; \ge \; d. \]

A vertex-only Pauli operator on the original code (before deformation) is a pair \((S_X, S_Z)\) where \(S_X, S_Z \subseteq V\) are the \(X\)- and \(Z\)-supports on vertex qubits.

An original code operator is nontrivial if \((S_X \cup S_Z) \neq \emptyset \).