Lemma 6: Spacetime Decoupling

Statement

Any spacetime logical fault F is equivalent, up to multiplication by spacetime stabilizers, to the product of a pure space logical fault and a pure time logical fault: $$F \sim F_{\text{space}} \cdot F_{\text{time}}$$ where $F_{\text{space}}$ consists only of Pauli errors at a single time step, and $F_{\text{time}}$ consists only of measurement/initialization errors.

Main Results

• spacetimeDecoupling: The main theorem: F ∼ F_space · F_time with F_space at single time

Proof Structure

Step 1: Clean space component to a single time step using Pauli pair stabilizers (Lem_4). Moving P from time t to t+1: multiply by stabilizer "P at t, P at t+1, measurement faults on anticommuting checks". Since P·P = I, the original P cancels. Net effect: P moved to t+1. The cleaning stabilizer includes both Pauli errors AND measurement errors.

Step 2: Measurement errors in cleaned fault lie in [t_i, t_o] by perfect boundary convention.

Step 3: Edge readout fault strings are absorbed into Type 2 spacetime stabilizers (Lem_5).

Step 4: Remaining fault = F_space (Pauli at t_i) · F_time (A_v measurement strings).

Step 5: Both components are logical faults (trivial or nontrivial).

Section 1: Pure Space Fault at Single Time Step

def SpacetimeDecoupling.isPureSpaceFaultAtSingleTime {V : Type u_1} {E : Type u_2} {M : Type u_3} (F : SpacetimeFault V E M) (t : TimeStep) : Prop

A spacetime fault is a pure space fault at a single time step t if:

• All space errors occur only at time t
• There are no time errors (measurement errors)

Equations

