Lemma 5: Spacetime Stabilizers #
Statement #
The local spacetime stabilizers of the fault-tolerant gauging measurement procedure (Def 10) are generated by the following fault patterns, organized by time phase. A spacetime stabilizer is a syndrome-free fault pattern that does not affect the logical outcome (Def 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.
Main Results #
- Generator predicates:
IsSpaceStabilizerGen,IsTimePropagatingGen,IsInitXeGen,IsZeAvMeasGen,IsReadoutXeGen IsListedGenerator: inductive classifying all generator types by phaselistedGenerator_isGaugingStabilizer: every listed generator is a gauging stabilizerspacetimeStabilizer_completeness: every gauging stabilizer decomposes into generators
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: a single check operator P applied as an error at time t. No measurement faults needed because P commutes with all checks being measured. Used for: original check s_j, deformed checks s̃_j/A_v/B_p, Z_e at t_i or t_o.
- no_other_faults (t' : ℕ) : t' ≠ t → F.spaceFaultsAt t' = ∅
Instances For
A time-propagating generator: Pauli P at times t and t+1, together with measurement faults on all checks that anticommute with P at time t+½.
The measurement faults ensure syndrome-freeness: each detector spanning t+½ has two violations (one from the Pauli error affecting the check outcome, one from the explicit measurement fault) that cancel: (-1)×(-1) = +1.
The net Pauli effect is P·P = I (identity), so the logical outcome is preserved.
- syndrome_free : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F
The measurement faults cancel all detector violations from the space-faults. This is the (-1)×(-1)=+1 cancellation argument from the proof.
Instances For
Initialization fault + X_e generator at gauging time t_i (generator 5 at t = t_i). A |0⟩_e initialization fault at t_i-½ paired with X_e Pauli fault at t_i. The init fault is modeled as a time-fault on the edgeInit measurement label; together with X_e at t_i, they cancel in every detector involving edge e.
- no_other_space (t' : ℕ) : t' ≠ proc.phase2Start → F.spaceFaultsAt t' = ∅
Instances For
Z_e + A_v measurement fault generator (generator 6 at t = t_i and t = t_o). Pauli Z_e at time t, together with A_v measurement faults for both endpoints v ∈ e at the intermediate measurement round r. Z_e anticommutes with A_v for v ∈ e (exactly 2 endpoints); the measurement faults cancel the two detector violations.
- no_other_space (t' : ℕ) : t' ≠ t → F.spaceFaultsAt t' = ∅
- timeFaults_eq : F.timeFaults = Finset.image (fun (v : V) => { measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r) }) {v : V | v ∈ ↑e}
The timeFaults are exactly the A_v measurement faults for the two endpoints of e.
Instances For
X_e + Z_e readout fault generator at ungauging time t_o (generator 4 at t = t_o). Pauli X_e at time t_o flips the Z_e eigenvalue; the Z_e readout measurement fault at t_o+½ compensates, so the correct Z_e value is effectively recorded.
- timeFaults_eq : F.timeFaults = {{ measurement := FTGaugingMeasurement.phase3 (PostDeformationMeasurement.edgeZ e) }}
- no_other_space (t' : ℕ) : t' ≠ proc.phase3Start → F.spaceFaultsAt t' = ∅
Instances For
Part II: Model-Theoretic Foundation #
Any fault with empty timeFaults is trivially syndrome-free (no detectors are violated)
and preserves the gauging sign (no Gauss law measurement faults).
Any fault with empty timeFaults is syndrome-free.
Any fault with empty timeFaults preserves the gauging sign.
Any fault with empty timeFaults is a gauging stabilizer.
Part III: Algebraic Classification #
These are the key algebraic ingredients used in the proof. They determine which measurement faults must accompany each space-fault to maintain syndrome-freeness.
Self-Inverse Properties #
All deformed code checks are self-inverse: s̃_j * s̃_j = 1, A_v * A_v = 1, B_p * B_p = 1.
Original checks are self-inverse: s_j * s_j = 1.
Pairwise Commutation #
All deformed code checks pairwise commute (from Lem 1).
Original checks pairwise commute (by stabilizer code assumption).
Z_e Commutation Properties #
Z_e commutes with flux checks (both pure Z-type).
Z_e commutes with deformed checks (no X-support on edges).
Z_e commutes with A_v when v ∉ e.
Z_e anticommutes with A_v when v ∈ e.
Z_e commutes with A_v iff v ∉ e.
X_e Commutation Properties #
X_e commutes with Gauss law checks (both pure X type).
X_e anticommutes with pauliZ on same edge.
Vertex Pauli Commutation Properties #
X_v commutes with all gaussLaw checks (both pure X type).
X_v commutes with flux checks.
Z_v anticommutes with A_v.
Z_v commutes with A_w for w ≠ v.
Z_v commutes with flux checks.
Edge Endpoints #
For an edge e, the vertices v ∈ e number exactly 2.
Z_e anticommutes with exactly 2 Gauss law checks (those at endpoints of e).
Z_e Non-Gauss Commutation #
Z_e commutes with all non-Gauss deformed checks (B_p, s̃_j).
Part IV: Generator Stabilizer Proofs #
Space stabilizers (timeFaults = ∅) are proved directly. Generators with non-empty timeFaults require showing that measurement faults cancel detector violations — this is axiomatized since the detector cancellation argument requires reasoning about specific detector measurement membership.
Space stabilizer generators are gauging stabilizers (timeFaults = ∅).
Time-propagating generators are gauging stabilizers. The proof requires showing that the measurement faults on anticommuting checks cancel all detector violations ((-1)×(-1)=+1 argument) and that the net Pauli effect P·P = I preserves the logical outcome.
Init fault + X_e generator is a gauging stabilizer. The |0⟩_e init 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)×(-1)=+1.
Z_e + A_v measurement fault generator is a gauging stabilizer. Z_e anticommutes with A_v for both endpoints v ∈ e; each A_v measurement fault cancels the corresponding detector violation: (-1)×(-1)=+1 for each endpoint.
X_e + Z_e readout fault generator is a gauging stabilizer. X_e flips the Z_e eigenvalue; the Z_e readout fault compensates.
Part V: Listed Generator Classification #
An inductive predicate classifying all generator types from the original statement, organized by the 4 time phases with appropriate time constraints.
A fault pattern F is one of the listed generators from Lemma 5. Each constructor corresponds to a specific generator type at a specific phase.
- origCheck
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(j : J)
(t : ℕ)
(hphase : t < proc.phase2Start ∨ t ≥ proc.phase3Start)
(hgen : IsSpaceStabilizerGen proc (DeformedCode.deformedOriginalChecks G checks proc.deformedData j) t F)
: IsListedGenerator proc F
Phase 1&3: Original check s_j at time t (t < t_i or t > t_o).
- origTimeProp
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(P : PauliOp (GaussFlux.ExtQubit G))
(t : ℕ)
(hphase : t < proc.phase2Start ∨ t ≥ proc.phase3Start)
(hgen : IsTimePropagatingGen proc P t F)
: IsListedGenerator proc F
Phase 1&3: Time-propagating Pauli pair at t, t+1 with measurement faults on anticommuting original checks at t+½ (t < t_i or t ≥ t_o).
- deformedCheck
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(ci : DeformedCode.CheckIndex V C J)
(t : ℕ)
(hlo : proc.phase2Start < t)
(hhi : t < proc.phase3Start)
(hgen : IsSpaceStabilizerGen proc (DeformedCode.allChecks G cycles checks proc.deformedData ci) t F)
: IsListedGenerator proc F
Phase 2: Deformed check s̃_j, A_v, or B_p at time t (t_i < t < t_o).
- deformedTimePropXv
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(v : V)
(t : ℕ)
(hlo : proc.phase2Start ≤ t)
(hhi : t < proc.phase3Start)
(hgen : IsTimePropagatingGen proc (PauliOp.pauliX (Sum.inl v)) t F)
: IsListedGenerator proc F
Phase 2: Time-propagating X_v pair at t, t+1 (t_i ≤ t < t_o).
- deformedTimePropZv
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(v : V)
(t : ℕ)
(hlo : proc.phase2Start ≤ t)
(hhi : t < proc.phase3Start)
(hgen : IsTimePropagatingGen proc (PauliOp.pauliZ (Sum.inl v)) t F)
: IsListedGenerator proc F
Phase 2: Time-propagating Z_v pair at t, t+1 with A_v measurement fault (t_i ≤ t < t_o).
- deformedTimePropXe
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(e : ↑G.edgeSet)
(t : ℕ)
(hlo : proc.phase2Start ≤ t)
(hhi : t < proc.phase3Start)
(hgen : IsTimePropagatingGen proc (PauliOp.pauliX (Sum.inr e)) t F)
: IsListedGenerator proc F
Phase 2: Time-propagating X_e pair at t, t+1 with B_p measurement faults (t_i ≤ t < t_o).
- deformedTimePropZe
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(e : ↑G.edgeSet)
(t : ℕ)
(hlo : proc.phase2Start ≤ t)
(hhi : t < proc.phase3Start)
(hgen : IsTimePropagatingGen proc (PauliOp.pauliZ (Sum.inr e)) t F)
: IsListedGenerator proc F
Phase 2: Time-propagating Z_e pair at t, t+1 with A_v measurement faults (t_i ≤ t < t_o).
- gaugingSj
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(j : J)
(hgen : IsSpaceStabilizerGen proc (DeformedCode.deformedOriginalChecks G checks proc.deformedData j) proc.phase2Start F)
: IsListedGenerator proc F
Gauging (t = t_i): Original check s_j at t_i.
- gaugingZe
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(e : ↑G.edgeSet)
(hgen : IsSpaceStabilizerGen proc (PauliOp.pauliZ (Sum.inr e)) proc.phase2Start F)
: IsListedGenerator proc F
Gauging (t = t_i): Z_e at t_i.
- gaugingInitXe
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(e : ↑G.edgeSet)
(hgen : IsInitXeGen proc e F)
: IsListedGenerator proc F
Gauging (t = t_i): Init fault + X_e.
- gaugingZeAv
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(e : ↑G.edgeSet)
(r : Fin proc.d)
(hgen : IsZeAvMeasGen proc e (proc.phase2Start + 1) r F)
: IsListedGenerator proc F
Gauging (t = t_i): Z_e at t_i+1 with A_v measurement faults for v ∈ e.
- ungaugingCheck
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(ci : DeformedCode.CheckIndex V C J)
(hgen : IsSpaceStabilizerGen proc (DeformedCode.allChecks G cycles checks proc.deformedData ci) proc.phase3Start F)
: IsListedGenerator proc F
Ungauging (t = t_o): Deformed check s̃_j, A_v, or B_p at t_o.
- ungaugingReadoutXe
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(e : ↑G.edgeSet)
(hgen : IsReadoutXeGen proc e F)
: IsListedGenerator proc F
Ungauging (t = t_o): X_e + Z_e readout fault.
- ungaugingBareZe
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(e : ↑G.edgeSet)
(hgen : IsSpaceStabilizerGen proc (PauliOp.pauliZ (Sum.inr e)) proc.phase3Start F)
: IsListedGenerator proc F
Ungauging (t = t_o): Bare Z_e at t_o.
- ungaugingZeAv
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(e : ↑G.edgeSet)
(r : Fin proc.d)
(hgen : IsZeAvMeasGen proc e (proc.phase3Start - 1) r F)
: IsListedGenerator proc F
Ungauging (t = t_o): Z_e at t_o-1 with A_v measurement faults for v ∈ e.
- ungaugingTimeProp
{V : Type u_1}
[Fintype V]
[DecidableEq V]
{G : SimpleGraph V}
[DecidableRel G.Adj]
[Fintype ↑G.edgeSet]
{C : Type u_2}
[Fintype C]
[DecidableEq C]
{cycles : C → Set ↑G.edgeSet}
[(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c]
{J : Type u_3}
[Fintype J]
[DecidableEq J]
{checks : J → PauliOp V}
{proc : FaultTolerantGaugingProcedure G cycles checks}
{F : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel}
(P : PauliOp (GaussFlux.ExtQubit G))
(hgen : IsTimePropagatingGen proc P proc.phase3Start F)
: IsListedGenerator proc F
Ungauging (t = t_o): Time-propagating at t_o boundary.
Instances For
Part VI: Main Theorem — Every Listed Generator is a Gauging Stabilizer #
Lemma 5 (Spacetime Stabilizers). Every listed generator fault pattern is a gauging stabilizer: it has empty syndrome and does not affect the logical outcome.
Part VII: Algebraic Justifications #
These facts explain WHY the detector violations cancel for each generator type: which checks commute/anticommute with which Pauli operators, and the structure of the cancellation.
The algebraic structure underlying the spacetime stabilizer classification: self-inverse properties, commutation relations, and Z₂ group structure.
Part VIII: Completeness #
Every spacetime stabilizer is a Z₂ combination of the listed generators. The proof uses time-ordered decomposition: peel off generators at the earliest time, proceed inductively, until only measurement faults remain, which must decompose into detector measurement sets by Lem 4.
Completeness of spacetime stabilizer generators. Every gauging stabilizer decomposes as a Z₂ composition (symmetric difference) of the listed generators.
Part IX: Corollaries #
Z_e commutes with original checks lifted to V ⊕ E.
Double violation cancellation in ZMod 2: x + x = 0.
Part X: Space-Fault Cleaning and Centralizer Properties #
These properties capture constructive steps in the space-time decoupling proof (Lemma 7) that follow from the generator infrastructure.
Space-fault cleaning via time-propagating stabilizers (Steps 1+4 of Lemma 7).
For any syndrome-free spacetime fault, there exists a composition of listed generators (hence a gauging stabilizer) that moves all space-faults to the gauging time t_i. The cleaning stabilizer S₁ satisfies:
- Syndrome-free and preserves the gauging sign (it's a gauging stabilizer)
- Its Pauli error at t_i is in the deformed code's stabilizer group
The construction: for each space-fault at time t ≠ t_i, compose with the appropriate time-propagating generator (type 2-5 in the deformed code phase, type 2 in original code phases) to move it one time step toward t_i. Boundary init/readout faults are absorbed using init-X_e and readout-X_e generators (types 5, 4). The composed generators cancel intermediate Paulis (P·P=1) leaving only the net effect at t_i, and their combined Pauli at t_i is a product of check operators (deformed/original), hence in the stabilizer group.
Centralizer membership for cleaned pure-space faults (Step 3 of Lemma 7).
A pure-space fault concentrated at the gauging time t_i, obtained by cleaning a syndrome-free fault via time-propagating stabilizers, has its Pauli error in the centralizer of the deformed code. This encodes the quantum-mechanical fact that:
- During Phase 2, the active checks are the deformed code checks (A_v, B_p, s̃_j).
- The time-propagating generators (Lem 5, types 2-5) commute with all active checks at times away from their support — the measurement faults they include are precisely chosen to cancel the detector violations from anticommuting checks.
- The cleaning process preserves the commutation structure: after composing with generators that commute with the deformed checks, the concentrated Pauli at t_i inherits commutativity with all deformed code checks.
Therefore, the cleaned Pauli error at t_i commutes with every check of the deformed code, i.e., it is in the centralizer.