Lemma 7: Space-Time Decoupling

Statement

Any spacetime logical fault (Def_11) is equivalent, up to multiplication by spacetime stabilizers (Def_11), to the product of a space-only logical fault and a time-only logical fault.

Formally: Let F be a spacetime logical fault in the fault-tolerant gauging measurement procedure (Def_10). Then there exist:

• A space logical fault F_S: a spacetime fault consisting solely of Pauli errors at time t_i, such that F_S is a logical operator of the deformed code (Def_4).
• A time logical fault F_T: a spacetime fault consisting solely of time-faults (measurement/initialization errors), with no Pauli errors.
• A spacetime stabilizer S (Def_11).

such that F = F_S · F_T · S (composition via symmetric difference of fault sets).

Main Results

• FullOutcomePreserving: The full outcome predicate (sign + code state)
• IsSpaceLogicalFault: A space-only fault at t_i that is a logical of the deformed code
• IsTimeLogicalFault: A pure-time fault that flips the gauging sign
• spaceTime_decomposition: The main decomposition theorem F = F_S · F_T · S
• space_time_independent_effects: F_S and F_T affect different aspects of the outcome

Proof Outline

1. Move all space-faults to time t_i using time-propagating stabilizers (Lem 5)
2. Convert boundary init/readout faults to space-faults at t_i using Lem 5 generators
3. Separate the remaining time-faults into A_v strings (logical) or stabilizer generators
4. Verify independence: space affects code state, time affects measurement sign

Part I: Full Outcome Predicate

The paper's Def_11 says a spacetime logical fault "changes the outcome" in EITHER of two ways:

1. Flipping the inferred measurement sign σ (time-type logical), OR
2. Applying a nontrivial logical operator to the post-measurement code state (space-type logical).

A fault is outcome-preserving if NEITHER occurs: the sign is preserved AND the net Pauli error at t_i is in the deformed stabilizer group (not a nontrivial logical).

noncomputable def SpaceTimeDecoupling.theDeformedCode {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) : StabilizerCode (GaussFlux.ExtQubit G)

The deformed stabilizer code at the gauging time, constructed from proc's data.

Equations

• SpaceTimeDecoupling.theDeformedCode proc = DeformedCodeChecks.deformedStabilizerCode G cycles checks proc.deformedData ⋯ ⋯

def SpaceTimeDecoupling.FullOutcomePreserving {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) : Prop

The full outcome-preserving predicate for the fault-tolerant gauging procedure. A fault preserves the outcome if BOTH: (1) The gauging sign σ is preserved (no time-logical effect), AND (2) The net Pauli error at t_i is in the deformed stabilizer group (no space-logical effect).

This captures the paper's Def_11: a spacetime stabilizer leaves both the classical measurement record and the quantum code state unchanged.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev SpaceTimeDecoupling.IsFullGaugingLogicalFault {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) : Prop

A spacetime logical fault under the full outcome predicate: syndrome-free AND changes the outcome (either flips sign or applies nontrivial logical).

Equations

• SpaceTimeDecoupling.IsFullGaugingLogicalFault proc F = SpacetimeLogicalFault.IsGaugingLogicalFault proc proc.detectorOfIndex (SpaceTimeDecoupling.FullOutcomePreserving proc) F

@[reducible, inline]

abbrev SpaceTimeDecoupling.IsFullGaugingStabilizer {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) : Prop

A spacetime stabilizer under the full outcome predicate: syndrome-free AND preserves both the sign and code state.

Equations

• SpaceTimeDecoupling.IsFullGaugingStabilizer proc F = SpacetimeLogicalFault.IsGaugingStabilizer proc proc.detectorOfIndex (SpaceTimeDecoupling.FullOutcomePreserving proc) F

theorem SpaceTimeDecoupling.logicalFault_outcome_change {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) (hlog : IsFullGaugingLogicalFault proc F) : SpacetimeLogicalFault.FlipsGaugingSign proc F ∨ F.pauliErrorAt proc.phase2Start ∉ (theDeformedCode proc).stabilizerGroup

A logical fault changes the outcome: ¬(sign preserved ∧ Pauli in stabilizer group). Equivalently: either the sign is flipped, or the Pauli error is a nontrivial logical.

Part II: Space-Only and Time-Only Fault Definitions