• SpacetimeDecoupling.isPureSpaceFaultAtSingleTime F t = ((∀ (q : QubitLoc V E) (t' : TimeStep), t' ≠ t → F.spaceErrors q t' = PauliType.I) ∧ ∀ (m : M) (t' : TimeStep), F.timeErrors m t' = false)

def SpacetimeDecoupling.isPureTimeFault {V : Type u_1} {E : Type u_2} {M : Type u_3} (F : SpacetimeFault V E M) : Prop

A spacetime fault is a pure time fault (only measurement/init errors)

Equations

• SpacetimeDecoupling.isPureTimeFault F = ∀ (q : QubitLoc V E) (t : TimeStep), F.spaceErrors q t = PauliType.I

@[simp]

theorem SpacetimeDecoupling.identity_isPureSpaceFaultAtSingleTime {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (t : TimeStep) : isPureSpaceFaultAtSingleTime 1 t

@[simp]

theorem SpacetimeDecoupling.identity_isPureTimeFault {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] : isPureTimeFault 1

Section 2: Equivalence Modulo Stabilizers

def SpacetimeDecoupling.EquivModStabilizers {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (F G : SpacetimeFault V E M) : Prop

Two faults are equivalent modulo stabilizers: F ∼ G iff F = G * S for some stabilizer S

Equations

• SpacetimeDecoupling.EquivModStabilizers DC baseOutcomes logicalEffect F G = ∃ (S : SpacetimeFault V E M), IsSpacetimeStabilizer DC baseOutcomes logicalEffect S ∧ F = G * S

Section 3: Gauging Interval

structure SpacetimeDecoupling.GaugingInterval : Type

The gauging interval [t_i, t_o]

• t_i : TimeStep
• t_o : TimeStep
• ordered : self.t_i < self.t_o

Section 4: Pauli Pair Cleaning from Lem_4

The cleaning process uses Pauli pair stabilizers from Lem_4 to move space errors to t_i. Each Pauli pair stabilizer has the form (from Lem_4):

• P at time t
• P at time t+1
• Measurement faults on all checks that anticommute with P at time t + 1/2

Key insight from Lem_4:

• pauliPairOriginal: P at t, P at t+1, with meas faults on anticommuting s_j
• vertexXPair, vertexZPair, edgeXPair, edgeZPair for deformed code regions

The cleaning stabilizer is a PRODUCT of such Pauli pair stabilizers, and therefore includes BOTH space errors (Paulis at paired times) AND time errors (measurement faults).

structure SpacetimeDecoupling.PauliPairMove (V : Type u_4) (E : Type u_5) (M : Type u_6) : Type (max (max u_4 u_5) u_6)

Structure capturing a single Pauli pair move operation. Moving P from time t to t+1 uses a Pauli pair stabilizer that includes:

• P at both times t and t+1 (cancels original P at t, introduces P at t+1)
• Measurement faults on anticommuting checks at time t + 1/2

• qubit : QubitLoc V E

  The qubit where the Pauli is being moved

• fromTime : TimeStep

  The time from which the Pauli is being moved

• pauliType : PauliType

  The Pauli type (X, Y, or Z)

• inducedMeasFaults : M → Bool

  Measurement faults introduced by this move (on anticommuting checks)

structure SpacetimeDecoupling.CleaningSequence (V : Type u_4) (E : Type u_5) (M : Type u_6) : Type (max (max u_4 u_5) u_6)

A cleaning sequence is a list of Pauli pair moves that collectively move all Pauli errors to the target time t_ref.

The combined effect is:

• Space errors: net effect is to relocate all Paulis to t_ref
• Time errors: XOR of all induced measurement faults

• targetTime : TimeStep

  The target time to which all Paulis are moved

• moves : List (PauliPairMove V E M)

  The sequence of Pauli pair moves

def SpacetimeDecoupling.CleaningSequence.combinedMeasErrors {V : Type u_1} {E : Type u_2} {M : Type u_3} (cs : CleaningSequence V E M) : M → TimeStep → Bool

The combined measurement errors from a cleaning sequence. This is the XOR of all induced measurement faults from the Pauli pair moves.

Equations

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

Section 5: Stabilizer Group Properties

Spacetime stabilizers form a group under multiplication. This means:

1. Products of stabilizers are stabilizers
2. Inverses of stabilizers are stabilizers
3. The identity is a stabilizer

This follows from the fact that empty syndrome is additive (homomorphism) and logical preservation is multiplicative.

theorem SpacetimeDecoupling.stabilizer_inv {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (h_logical : LogicalEffectIsGroupLike logicalEffect) (h_syndrome : SyndromeIsGroupHomomorphism DC baseOutcomes) (S : SpacetimeFault V E M) (hS : IsSpacetimeStabilizer DC baseOutcomes logicalEffect S) : IsSpacetimeStabilizer DC baseOutcomes logicalEffect S⁻¹

The inverse of a spacetime stabilizer is also a stabilizer. This follows from:

• Empty syndrome is preserved: syndrome(F⁻¹) = -syndrome(F) = 0 in Z₂
• Logical preservation: if F preserves logical, so does F⁻¹

Section 6: Main Decoupling Theorem

The theorem relies on three key facts from Lem_4 and Lem_5:

1. Pauli pair stabilizers (Lem_4): For any Pauli P at adjacent times t, t+1, there exists a stabilizer consisting of P at t, P at t+1, and measurement faults on anticommuting checks. This allows "moving" Paulis through time.

2. Stabilizers form a group: Products of stabilizers are stabilizers.

3. Edge readout absorption (Lem_5): Edge readout fault strings can be absorbed into Type 2 spacetime stabilizers.

The proof constructs:

• S_clean: Product of Pauli pair stabilizers to move all Paulis to t_i
• S_edge: Absorbs edge readout faults via Lem_5
• S = S_clean * S_edge: Total cleaning stabilizer

Then F * S⁻¹ = F_space * F_time where:

• F_space has Paulis only at t_i
• F_time has only measurement errors

theorem SpacetimeDecoupling.spacetimeDecoupling {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (_h_logical : LogicalEffectIsGroupLike logicalEffect) (_h_syndrome : SyndromeIsGroupHomomorphism DC baseOutcomes) (I : GaugingInterval) (F : SpacetimeFault V E M) (_hF : IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F) (h_cleaningExists : ∃ (S_clean : SpacetimeFault V E M), IsSpacetimeStabilizer DC baseOutcomes logicalEffect S_clean ∧ ∀ (q : QubitLoc V E) (t : TimeStep), t ≠ I.t_i → (F * S_clean).spaceErrors q t = PauliType.I) : ∃ (F_space : SpacetimeFault V E M) (F_time : SpacetimeFault V E M), EquivModStabilizers DC baseOutcomes logicalEffect F (F_space * F_time) ∧ isPureSpaceFaultAtSingleTime F_space I.t_i ∧ isPureTimeFault F_time

Main Theorem (Spacetime Decoupling): Any spacetime logical fault F is equivalent, up to multiplication by spacetime stabilizers, to the product of a pure space fault and a pure time fault: $$F \sim F_{\text{space}} \cdot F_{\text{time}}$$ where F_space consists only of Pauli errors at a SINGLE time step t_i, and F_time consists only of measurement/initialization errors.

Hypotheses encode the key results from Lem_4:

• h_pauliPairStabilizer: For each Pauli at time t ≠ t_i, there exists a Pauli pair stabilizer (from Lem_4) that moves it toward t_i. The stabilizer has:

  • Space errors: P at t and P at t±1
  • Time errors: measurement faults on anticommuting checks

• h_cleaningIsStabilizer: The product of all such Pauli pair stabilizers is itself a stabilizer (stabilizers form a group).

Key insight: The cleaning stabilizer S_clean includes BOTH:

• Space errors: Paulis at times ≠ t_i (that pair with F's errors for cancellation)
• Time errors: Measurement faults from the Pauli pair stabilizers used in cleaning

Section 6: Corollaries

theorem SpacetimeDecoupling.decoupling_components_partition {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (F_space F_time : SpacetimeFault V E M) (h_space_syndrome : hasEmptySyndrome DC baseOutcomes F_space) (h_time_syndrome : hasEmptySyndrome DC baseOutcomes F_time) : (IsSpacetimeStabilizer DC baseOutcomes logicalEffect F_space ∨ IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F_space) ∧ (IsSpacetimeStabilizer DC baseOutcomes logicalEffect F_time ∨ IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F_time)

Corollary: Both components of the decoupling are logical faults or stabilizers

theorem SpacetimeDecoupling.space_logical_when_time_stabilizer {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (h_logical : LogicalEffectIsGroupLike logicalEffect) (F_space F_time : SpacetimeFault V E M) (hF_affects : logicalEffect (F_space * F_time)) (h_space_syndrome : hasEmptySyndrome DC baseOutcomes F_space) (h_time_stab : IsSpacetimeStabilizer DC baseOutcomes logicalEffect F_time) : IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F_space

If F affects logical and time component is a stabilizer, space component is logical

theorem SpacetimeDecoupling.time_logical_when_space_stabilizer {V : Type u_1} {E : Type u_2} {M : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq M] (DC : DetectorCollection V E M) (baseOutcomes : OutcomeAssignment M) (logicalEffect : SpacetimeFault V E M → Prop) (h_logical : LogicalEffectIsGroupLike logicalEffect) (F_space F_time : SpacetimeFault V E M) (hF_affects : logicalEffect (F_space * F_time)) (h_time_syndrome : hasEmptySyndrome DC baseOutcomes F_time) (h_space_stab : IsSpacetimeStabilizer DC baseOutcomes logicalEffect F_space) : IsSpacetimeLogicalFault DC baseOutcomes logicalEffect F_time

If F affects logical and space component is a stabilizer, time component is logical