32 Lem 5: Spacetime Stabilizers
The local spacetime stabilizers of the fault-tolerant gauging measurement procedure (Definition 10) are generated by specific fault patterns, organized by time phase. A spacetime stabilizer is a syndrome-free fault pattern that does not affect the logical outcome (Definition 11). Each generator consists of space-faults (Pauli errors at specific times) together with measurement faults on anticommuting checks that cancel the resulting detector violations.
Part I: Generator Predicates
Generators are classified by their fault structure: which space-faults (Pauli errors) and which time-faults (measurement errors) they contain. Space stabilizers have no measurement faults; time-propagating and boundary generators include measurement faults on anticommuting checks that cancel detector violations.
A space-only stabilizer generator is a structure \((\mathsf{IsSpaceStabilizerGen}\ \mathrm{proc}\ P\ t\ F)\) asserting that a spacetime fault \(F\) consists of a single check operator \(P\) applied as an error at time \(t\), with no measurement faults. Formally:
\(F.\mathrm{timeFaults} = \emptyset \),
\(F.\mathrm{pauliErrorAt}(t) = P\),
For all \(t' \neq t\), \(F.\mathrm{spaceFaultsAt}(t') = \emptyset \).
This is used for: original checks \(s_j\), deformed checks \(\tilde{s}_j / A_v / B_p\), and \(Z_e\) at initialization or readout times.
A time-propagating generator is a structure \((\mathsf{IsTimePropagatingGen}\ \mathrm{proc}\ P\ t\ F)\) asserting that \(F\) has Pauli error \(P\) at times \(t\) and \(t+1\), together with measurement faults on all checks that anticommute with \(P\) at time \(t + \tfrac {1}{2}\). Formally:
\(F.\mathrm{pauliErrorAt}(t) = P\),
\(F.\mathrm{pauliErrorAt}(t+1) = P\),
For all \(t' \neq t\) and \(t' \neq t+1\), \(F.\mathrm{spaceFaultsAt}(t') = \emptyset \),
\(F\) is syndrome-free for the gauging procedure.
The measurement faults ensure syndrome-freeness: each detector spanning time \(t + \tfrac {1}{2}\) has two violations (one from the Pauli error, one from the measurement fault) that cancel via \((-1) \times (-1) = +1\). The net Pauli effect is \(P \cdot P = I\), so the logical outcome is preserved.
An initialization fault \(+ X_e\) generator is a structure \((\mathsf{IsInitXeGen}\ \mathrm{proc}\ e\ F)\) for an edge \(e\) and spacetime fault \(F\), consisting of a \(|0\rangle _e\) initialization fault at time \(t_i - \tfrac {1}{2}\) paired with an \(X_e\) Pauli fault at the gauging start time \(t_i\). Formally:
\(F.\mathrm{timeFaults} = \{ \langle \mathrm{edgeInit}\ e \rangle \} \),
\(F.\mathrm{pauliErrorAt}(\mathrm{phase2Start}) = X_e\),
For all \(t' \neq \mathrm{phase2Start}\), \(F.\mathrm{spaceFaultsAt}(t') = \emptyset \).
Together, the initialization fault and \(X_e\) cancel in every detector involving edge \(e\).
A \(Z_e + A_v\) measurement fault generator is a structure \((\mathsf{IsZeAvMeasGen}\ \mathrm{proc}\ e\ t\ r\ F)\) for an edge \(e\), time \(t\), and round \(r\). It consists of Pauli \(Z_e\) at time \(t\) together with \(A_v\) measurement faults for both endpoints \(v \in e\) at measurement round \(r\). Formally:
\(F.\mathrm{pauliErrorAt}(t) = Z_e\),
For all \(t' \neq t\), \(F.\mathrm{spaceFaultsAt}(t') = \emptyset \),
\(F.\mathrm{timeFaults}\) equals the image of the set of vertices \(v \in e\) under the map \(v \mapsto \langle \mathrm{phase2}\ (\mathrm{gaussLaw}\ v\ r) \rangle \).
Since \(Z_e\) anticommutes with \(A_v\) for exactly the two endpoints \(v \in e\), the measurement faults cancel the two detector violations.
A readout \(X_e\) generator is a structure \((\mathsf{IsReadoutXeGen}\ \mathrm{proc}\ e\ F)\) for an edge \(e\) and spacetime fault \(F\), consisting of Pauli \(X_e\) at ungauging time \(t_o\) paired with a \(Z_e\) readout measurement fault at \(t_o + \tfrac {1}{2}\). Formally:
\(F.\mathrm{timeFaults} = \{ \langle \mathrm{phase3}\ (\mathrm{edgeZ}\ e) \rangle \} \),
\(F.\mathrm{pauliErrorAt}(\mathrm{phase3Start}) = X_e\),
For all \(t' \neq \mathrm{phase3Start}\), \(F.\mathrm{spaceFaultsAt}(t') = \emptyset \).
The \(X_e\) flips the \(Z_e\) eigenvalue, and the \(Z_e\) readout measurement fault compensates, so the correct \(Z_e\) value is effectively recorded.
Part II: Model-Theoretic Foundation
Any fault with empty time-faults is trivially syndrome-free and preserves the gauging sign.
Any spacetime fault \(F\) with \(F.\mathrm{timeFaults} = \emptyset \) is syndrome-free for the gauging procedure.
We unfold the definition of \(\mathsf{IsSyndromeFreeGauging}\). Let \(\mathrm{idx}\) be an arbitrary detector index. Rewriting using the hypothesis that \(F.\mathrm{timeFaults} = \emptyset \), the result follows directly from the fact that no detector is violated when there are no faults.
Any spacetime fault \(F\) with \(F.\mathrm{timeFaults} = \emptyset \) preserves the gauging sign.
We unfold the definitions of \(\mathsf{PreservesGaugingSign}\) and \(\mathsf{gaussSignFlip}\). The outer sum over vertices \(v\) equals zero because for each \(v\), the inner sum over rounds \(r\) equals zero. Each term in the inner sum vanishes by simplification using the hypothesis \(F.\mathrm{timeFaults} = \emptyset \).
Any spacetime fault \(F\) with \(F.\mathrm{timeFaults} = \emptyset \) is a gauging stabilizer.
The gauging stabilizer condition is the conjunction of syndrome-freeness and gauging sign preservation. Both follow from the preceding lemmas applied to the hypothesis \(F.\mathrm{timeFaults} = \emptyset \).
Part III: Algebraic Classification
These are the key algebraic ingredients determining which measurement faults must accompany each space-fault to maintain syndrome-freeness.
All deformed code checks are self-inverse: for any check index \(\mathrm{ci}\),
This follows directly from the \(\mathsf{allChecks\_ self\_ inverse}\) property of deformed code checks.
For any original check index \(j\), the check operator satisfies \(\mathrm{checks}(j) \cdot \mathrm{checks}(j) = 1\).
This follows directly from the Pauli operator self-inverse property \(P \cdot P = 1\).
Any Pauli operator \(P\) is self-inverse: \(P \cdot P = 1\).
This follows directly from \(\mathsf{PauliOp.mul\_ self}\).
All deformed code checks pairwise commute: for any check indices \(\mathrm{ci}\) and \(\mathrm{cj}\),
This follows from the \(\mathsf{allChecks\_ commute}\) property, which uses the cycle parity data and the commutativity of the original checks.
For any original check indices \(i\) and \(j\), \(\mathrm{PauliCommute}(\mathrm{checks}(i),\; \mathrm{checks}(j))\).
This follows directly from the stabilizer code assumption \(\mathrm{proc.checks\_ commute}\).
\(Z_e\) Commutation Properties
For any edge \(e\) and cycle \(p\), \(Z_e\) commutes with the flux check \(B_p\). Both operators are pure \(Z\)-type.
We unfold \(\mathsf{PauliCommute}\) and \(\mathsf{symplecticInner}\) and show the sum equals zero. For each qubit \(q\), we case-split: if \(q = \mathrm{inl}(w)\) for some vertex \(w\), the term vanishes by properties of \(\mathsf{pauliZ}\); if \(q = \mathrm{inr}(e')\) for some edge \(e'\), the term vanishes because the \(x\)-component of \(\mathsf{pauliZ}\) is zero and the \(x\)-component of the flux operator is zero, so both products are zero.
For any edge \(e\) and original check index \(j\), \(Z_e\) commutes with the deformed original check \(\tilde{s}_j\). This holds because deformed checks have no \(X\)-support on edges.
We unfold \(\mathsf{PauliCommute}\) and \(\mathsf{symplecticInner}\) and show the sum equals zero. For each qubit \(q\), we case-split: if \(q = \mathrm{inl}(w)\), the term vanishes by properties of \(\mathsf{pauliZ}\). If \(q = \mathrm{inr}(e')\), we use the fact that the deformed original check has no \(X\)-support on edges, i.e., \((\tilde{s}_j).\mathrm{xVec}(\mathrm{inr}(e')) = 0\). Simplifying with \(\mathsf{pauliZ}\) having zero \(x\)-component and applying the single-apply rule, the term vanishes in both sub-cases (whether \(e' = e\) or not).
For an edge \(e\) and vertex \(v\) with \(v \notin e\), \(Z_e\) commutes with the Gauss law check \(A_v\).
We unfold \(\mathsf{PauliCommute}\) and \(\mathsf{symplecticInner}\) and show the sum equals zero. For each qubit \(q\): if \(q = \mathrm{inl}(w)\), the term vanishes by \(\mathsf{pauliZ}\) properties. If \(q = \mathrm{inr}(e')\), the \(x\)-component of \(\mathsf{pauliZ}\) is zero, so we simplify and apply the single-apply rule. In the case \(e' = e\), we use the hypothesis \(v \notin e\) to show the Gauss law operator’s \(x\)-component at edge \(e\) is zero. Otherwise the indicator function vanishes. In both cases the term is zero.
For an edge \(e\) and vertex \(v\) with \(v \in e\), \(Z_e\) anticommutes with the Gauss law check \(A_v\):
We unfold \(\mathsf{PauliCommute}\) and \(\mathsf{symplecticInner}\) and assume for contradiction that the symplectic inner product is \(0\). We show the key identity: for each qubit \(q\), the symplectic inner product term equals \((\mathrm{gaussLawOp}\ G\ v).\mathrm{xVec}(\mathrm{inr}(e))\) if \(q = \mathrm{inr}(e)\), and \(0\) otherwise. This is established by case-splitting on \(q\): vertex qubits contribute zero by \(\mathsf{pauliZ}\) properties, and for edge qubits \(\mathrm{inr}(e')\), we simplify the \(\mathsf{pauliZ}\) terms and apply the indicator function, which is nonzero only when \(e' = e\).
Summing using \(\mathsf{Finset.sum\_ ite\_ eq'}\), we obtain the total as \((\mathrm{gaussLawOp}\ G\ v).\mathrm{xVec}(\mathrm{inr}(e))\). Since \(v \in e\), this equals \(1\). Substituting into the commutativity hypothesis and rewriting, we obtain \(1 = 0\), a contradiction.
For any edge \(e\) and vertex \(v\):
We prove both directions. For the forward direction, we assume \(\mathrm{PauliCommute}(Z_e, A_v)\) and \(v \in e\), and derive a contradiction using the anticommutativity lemma. For the reverse direction, we assume \(v \notin e\) and apply the commutativity lemma for non-member vertices.
\(X_e\) Commutation Properties
For any edge \(e\) and vertex \(v\), \(X_e\) commutes with the Gauss law check \(A_v\). Both are pure \(X\)-type.
We unfold \(\mathsf{PauliCommute}\) and \(\mathsf{symplecticInner}\) and show the sum equals zero. For each qubit \(q\), the term vanishes by simplification using the properties of \(\mathsf{pauliX}\) and \(\mathsf{gaussLawOp}\), case-splitting on whether \(q\) is a vertex or edge qubit.
For any edge \(e\), \(X_e\) anticommutes with \(Z_e\):
We unfold \(\mathsf{PauliCommute}\) and \(\mathsf{symplecticInner}\) and assume for contradiction that the symplectic inner product is \(0\). For each qubit \(q\), we show the symplectic inner product term equals \(1\) if \(q = \mathrm{inr}(e)\) and \(0\) otherwise, by simplifying the \(\mathsf{pauliX}\) and \(\mathsf{pauliZ}\) components and applying the indicator function. Summing using \(\mathsf{Finset.sum\_ ite\_ eq'}\), we obtain the total as \(1 \in \mathbb {Z}/2\mathbb {Z}\). Rewriting in the commutativity hypothesis, we get \(1 = 0\), a contradiction.
Vertex Pauli Commutation Properties
For any vertices \(v\) and \(w\), \(X_v\) commutes with the Gauss law check \(A_w\). Both are pure \(X\)-type.
We unfold \(\mathsf{PauliCommute}\) and \(\mathsf{symplecticInner}\) and show the sum equals zero. Each term vanishes by simplification using the properties of \(\mathsf{pauliX}\) and \(\mathsf{gaussLawOp}\).
For any vertex \(v\) and cycle \(p\), \(X_v\) commutes with the flux check \(B_p\).
We unfold \(\mathsf{PauliCommute}\) and \(\mathsf{symplecticInner}\) and show the sum equals zero. For each qubit \(q\), we simplify using \(\mathsf{pauliX}\) and \(\mathsf{fluxOp}\) properties, case-splitting on vertex vs. edge qubits. Each term vanishes.
For any vertex \(v\), \(Z_v\) anticommutes with the Gauss law check \(A_v\):
We unfold \(\mathsf{PauliCommute}\) and \(\mathsf{symplecticInner}\) and assume for contradiction that the symplectic inner product is \(0\). For each qubit \(q\), we show the term equals \(1\) if \(q = \mathrm{inl}(v)\) and \(0\) otherwise. For vertex qubits \(\mathrm{inl}(w)\), we simplify \(\mathsf{pauliZ}\) and apply the indicator function: when \(w = v\), the Gauss law operator’s \(x\)-component at vertex \(v\) is \(1\). For edge qubits, the term vanishes. Summing via \(\mathsf{Finset.sum\_ ite\_ eq'}\), the total is \(1\). Substituting into the hypothesis gives \(1 = 0\), a contradiction.
For vertices \(v \neq w\), \(Z_v\) commutes with the Gauss law check \(A_w\).
We unfold \(\mathsf{PauliCommute}\) and \(\mathsf{symplecticInner}\) and show the sum equals zero. For each qubit \(q\): if \(q = \mathrm{inl}(u)\) for some vertex \(u\), we simplify \(\mathsf{pauliZ}\) and apply the indicator function. When \(u = v\), the Gauss law operator at \(w\) evaluated at vertex \(v\) gives \(0\) because \(v \neq w\). Otherwise the indicator vanishes. If \(q = \mathrm{inr}(\cdot )\), the term vanishes by \(\mathsf{pauliZ}\) and \(\mathsf{gaussLawOp}\) properties.
For any vertex \(v\) and cycle \(p\), \(Z_v\) commutes with the flux check \(B_p\).
We unfold \(\mathsf{PauliCommute}\) and \(\mathsf{symplecticInner}\) and show the sum equals zero. For each qubit \(q\), we simplify using \(\mathsf{pauliZ}\) and \(\mathsf{fluxOp}\) properties, case-splitting on vertex vs. edge qubits. Each term vanishes.
Edge Endpoints
For any edge \(e\) in the graph \(G\), the set of vertices \(v\) with \(v \in e\) has cardinality exactly \(2\):
We destructure the edge \(e\) and proceed by induction on its \(\mathrm{Sym2}\) representation \(\{ a, b\} \). Since \(G\) is loopless, \(a \neq b\). The filter set \(\{ v \mid v = a \lor v = b\} \) equals the pair \(\{ a, b\} \) by extensionality. The cardinality of a two-element set with distinct elements is \(2\).
\(Z_e\) anticommutes with exactly \(2\) Gauss law checks (those at the endpoints of \(e\)):
We show that the set of vertices \(v\) such that \(\neg \, \mathrm{PauliCommute}(Z_e, A_v)\) equals the set of vertices \(v \in e\). This follows by extensionality using the \(Z_e\)–\(A_v\) commutation characterization: \(\mathrm{PauliCommute}(Z_e, A_v) \iff v \notin e\), so \(\neg \, \mathrm{PauliCommute}(Z_e, A_v) \iff v \in e\). Rewriting, the cardinality equals \(2\) by the edge endpoint count lemma.
\(Z_e\) Non-Gauss Commutation
For any edge \(e\) and check index \(\mathrm{ci}\) that is not a Gauss law check (i.e., \(\mathrm{ci} \neq \mathrm{gaussLaw}(v)\) for all \(v\)), \(Z_e\) commutes with \(\mathrm{allChecks}(\mathrm{ci})\).
We case-split on the check index \(\mathrm{ci}\):
If \(\mathrm{ci} = \mathrm{gaussLaw}(v)\) for some \(v\), this contradicts the hypothesis \(\mathrm{ci} \neq \mathrm{gaussLaw}(v)\).
If \(\mathrm{ci} = \mathrm{flux}(p)\), the check is a flux check \(B_p\), and \(Z_e\) commutes with it by the \(Z_e\)–flux commutation lemma.
If \(\mathrm{ci} = \mathrm{deformed}(j)\), the check is a deformed original check \(\tilde{s}_j\), and \(Z_e\) commutes with it by the \(Z_e\)–deformed commutation lemma.
Part IV: Generator Stabilizer Proofs
Space stabilizers (with empty time-faults) are proved directly. Generators with non-empty time-faults require showing that measurement faults cancel detector violations; this is axiomatized since the detector cancellation argument requires reasoning about specific detector measurement membership.
If \(F\) is a space stabilizer generator (i.e., \(\mathsf{IsSpaceStabilizerGen}\ \mathrm{proc}\ P\ t\ F\)), then \(F\) is a gauging stabilizer.
This follows directly from the gauging stabilizer property for faults with empty time-faults, since \(\mathsf{IsSpaceStabilizerGen}\) implies \(F.\mathrm{timeFaults} = \emptyset \).
red[UNPROVEN AXIOM]
If \(F\) is a time-propagating generator \((\mathsf{IsTimePropagatingGen}\ \mathrm{proc}\ P\ t\ F)\), then \(F\) is a gauging stabilizer. The proof requires showing that the measurement faults on anticommuting checks cancel all detector violations via the \((-1) \times (-1) = +1\) argument, and that the net Pauli effect \(P \cdot P = I\) preserves the logical outcome.
Note: This is stated as an axiom because the full proof was not completed in the formalization.
red[UNPROVEN AXIOM]
If \(F\) is an initialization \(X_e\) generator \((\mathsf{IsInitXeGen}\ \mathrm{proc}\ e\ F)\), then \(F\) is a gauging stabilizer. The \(|0\rangle _e\) initialization fault flips the init detector for edge \(e\); the \(X_e\) Pauli at \(t_i\) flips the same detector via the check measurement. These cancel: \((-1) \times (-1) = +1\).
Note: This is stated as an axiom because the full proof was not completed in the formalization.
red[UNPROVEN AXIOM]
If \(F\) is a \(Z_e + A_v\) measurement fault generator \((\mathsf{IsZeAvMeasGen}\ \mathrm{proc}\ e\ t\ r\ F)\), then \(F\) is a gauging stabilizer. \(Z_e\) anticommutes with \(A_v\) for both endpoints \(v \in e\); each \(A_v\) measurement fault cancels the corresponding detector violation: \((-1) \times (-1) = +1\) for each endpoint.
Note: This is stated as an axiom because the full proof was not completed in the formalization.
red[UNPROVEN AXIOM]
If \(F\) is a readout \(X_e\) generator \((\mathsf{IsReadoutXeGen}\ \mathrm{proc}\ e\ F)\), then \(F\) is a gauging stabilizer. \(X_e\) flips the \(Z_e\) eigenvalue; the \(Z_e\) readout fault compensates.
Note: This is stated as an axiom because the full proof was not completed in the formalization.
Part V: Listed Generator Classification
A spacetime fault \(F\) is a listed generator \((\mathsf{IsListedGenerator}\ \mathrm{proc}\ F)\) if it falls into one of the following categories, organized by time phase:
Phase 1 & 3 – Original check: \(F\) is a space stabilizer generator for an original check \(\tilde{s}_j\) at time \(t\) with \(t {\lt} t_i\) or \(t \geq t_o\).
Phase 1 & 3 – Time-propagating: \(F\) is a time-propagating generator with Pauli \(P\) at time \(t\) with \(t {\lt} t_i\) or \(t \geq t_o\).
Phase 2 – Deformed check: \(F\) is a space stabilizer generator for a deformed check \(\mathrm{allChecks}(\mathrm{ci})\) at time \(t\) with \(t_i {\lt} t {\lt} t_o\).
Phase 2 – Time-propagating \(X_v\): at time \(t\) with \(t_i \leq t {\lt} t_o\).
Phase 2 – Time-propagating \(Z_v\): at time \(t\) with \(t_i \leq t {\lt} t_o\).
Phase 2 – Time-propagating \(X_e\): at time \(t\) with \(t_i \leq t {\lt} t_o\).
Phase 2 – Time-propagating \(Z_e\): at time \(t\) with \(t_i \leq t {\lt} t_o\).
Gauging (\(t = t_i\)) – Original check \(s_j\): space stabilizer at \(t_i\).
Gauging (\(t = t_i\)) – \(Z_e\): space stabilizer at \(t_i\).
Gauging (\(t = t_i\)) – Init \(+ X_e\): initialization fault paired with \(X_e\).
Gauging (\(t = t_i\)) – \(Z_e + A_v\): \(Z_e\) at \(t_i + 1\) with \(A_v\) measurement faults.
Ungauging (\(t = t_o\)) – Deformed check: space stabilizer at \(t_o\).
Ungauging (\(t = t_o\)) – Readout \(X_e\): \(X_e\) paired with \(Z_e\) readout fault.
Ungauging (\(t = t_o\)) – Bare \(Z_e\): space stabilizer at \(t_o\).
Ungauging (\(t = t_o\)) – \(Z_e + A_v\): \(Z_e\) at \(t_o - 1\) with \(A_v\) measurement faults.
Ungauging (\(t = t_o\)) – Time-propagating: at the \(t_o\) boundary.
Part VI: Main Theorem
Every listed generator fault pattern \(F\) is a gauging stabilizer: it has empty syndrome and does not affect the logical outcome.
We case-split on the type of listed generator:
origCheck: \(F\) is a space stabilizer generator for an original check. By the space stabilizer lemma, \(F\) is a gauging stabilizer.
origTimeProp: \(F\) is a time-propagating generator in Phase 1 or 3. By the time-propagating axiom, \(F\) is a gauging stabilizer.
deformedCheck: \(F\) is a space stabilizer generator for a deformed check. By the space stabilizer lemma, \(F\) is a gauging stabilizer.
deformedTimePropXv, deformedTimePropZv, deformedTimePropXe, deformedTimePropZe: Each is a time-propagating generator in Phase 2. By the time-propagating axiom, each is a gauging stabilizer.
gaugingSj, gaugingZe: Space stabilizer generators at the gauging time \(t_i\). By the space stabilizer lemma, each is a gauging stabilizer.
gaugingInitXe: An init \(X_e\) generator. By the init \(X_e\) axiom, \(F\) is a gauging stabilizer.
gaugingZeAv: A \(Z_e + A_v\) measurement fault generator. By the \(Z_e + A_v\) axiom, \(F\) is a gauging stabilizer.
ungaugingCheck: A space stabilizer generator at \(t_o\). By the space stabilizer lemma, \(F\) is a gauging stabilizer.
ungaugingReadoutXe: A readout \(X_e\) generator. By the readout \(X_e\) axiom, \(F\) is a gauging stabilizer.
ungaugingBareZe: A space stabilizer generator at \(t_o\). By the space stabilizer lemma, \(F\) is a gauging stabilizer.
ungaugingZeAv: A \(Z_e + A_v\) generator at \(t_o - 1\). By the \(Z_e + A_v\) axiom, \(F\) is a gauging stabilizer.
ungaugingTimeProp: A time-propagating generator at the \(t_o\) boundary. By the time-propagating axiom, \(F\) is a gauging stabilizer.
Part VII: Algebraic Justifications
The algebraic structure underlying the spacetime stabilizer classification consists of the following eleven properties:
Original checks are self-inverse: \(\forall j,\; \mathrm{checks}(j) \cdot \mathrm{checks}(j) = 1\).
Original checks pairwise commute: \(\forall i,j,\; \mathrm{PauliCommute}(\mathrm{checks}(i), \mathrm{checks}(j))\).
Deformed checks are self-inverse: \(\forall \mathrm{ci},\; \mathrm{allChecks}(\mathrm{ci})^2 = 1\).
Deformed checks pairwise commute: \(\forall \mathrm{ci}, \mathrm{cj},\; \mathrm{PauliCommute}(\mathrm{allChecks}(\mathrm{ci}), \mathrm{allChecks}(\mathrm{cj}))\).
\(Z_e\)–\(A_v\) commutation characterization: \(\mathrm{PauliCommute}(Z_e, A_v) \iff v \notin e\).
\(Z_e\) anticommutes with exactly \(2\) Gauss law checks: \(|\{ v \mid v \in e\} | = 2\).
\(Z_e\) commutes with all non-Gauss deformed checks.
\(X_e\) anticommutes with \(Z_e\) (init/readout generator structure).
\(X_e\) commutes with all Gauss law checks.
Any Pauli is self-inverse: \(P \cdot P = 1\).
Composition uses symmetric difference on time-faults (\(\mathbb {Z}_2\) group closure).
The proof constructs the eleven-fold conjunction directly:
By \(\mathsf{PauliOp.mul\_ self}\).
By \(\mathrm{proc.checks\_ commute}\).
By \(\mathsf{allChecks\_ self\_ inverse}\).
By \(\mathsf{allChecks\_ commute}\) using cycle parity and original check commutativity.
By the \(Z_e\)–\(A_v\) commutation characterization lemma.
By the edge endpoint count lemma.
By the \(Z_e\) non-Gauss commutation lemma.
By the \(X_e\)–\(Z_e\) anticommutativity lemma.
By the \(X_e\)–Gauss law commutativity lemma.
By \(\mathsf{PauliOp.mul\_ self}\).
By reflexivity (the composition is definitionally symmetric difference on time-faults).
Part VIII: Completeness
red[UNPROVEN AXIOM]
Every gauging stabilizer decomposes as a \(\mathbb {Z}_2\) composition (symmetric difference) of the listed generators. Formally, if \(F\) is a gauging stabilizer, then there exists a list \(\mathrm{gens}\) of spacetime faults such that:
Every \(g \in \mathrm{gens}\) satisfies \(\mathsf{IsListedGenerator}(\mathrm{proc}, g)\), and
\(F = \mathrm{gens.foldl}(\mathsf{compose},\; \mathsf{empty})\).
The proof uses time-ordered decomposition: peel off generators at the earliest active time, proceed inductively, until only measurement faults remain, which must decompose into detector measurement sets.
Note: This is stated as an axiom because the full proof was not completed in the formalization.
Part IX: Corollaries
For any edge \(e\) and original check index \(j\), \(Z_e\) commutes with the original check \(\tilde{s}_j\) lifted to \(V \oplus E\).
This follows directly from the \(Z_e\)–deformed check commutation lemma.
Part X: Space-Fault Cleaning and Centralizer Properties
red[UNPROVEN AXIOM]
For any syndrome-free spacetime fault \(F\), there exists a stabilizer \(S_1\) such that:
\(S_1\) is syndrome-free for the gauging procedure,
\(S_1\) preserves the gauging sign,
\(S_1.\mathrm{pauliErrorAt}(t_i)\) is in the stabilizer group of the deformed code, and
For all \(t \neq t_i\), \((F \circ S_1).\mathrm{spaceFaultsAt}(t) = \emptyset \).
The construction uses time-propagating generators to move all space-faults to the gauging time \(t_i\). Boundary initialization/readout faults are absorbed using init-\(X_e\) and readout-\(X_e\) generators. The composed generators cancel intermediate Paulis (\(P \cdot P = 1\)), leaving only the net effect at \(t_i\), which is a product of check operators and hence in the stabilizer group.
Note: This is stated as an axiom because the full proof was not completed in the formalization.
red[UNPROVEN AXIOM]
A pure-space fault \(F\) concentrated at the gauging time \(t_i\) (i.e., \(F.\mathrm{spaceFaultsAt}(t) = \emptyset \) for all \(t \neq t_i\) and \(F.\mathrm{isPureSpace}\)), if syndrome-free for the gauging procedure, has its Pauli error \(F.\mathrm{pauliErrorAt}(t_i)\) in the centralizer of the deformed code.
This encodes the fact that during Phase 2, the active checks are the deformed code checks \((A_v, B_p, \tilde{s}_j)\), and the time-propagating generators commute with all active checks away from their support. The cleaning process preserves the commutation structure, so the concentrated Pauli at \(t_i\) commutes with every deformed code check.
Note: This is stated as an axiom because the full proof was not completed in the formalization.