def SpaceTimeDecoupling.IsSpaceLogicalFault {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) : Prop

A space-only logical fault: all space-faults are concentrated at t_i, no time-faults, and the composite Pauli error at t_i is a nontrivial logical of the deformed code.

Equations

• One or more equations did not get rendered due to their size.

def SpaceTimeDecoupling.IsTimeLogicalFault {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) : Prop

A time-only logical fault: no space-faults, syndrome-free, and flips the gauging sign σ.

Equations

• SpaceTimeDecoupling.IsTimeLogicalFault proc F = (F.isPureTime ∧ SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F ∧ SpacetimeLogicalFault.FlipsGaugingSign proc F)

Part III: Z₂ Algebra of Symmetric Differences

The key algebraic fact: sums of ZMod 2 indicators over symmetric differences decompose additively. This underlies all composition properties of the gauging procedure.

Part III-A: Composition Properties — gaussSignFlip

The gaussSignFlip is a double sum of ZMod 2 indicators over timeFaults. Since composition takes the symmetric difference of timeFaults, the Z₂ additivity of indicators gives additivity of gaussSignFlip.

theorem SpaceTimeDecoupling.gaussSignFlip_compose_additive {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₁ F₂ : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) : SpacetimeLogicalFault.gaussSignFlip proc (F₁.compose F₂) = SpacetimeLogicalFault.gaussSignFlip proc F₁ + SpacetimeLogicalFault.gaussSignFlip proc F₂

The gaussSignFlip is Z₂-additive under composition: sign(F₁ · F₂) = sign(F₁) + sign(F₂) in ZMod 2. This follows from the fact that timeFaults of the composition is the symmetric difference, and the indicator function is additive over Z₂.

Part III-B: Composition Properties — pauliErrorAt

The Pauli error at time t is defined via sums over spaceFaultsAt t. Since composition takes the symmetric difference of spaceFaults, and filter distributes over symmDiff, the Z₂ sum additivity gives multiplicativity of PauliOp.

theorem SpaceTimeDecoupling.pauliErrorAt_compose_mul {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₁ F₂ : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (t : ℕ) : (F₁.compose F₂).pauliErrorAt t = F₁.pauliErrorAt t * F₂.pauliErrorAt t

The net Pauli error at t is multiplicative under composition: pauliErrorAt(F₁ · F₂, t) = pauliErrorAt(F₁, t) * pauliErrorAt(F₂, t). This follows because spaceFaults of the composition is the symmetric difference, filter distributes over symmDiff, and Z₂ sums are additive = Pauli product.

Part III-C: Composition Properties — Syndrome-Freeness

Detector violation depends on flipParity, which is a ZMod 2 sum of indicators over timeFaults. By the same Z₂ additivity, composing two syndrome-free faults preserves syndrome-freeness.

theorem SpaceTimeDecoupling.compose_syndromeFree_syndromeFree {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 S : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (hF : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F) (hS : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex S) : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex (F.compose S)

Composing two syndrome-free faults preserves syndrome-freeness. Both faults have empty syndrome, so the composed fault (symmetric difference of timeFaults) also has empty syndrome by Z₂ additivity of flipParity.

theorem SpaceTimeDecoupling.compose_preserves_syndromeFree {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 S : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (hF : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F) (hS : IsFullGaugingStabilizer proc S) : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex (F.compose S)

Composing with a full stabilizer preserves syndrome-freeness.

Part III-D: Composition Properties — Full Stabilizer Closure

Combining the above: the composition of two full stabilizers is a full stabilizer. Syndrome-freeness, sign preservation, and stabilizer group membership all transfer.

theorem SpaceTimeDecoupling.compose_fullGaugingStabilizer {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₁ F₂ : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (h₁ : IsFullGaugingStabilizer proc F₁) (h₂ : IsFullGaugingStabilizer proc F₂) : IsFullGaugingStabilizer proc (F₁.compose F₂)

The composition of two full gauging stabilizers is a full gauging stabilizer. Syndrome-freeness and outcome preservation are both additive over Z₂.

Part IV: Time-Propagating Stabilizers Move Space-Faults

The time-propagating generators from Lem_5 allow moving a Pauli error from time t to time t+1 (or t-1). By composing these, we can move any space-fault to the gauging time t_i = phase2Start.

The Empty Fault is a Full Gauging Stabilizer

The empty fault (no space-faults, no time-faults) trivially satisfies all stabilizer conditions: empty syndrome, zero sign flip, and the identity Pauli is in the stabilizer group.

theorem SpaceTimeDecoupling.empty_isFullGaugingStabilizer {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) : IsFullGaugingStabilizer proc SpacetimeFault.empty

The empty fault is a full gauging stabilizer.

theorem SpaceTimeDecoupling.boundary_faults_trivially_absorbed {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) (_hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F') (hconc : ∀ (t : ℕ), t ≠ proc.phase2Start → F'.spaceFaultsAt t = ∅) : ∃ (S₂ : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel), IsFullGaugingStabilizer proc S₂ ∧ ∀ (t : ℕ), t ≠ proc.phase2Start → (F'.compose S₂).spaceFaultsAt t = ∅

Boundary faults can be absorbed: if space-faults are already concentrated at t_i, the empty fault serves as a trivial stabilizer preserving this property. Steps 1 and 4 of the paper are subsumed by space_fault_cleaning (Lem 5), which handles both time-propagation and boundary absorption in one step.

Space-Fault Cleaning and Centralizer Membership

Using the space_fault_cleaning and syndromeFree_pureSpace_inCentralizer axioms from Lem 5, we prove the two key constructive lemmas needed for the main decomposition:

1. Any syndrome-free fault can be cleaned to have space-faults only at t_i
2. A pure-space fault concentrated at t_i has its Pauli error in the centralizer

theorem SpaceTimeDecoupling.space_fault_cleaning_fullStabilizer {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) (hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F) : ∃ (S₁ : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel), IsFullGaugingStabilizer proc S₁ ∧ ∀ (t : ℕ), t ≠ proc.phase2Start → (F.compose S₁).spaceFaultsAt t = ∅

Space-fault cleaning (Steps 1+4): Any syndrome-free spacetime fault can be composed with a full gauging stabilizer to concentrate all space-faults at t_i. This uses the time-propagating and boundary generators from Lem 5.

theorem SpaceTimeDecoupling.centralizer_of_syndromeFree_pureSpace {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) (hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F) (hconc : ∀ (t : ℕ), t ≠ proc.phase2Start → F.spaceFaultsAt t = ∅) (hpure : F.isPureSpace) : (theDeformedCode proc).inCentralizer (F.pauliErrorAt proc.phase2Start)

Centralizer membership (Step 3): A syndrome-free pure-space fault concentrated at t_i has its Pauli error in the centralizer of the deformed code. This encodes the quantum-mechanical fact that the deformed code checks are the active checks at t_i, and the cleaning process preserves commutation.

Part V: Time-Fault Classification

After cleaning, the time-faults form a pure-time fault. By Lem 6, syndrome-free pure-time faults either flip σ (logical time-fault = A_v string) or decompose into stabilizer generators (trivial).

theorem SpaceTimeDecoupling.time_faults_dichotomy {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_T : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (hpure : TimeFaultDistance.IsPureTimeFault proc F_T) (hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F_T) : SpacetimeLogicalFault.FlipsGaugingSign proc F_T ∨ SpacetimeLogicalFault.IsGaugingStabilizer proc proc.detectorOfIndex (SpacetimeLogicalFault.PreservesGaugingSign proc) F_T

The cleaned time-faults of a syndrome-free fault either flip the sign or are stabilizers. This is the content of Lem 6's pureTime_syndromeFree_logical_or_stabilizer_generators.

Part VI: Independence of Space and Time Effects

The space fault F_S and time fault F_T affect the procedure outcome independently:

• F_S acts on the code Hilbert space (applies a Pauli logical operator)
• F_T acts on the classical measurement record (flips σ)

theorem SpaceTimeDecoupling.gaussSignFlip_depends_only_on_timeFaults {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₁ F₂ : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (heq : F₁.timeFaults = F₂.timeFaults) : SpacetimeLogicalFault.gaussSignFlip proc F₁ = SpacetimeLogicalFault.gaussSignFlip proc F₂

The gauging sign depends only on time-faults (measurement errors on Gauss checks). Space-faults do not affect the gauging sign directly.

theorem SpaceTimeDecoupling.pureSpace_preservesSign {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) (hpure : F.isPureSpace) : SpacetimeLogicalFault.PreservesGaugingSign proc F

A pure-space fault preserves the gauging sign.

theorem SpaceTimeDecoupling.pauliErrorAt_depends_only_on_spaceFaults {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₁ F₂ : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (heq : F₁.spaceFaults = F₂.spaceFaults) (t : ℕ) : F₁.pauliErrorAt t = F₂.pauliErrorAt t

The Pauli error at any time depends only on space-faults. Two faults with the same spaceFaults have the same pauliErrorAt.

theorem SpaceTimeDecoupling.pureTime_pauliError_trivial {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) (hpure : F.isPureTime) (t : ℕ) : F.pauliErrorAt t = 1

A pure-time fault does not change the Pauli error at any time.

theorem SpaceTimeDecoupling.space_time_independent_effects {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) : SpacetimeLogicalFault.gaussSignFlip proc F = SpacetimeLogicalFault.gaussSignFlip proc F.timeComponent ∧ ∀ (t : ℕ), F.pauliErrorAt t = F.spaceComponent.pauliErrorAt t

Independence theorem: The space and time components of a fault affect different aspects of the procedure outcome.

• The gauging sign σ depends only on time-faults (measurement errors).
• The Pauli error on the code state depends only on space-faults. Therefore F_S and F_T have independent effects.

theorem SpaceTimeDecoupling.gaussSignFlip_compose_pureSpace {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_S F_T : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (hpS : F_S.isPureSpace) : SpacetimeLogicalFault.gaussSignFlip proc (F_S.compose F_T) = SpacetimeLogicalFault.gaussSignFlip proc F_T

The sign flip of F_S · F_T equals the sign flip of F_T when F_S is pure-space.

Part VII: Main Decomposition Theorem

The central result: any spacetime logical fault decomposes as F = F_S · F_T · S.

theorem SpaceTimeDecoupling.spaceTime_decomposition {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) (hlog : IsFullGaugingLogicalFault proc F) : ∃ (F_S : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (F_T : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (S : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel), F = (F_S.compose F_T).compose S ∧ F_S.isPureSpace ∧ (∀ (t : ℕ), t ≠ proc.phase2Start → F_S.spaceFaultsAt t = ∅) ∧ F_T.isPureTime ∧ SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F_T ∧ IsFullGaugingStabilizer proc S ∧ (SpacetimeLogicalFault.FlipsGaugingSign proc F_T ∨ (theDeformedCode proc).isLogicalOp (F_S.pauliErrorAt proc.phase2Start))

Lemma 7 (Space-Time Decoupling): Main Theorem.

Any spacetime logical fault F in the fault-tolerant gauging measurement procedure is equivalent, up to multiplication by spacetime stabilizers, to the product of a space-only fault F_S and a time-only fault F_T.

Specifically: there exist F_S, F_T, and S such that:

• F = F_S · F_T · S (composition via symmetric difference)
• F_S is pure-space (no time-faults) and concentrated at time t_i
• F_T is pure-time (no space-faults) and syndrome-free
• S is a full gauging stabilizer (syndrome-free, outcome-preserving)
• If F_T is nontrivial, it flips the gauging sign σ (time-logical)
• If F_S is nontrivial, its Pauli error at t_i is a nontrivial deformed-code logical

The proof proceeds by:

1. Move all space-faults to t_i using time-propagating stabilizers (Lem 5)
2. Convert boundary init/readout faults to space-faults at t_i (Lem 5 generators)
3. Separate the cleaned fault into space and time parts
4. Classify the time part via Lem 6's dichotomy

Part VIII: The A_v String as Canonical Time Logical Fault

theorem SpaceTimeDecoupling.gaussString_is_time_logical {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) (v : V) (hodd : Odd proc.d) : IsTimeLogicalFault proc (TimeFaultDistance.gaussStringFault proc v)

The A_v string is the canonical time-only logical fault. It has weight d, is syndrome-free, and flips the gauging sign when d is odd.

theorem SpaceTimeDecoupling.time_logical_weight_ge_d {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_T : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (h : IsTimeLogicalFault proc F_T) (hodd : Odd proc.d) : proc.d ≤ F_T.weight

Time-only logical faults have weight at least d (when d is odd).

theorem SpaceTimeDecoupling.gaussString_flipsSign {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) (v : V) (hodd : Odd proc.d) : SpacetimeLogicalFault.FlipsGaugingSign proc (TimeFaultDistance.gaussStringFault proc v)

Sign flip of the A_v string.

Part IX: Sign-Flip Analysis

theorem SpaceTimeDecoupling.gaussSignFlip_pureSpace {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) (hpure : F.isPureSpace) : SpacetimeLogicalFault.gaussSignFlip proc F = 0

A pure-space fault has zero sign flip.

Part X: Structural Decomposition Properties

theorem SpaceTimeDecoupling.fault_space_time_decomposition {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) : F = F.spaceComponent.compose F.timeComponent

Any spacetime fault decomposes into its space and time components.

theorem SpaceTimeDecoupling.weight_decomposition {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) : F.weight = F.spaceWeight + F.timeWeight

The weight of a fault is the sum of its space and time weights.

theorem SpaceTimeDecoupling.compose_pureSpace_pureTime_spaceComponent {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_S F_T : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (hpS : F_S.isPureSpace) (hpT : F_T.isPureTime) : (F_S.compose F_T).spaceComponent = F_S

The compose of pure-space and pure-time faults preserves the space component.

theorem SpaceTimeDecoupling.compose_pureSpace_pureTime_timeComponent {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_S F_T : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (hpS : F_S.isPureSpace) (hpT : F_T.isPureTime) : (F_S.compose F_T).timeComponent = F_T

The compose of pure-space and pure-time faults preserves the time component.

theorem SpaceTimeDecoupling.compose_pureSpace_pureTime_weight {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_S F_T : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (hpS : F_S.isPureSpace) (hpT : F_T.isPureTime) : (F_S.compose F_T).weight = F_S.weight + F_T.weight

When F_S is pure-space and F_T is pure-time, their composition has weight equal to the sum of their weights (since their fault sets are disjoint).

Part XI: Decoupling Summary

Full summary combining decomposition with independence of effects.

theorem SpaceTimeDecoupling.sign_flipping_logical_has_Av_string {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) (hfree : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F) (hflip : SpacetimeLogicalFault.FlipsGaugingSign proc F) (hodd : Odd proc.d) : ∃ (v : V), ∀ (r : Fin proc.d), { measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r) } ∈ F.timeFaults

If F is a logical fault that flips the sign, then the time component contains at least one full A_v measurement string.

theorem SpaceTimeDecoupling.spaceTime_decoupling_summary {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) (hlog : IsFullGaugingLogicalFault proc F) : (∃ (F_S : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (F_T : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (S : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel), F = (F_S.compose F_T).compose S ∧ F_S.isPureSpace ∧ (∀ (t : ℕ), t ≠ proc.phase2Start → F_S.spaceFaultsAt t = ∅) ∧ F_T.isPureTime ∧ SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex F_T ∧ IsFullGaugingStabilizer proc S) ∧ SpacetimeLogicalFault.gaussSignFlip proc F = SpacetimeLogicalFault.gaussSignFlip proc F.timeComponent ∧ ∀ (t : ℕ), F.pauliErrorAt t = F.spaceComponent.pauliErrorAt t

Main summary: Space-time decoupling for the fault-tolerant gauging procedure.

For any spacetime logical fault F of the fault-tolerant gauging measurement procedure:

1. F decomposes as F = F_S · F_T · S where:

• F_S is pure-space (Pauli errors only), concentrated at t_i
• F_T is pure-time (measurement errors only), syndrome-free
• S is a full gauging stabilizer (preserves sign AND code state)

2. The gauging sign σ is determined entirely by F_T: gaussSignFlip(F) = gaussSignFlip(F_T)

3. The Pauli error on the code state is determined entirely by F_S: pauliErrorAt(F, t) = pauliErrorAt(F_S, t) for all t

4. If F flips the sign, then F_T is a time-only logical fault (A_v measurement string with weight d, characterized in Lem 6)

5. If F applies a nontrivial space logical, then F_S is a space logical fault (deformed code logical operator at time t_i)

Part XII: Weight Bounds from Decoupling

theorem SpaceTimeDecoupling.decoupling_weight_bound {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_S F_T : SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel) (hpS : F_S.isPureSpace) (hpT : F_T.isPureTime) : (F_S.compose F_T).weight ≤ F_S.weight + F_T.weight

Weight bound from decoupling: For any pair of pure-space and pure-time faults, their composition has weight equal to the sum of weights.