Lemma 3: Spacetime Code Detectors

Statement

The following form a generating set of local detectors in the fault-tolerant gauging measurement procedure:

For t < t_i and t > t_o (before and after code deformation):

• s_j^t: Repeated measurement of check s_j at times t - 1/2 and t + 1/2

For t_i < t < t_o (during code deformation):

• A_v^t: Repeated measurement of A_v at times t - 1/2 and t + 1/2
• B_p^t: Repeated measurement of B_p at times t - 1/2 and t + 1/2
• s̃_j^t: Repeated measurement of s̃_j at times t - 1/2 and t + 1/2

For t = t_i (start of code deformation):

• B_p^{t_i}: Initialization of edges e ∈ p in |0⟩_e at t_i - 1/2 and first measurement of B_p at t_i + 1/2 (since B_p|0⟩^⊗p = |0⟩^⊗p)
• s̃_j^{t_i}: Initialization of edges e ∈ γ_j in |0⟩_e, measurement of s_j at t_i - 1/2, and measurement of s̃_j at t_i + 1/2

For t = t_o (end of code deformation):

• B_p^{t_o}: Measurement of B_p at t_o - 1/2 and Z_e measurements on edges e ∈ p at t_o + 1/2
• s̃_j^{t_o}: Measurement of s̃_j at t_o - 1/2, Z_e measurements on edges e ∈ γ_j, and measurement of s_j at t_o + 1/2

Main Results

• bulk_detector_parity_zero: Repeated measurements of same check give XOR = 0
• initial_Bp_parity_from_zero_init: B_p = +1 on |0⟩^⊗|E| state
• initial_stilde_from_zero_init: s̃_j = s_j when Z_γ = +1
• final_Bp_equals_product_Ze: B_p measurement = ∏ Z_e measurements
• detectors_generate_local: Elementary detectors span all local parities

Proof Approach

The generating property follows from four sub-lemmas:

1. Bulk detectors: Projective measurement gives equal consecutive outcomes
2. Initial B_p boundary: |0⟩ is +1 eigenstate of all Z operators
3. Initial s̃_j boundary: Z_γ acts as +1 on |0⟩ initialization
4. Final boundary: B_p and s̃_j decompose into individual Z measurements

Section 1: Time Region Classification

The gauging measurement procedure has three time regions:

1. Before code deformation: t < t_i (original code)
2. During code deformation: t_i < t < t_o (gauged code)
3. After code deformation: t > t_o (original code)

Plus two boundary times: 4. Start of deformation: t = t_i 5. End of deformation: t = t_o

structure SpacetimeCodeDetectors.GaugingRegion : Type

Configuration of the gauging procedure time boundaries

• t_i : TimeStep

  Start time of code deformation

• t_o : TimeStep

  End time of code deformation

• valid_range : self.t_i < self.t_o

  t_i < t_o: deformation has positive duration

def SpacetimeCodeDetectors.GaugingRegion.isBefore (R : GaugingRegion) (t : TimeStep) : Prop

Check if a time is before code deformation

Equations

• R.isBefore t = (t < R.t_i)

def SpacetimeCodeDetectors.GaugingRegion.isDuring (R : GaugingRegion) (t : TimeStep) : Prop

Check if a time is during code deformation (strictly between boundaries)

Equations

• R.isDuring t = (R.t_i < t ∧ t < R.t_o)

def SpacetimeCodeDetectors.GaugingRegion.isAfter (R : GaugingRegion) (t : TimeStep) : Prop

Check if a time is after code deformation

Equations

• R.isAfter t = (t > R.t_o)

def SpacetimeCodeDetectors.GaugingRegion.isStart (R : GaugingRegion) (t : TimeStep) : Prop

Check if a time is at the start boundary

Equations

• R.isStart t = (t = R.t_i)

def SpacetimeCodeDetectors.GaugingRegion.isEnd (R : GaugingRegion) (t : TimeStep) : Prop

Check if a time is at the end boundary

Equations

• R.isEnd t = (t = R.t_o)

instance SpacetimeCodeDetectors.GaugingRegion.instDecidablePredTimeStepIsBefore (R : GaugingRegion) : DecidablePred R.isBefore

Equations

• R.instDecidablePredTimeStepIsBefore t = inferInstanceAs (Decidable (t < R.t_i))

instance SpacetimeCodeDetectors.GaugingRegion.instDecidablePredTimeStepIsDuring (R : GaugingRegion) : DecidablePred R.isDuring

Equations

• R.instDecidablePredTimeStepIsDuring t = inferInstanceAs (Decidable (R.t_i < t ∧ t < R.t_o))

instance SpacetimeCodeDetectors.GaugingRegion.instDecidablePredTimeStepIsAfter (R : GaugingRegion) : DecidablePred R.isAfter

Equations

• R.instDecidablePredTimeStepIsAfter t = inferInstanceAs (Decidable (t > R.t_o))

instance SpacetimeCodeDetectors.GaugingRegion.instDecidablePredTimeStepIsStart (R : GaugingRegion) : DecidablePred R.isStart

Equations

• R.instDecidablePredTimeStepIsStart t = inferInstanceAs (Decidable (t = R.t_i))

instance SpacetimeCodeDetectors.GaugingRegion.instDecidablePredTimeStepIsEnd (R : GaugingRegion) : DecidablePred R.isEnd

Equations

• R.instDecidablePredTimeStepIsEnd t = inferInstanceAs (Decidable (t = R.t_o))

theorem SpacetimeCodeDetectors.GaugingRegion.region_classification (R : GaugingRegion) (t : TimeStep) : R.isBefore t ∨ R.isStart t ∨ R.isDuring t ∨ R.isEnd t ∨ R.isAfter t

The time regions partition all times

theorem SpacetimeCodeDetectors.GaugingRegion.regions_mutually_exclusive (R : GaugingRegion) (t : TimeStep) : ¬(R.isBefore t ∧ R.isStart t) ∧ ¬(R.isBefore t ∧ R.isDuring t) ∧ ¬(R.isStart t ∧ R.isDuring t) ∧ ¬(R.isDuring t ∧ R.isEnd t) ∧ ¬(R.isDuring t ∧ R.isAfter t)

The time regions are mutually exclusive

Section 2: Parity Value Algebra

Parity values are in ZMod 2:

• 0 represents +1 (no flip)
• 1 represents -1 (flip)

The XOR operation (addition in ZMod 2) computes parity of measurement outcomes.

@[reducible, inline]

abbrev SpacetimeCodeDetectors.ParityValue : Type

Parity value type: 0 represents +1 (no flip), 1 represents -1 (flip)

Equations

• SpacetimeCodeDetectors.ParityValue = ZMod 2

@[reducible, inline]

abbrev SpacetimeCodeDetectors.MeasOutcome : Type

Measurement outcome represented as ZMod 2 (0 = +1 outcome, 1 = -1 outcome)

Equations

• SpacetimeCodeDetectors.MeasOutcome = ZMod 2

theorem SpacetimeCodeDetectors.ZMod2_self_add_self (x : ZMod 2) : x + x = 0

In ZMod 2, any element added to itself is 0

def SpacetimeCodeDetectors.xorParity (m1 m2 : MeasOutcome) : ParityValue

The XOR (parity) of two measurement outcomes

Equations

• SpacetimeCodeDetectors.xorParity m1 m2 = m1 + m2

@[simp]

theorem SpacetimeCodeDetectors.xorParity_comm (m1 m2 : MeasOutcome) : xorParity m1 m2 = xorParity m2 m1

theorem SpacetimeCodeDetectors.xorParity_assoc (m1 m2 m3 : MeasOutcome) : xorParity (xorParity m1 m2) m3 = xorParity m1 (xorParity m2 m3)

@[simp]

theorem SpacetimeCodeDetectors.xorParity_self (m : MeasOutcome) : xorParity m m = 0

@[simp]

theorem SpacetimeCodeDetectors.xorParity_zero_right (m : MeasOutcome) : xorParity m 0 = m

@[simp]

theorem SpacetimeCodeDetectors.xorParity_zero_left (m : MeasOutcome) : xorParity 0 m = m

Section 3: Elementary Detector Types

The generating set consists of:

1. Bulk detectors: XOR of consecutive measurements of the same observable
2. Initial boundary detectors: Relate initialization to first measurement
3. Final boundary detectors: Relate last measurement to final readout

inductive SpacetimeCodeDetectors.OperatorType : Type

The type of operator involved in a detector

• originalCheck (j : ℕ) : OperatorType

  Original stabilizer check s_j

• gaussLaw (v : ℕ) : OperatorType

  Gauss law operator A_v

• flux (p : ℕ) : OperatorType

  Flux operator B_p

• deformedCheck (j : ℕ) : OperatorType

  Deformed check s̃_j

• edgeZ (e : ℕ) : OperatorType

  Single-qubit Z measurement on edge e

instance SpacetimeCodeDetectors.instDecidableEqOperatorType : DecidableEq OperatorType

Equations

• SpacetimeCodeDetectors.instDecidableEqOperatorType = SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq

def SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (x✝ x✝¹ : OperatorType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.originalCheck j) (SpacetimeCodeDetectors.OperatorType.gaussLaw v) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.originalCheck j) (SpacetimeCodeDetectors.OperatorType.flux p) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.originalCheck j) (SpacetimeCodeDetectors.OperatorType.deformedCheck j_1) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.originalCheck j) (SpacetimeCodeDetectors.OperatorType.edgeZ e) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.gaussLaw v) (SpacetimeCodeDetectors.OperatorType.originalCheck j) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.gaussLaw v) (SpacetimeCodeDetectors.OperatorType.flux p) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.gaussLaw v) (SpacetimeCodeDetectors.OperatorType.deformedCheck j) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.gaussLaw v) (SpacetimeCodeDetectors.OperatorType.edgeZ e) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.flux p) (SpacetimeCodeDetectors.OperatorType.originalCheck j) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.flux p) (SpacetimeCodeDetectors.OperatorType.gaussLaw v) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.flux p) (SpacetimeCodeDetectors.OperatorType.deformedCheck j) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.flux p) (SpacetimeCodeDetectors.OperatorType.edgeZ e) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.deformedCheck j) (SpacetimeCodeDetectors.OperatorType.originalCheck j_1) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.deformedCheck j) (SpacetimeCodeDetectors.OperatorType.gaussLaw v) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.deformedCheck j) (SpacetimeCodeDetectors.OperatorType.flux p) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.deformedCheck j) (SpacetimeCodeDetectors.OperatorType.edgeZ e) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.edgeZ e) (SpacetimeCodeDetectors.OperatorType.originalCheck j) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.edgeZ e) (SpacetimeCodeDetectors.OperatorType.gaussLaw v) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.edgeZ e) (SpacetimeCodeDetectors.OperatorType.flux p) = isFalse ⋯
• SpacetimeCodeDetectors.instDecidableEqOperatorType.decEq (SpacetimeCodeDetectors.OperatorType.edgeZ e) (SpacetimeCodeDetectors.OperatorType.deformedCheck j) = isFalse ⋯

inductive SpacetimeCodeDetectors.DetectorTimeType : Type

Detector time type classification

• bulk : DetectorTimeType

  Bulk: repeated measurement of same observable at t-1/2 and t+1/2

• initialBoundary : DetectorTimeType

  Initial boundary: initialization at t_i - 1/2, first measurement at t_i + 1/2

• finalBoundary : DetectorTimeType

  Final boundary: last measurement at t_o - 1/2, readout at t_o + 1/2

instance SpacetimeCodeDetectors.instDecidableEqDetectorTimeType : DecidableEq DetectorTimeType

Equations

• SpacetimeCodeDetectors.instDecidableEqDetectorTimeType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure SpacetimeCodeDetectors.ElementaryDetector : Type

An elementary detector: one of the generators of the detector group

• operatorType : OperatorType

  The type of operator involved

• time : TimeStep

  The time of the detector

• timeType : DetectorTimeType

  The time type (bulk or boundary)

def SpacetimeCodeDetectors.instDecidableEqElementaryDetector.decEq (x✝ x✝¹ : ElementaryDetector) : Decidable (x✝ = x✝¹)

Equations

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

instance SpacetimeCodeDetectors.instDecidableEqElementaryDetector : DecidableEq ElementaryDetector

Equations

• SpacetimeCodeDetectors.instDecidableEqElementaryDetector = SpacetimeCodeDetectors.instDecidableEqElementaryDetector.decEq

Section 4: Bulk Detector Parity

Lemma (bulk_detectors): Away from boundary times, detectors are pairs of consecutive measurements of the same check. The parity constraint is: outcome(C, time t) XOR outcome(C, time t+1) = 0

This follows from the fact that measuring the same observable twice on the same state yields the same result (projective measurement property).

structure SpacetimeCodeDetectors.BulkDetectorSpec (n : ℕ) : Type

A bulk detector specification: two consecutive measurements of the same observable

• support : Finset (Fin n)

  The observable being measured (represented by qubit support)

• time1 : TimeStep

  First measurement time (at t - 1/2)

• time2 : TimeStep

  Second measurement time (at t + 1/2)

• consecutive : self.time2 = self.time1 + 1

  Times are consecutive

theorem SpacetimeCodeDetectors.bulk_detector_parity_zero (m : MeasOutcome) : xorParity m m = 0

Bulk Detector Theorem (Part 1 of proof): XOR of identical outcomes is zero.

In error-free projective measurement, measuring the same observable twice on the same state gives identical outcomes. Hence m(t) XOR m(t+1) = 0.

def SpacetimeCodeDetectors.bulkDetectorParity (m1 m2 : MeasOutcome) : ParityValue

The parity of a bulk detector is the XOR of its two measurement outcomes

Equations

• SpacetimeCodeDetectors.bulkDetectorParity m1 m2 = SpacetimeCodeDetectors.xorParity m1 m2

theorem SpacetimeCodeDetectors.bulk_parity_zero_iff_equal (m1 m2 : MeasOutcome) : bulkDetectorParity m1 m2 = 0 ↔ m1 = m2

Bulk detector parity is zero iff outcomes are equal

Section 5: Initial Boundary Parity (t = t_i)

Lemma (initial_boundary_B): At t = t_i, edge qubits are initialized in |0⟩. Since |0⟩ is a +1 eigenstate of Z, we have:

• Z_e|0⟩_e = (+1)|0⟩_e for each edge e
• B_p = ∏{e ∈ p} Z_e has eigenvalue ∏{e ∈ p}(+1) = +1

Therefore the first measurement of B_p yields +1 (encoded as 0 in ZMod 2).

Lemma (initial_boundary_s): At t = t_i, s̃_j = s_j · ∏_{e ∈ γ_j} Z_e. Since Z_e|0⟩ = |0⟩ for all edges:

• ∏_{e ∈ γ_j} Z_e acts as +1 on the edge qubits
• Therefore s̃_j and s_j have the same eigenvalue on the initialized state

def SpacetimeCodeDetectors.z_eigenvalue_on_zero : MeasOutcome

Z measurement on |0⟩ state gives +1 (eigenvalue equation Z|0⟩ = +1·|0⟩)

Equations

• SpacetimeCodeDetectors.z_eigenvalue_on_zero = 0

@[simp]

theorem SpacetimeCodeDetectors.z_on_zero_is_plus_one : z_eigenvalue_on_zero = 0

theorem SpacetimeCodeDetectors.product_z_eigenvalue_on_zero (n : ℕ) (edges : Finset (Fin n)) : ∑ x ∈ edges, z_eigenvalue_on_zero = 0

Product of Z eigenvalues on |0⟩⊗n is +1 (product of +1's is +1). For any finite set of edges, (∏ Z_e)|0⟩^⊗|E| = (+1)|0⟩^⊗|E|. In ZMod 2: sum of zeros is zero.

theorem SpacetimeCodeDetectors.initial_Bp_parity_from_zero_init : have init_value := 0; have bp_value := 0; xorParity init_value bp_value = 0

Initial B_p Parity Theorem (Part 1 of proof): B_p measurement on |0⟩^⊗|p| yields +1.

This is because B_p = ∏_{e ∈ p} Z_e and each Z_e|0⟩_e = |0⟩_e.

The detector at t_i compares:

• Init outcome: +1 (from |0⟩ initialization, implicitly)
• B_p measurement at t_i + 1/2: +1 (from Z eigenvalue on |0⟩) Parity = 0 + 0 = 0

theorem SpacetimeCodeDetectors.initial_stilde_from_zero_init (sj_outcome : MeasOutcome) : have z_gamma_eigenvalue := 0; have stilde_outcome := sj_outcome + z_gamma_eigenvalue; xorParity sj_outcome stilde_outcome = 0

Initial s̃_j Parity Theorem (Part 1 of proof): The relation s̃_j = s_j · Z_γ with Z_γ = +1 on |0⟩.

At t_i - 1/2: measure s_j, get outcome m_sj At t_i + 1/2: measure s̃_j = s_j · Z_γ, get outcome m_stilde

Since Z_γ|0⟩ = |0⟩ (eigenvalue +1), we have: s̃_j = s_j · Z_γ acts the same as s_j on the code qubits when edges are in |0⟩.

Therefore m_stilde = m_sj and the parity m_sj XOR m_stilde = 0.

Section 6: Final Boundary Parity (t = t_o)

Lemma (final_boundary): At t = t_o, we measure B_p at t_o - 1/2, then perform Z_e measurements on all edges e ∈ p at t_o + 1/2.

By definition B_p = ∏_{e ∈ p} Z_e, so: B_p outcome = XOR of all Z_e outcomes

The detector compares B_p measurement with the product of Z_e measurements. Since they measure the same quantity, the parity is 0.

theorem SpacetimeCodeDetectors.final_Bp_equals_product_Ze (bp_outcome ze_product : MeasOutcome) (h_definition : bp_outcome = ze_product) : xorParity bp_outcome ze_product = 0

Final B_p Parity Theorem (Part 1 of proof): B_p measurement equals product of Z_e measurements. B_p = ∏_{e ∈ p} Z_e by definition, so measuring B_p and measuring all Z_e then taking the product (XOR in ZMod 2) give the same result.

If bp_outcome = ze_product (which holds by definition of B_p), then parity = 0.

theorem SpacetimeCodeDetectors.final_stilde_parity (stilde_outcome sj_outcome z_gamma_outcome : MeasOutcome) (h_relation : stilde_outcome = sj_outcome + z_gamma_outcome) : stilde_outcome + sj_outcome + z_gamma_outcome = 0

Final s̃_j Parity Theorem (Part 1 of proof): s̃_j = s_j · Z_γ relates the three measurements.

At t_o - 1/2: measure s̃_j, get m_stilde At t_o + 1/2: measure s_j, get m_sj; measure Z_e for e ∈ γ, get m_ze for each

The relation s̃_j = s_j · Z_γ means: m_stilde = m_sj + Σ m_ze (in ZMod 2)

The three-way parity: m_stilde + m_sj + (Σ m_ze) = 0

Section 7: Detector Configuration

structure SpacetimeCodeDetectors.DetectorConfig : Type

Configuration specifying the detector generating set

• region : GaugingRegion

  Time region boundaries

• numOriginalChecks : ℕ

  Number of original checks

• numVertices : ℕ

  Number of vertices (Gauss law operators)

• numCycles : ℕ

  Number of cycles/plaquettes (flux operators)

def SpacetimeCodeDetectors.bulkOriginalCheckDetectors (cfg : DetectorConfig) (t : TimeStep) : Finset ElementaryDetector

The set of bulk detectors for original checks (t < t_i and t > t_o)

Equations

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

def SpacetimeCodeDetectors.bulkDeformationDetectors (cfg : DetectorConfig) (t : TimeStep) : Finset ElementaryDetector

The set of bulk detectors during deformation (t_i < t < t_o)

Equations

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

def SpacetimeCodeDetectors.initialBoundaryDetectors (cfg : DetectorConfig) : Finset ElementaryDetector

Initial boundary detectors at t = t_i

Equations

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

def SpacetimeCodeDetectors.finalBoundaryDetectors (cfg : DetectorConfig) : Finset ElementaryDetector

Final boundary detectors at t = t_o

Equations

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

Section 8: Detector Existence Theorems (Part 2 of proof - Completeness)

theorem SpacetimeCodeDetectors.bulk_detector_exists_originalCheck (cfg : DetectorConfig) (t : TimeStep) (j : Fin cfg.numOriginalChecks) : { operatorType := OperatorType.originalCheck ↑j, time := t, timeType := DetectorTimeType.bulk } ∈ bulkOriginalCheckDetectors cfg t

Bulk detectors exist for original checks before/after deformation

theorem SpacetimeCodeDetectors.bulk_detector_exists_gaussLaw (cfg : DetectorConfig) (t : TimeStep) (v : Fin cfg.numVertices) : { operatorType := OperatorType.gaussLaw ↑v, time := t, timeType := DetectorTimeType.bulk } ∈ bulkDeformationDetectors cfg t

Bulk detectors exist for Gauss law operators during deformation

theorem SpacetimeCodeDetectors.bulk_detector_exists_flux (cfg : DetectorConfig) (t : TimeStep) (p : Fin cfg.numCycles) : { operatorType := OperatorType.flux ↑p, time := t, timeType := DetectorTimeType.bulk } ∈ bulkDeformationDetectors cfg t

Bulk detectors exist for flux operators during deformation

theorem SpacetimeCodeDetectors.bulk_detector_exists_deformedCheck (cfg : DetectorConfig) (t : TimeStep) (j : Fin cfg.numOriginalChecks) : { operatorType := OperatorType.deformedCheck ↑j, time := t, timeType := DetectorTimeType.bulk } ∈ bulkDeformationDetectors cfg t

Bulk detectors exist for deformed checks during deformation

theorem SpacetimeCodeDetectors.initial_boundary_detector_exists_flux (cfg : DetectorConfig) (p : Fin cfg.numCycles) : { operatorType := OperatorType.flux ↑p, time := cfg.region.t_i, timeType := DetectorTimeType.initialBoundary } ∈ initialBoundaryDetectors cfg

Initial boundary detectors exist for flux operators

theorem SpacetimeCodeDetectors.initial_boundary_detector_exists_deformedCheck (cfg : DetectorConfig) (j : Fin cfg.numOriginalChecks) : { operatorType := OperatorType.deformedCheck ↑j, time := cfg.region.t_i, timeType := DetectorTimeType.initialBoundary } ∈ initialBoundaryDetectors cfg

Initial boundary detectors exist for deformed checks

theorem SpacetimeCodeDetectors.final_boundary_detector_exists_flux (cfg : DetectorConfig) (p : Fin cfg.numCycles) : { operatorType := OperatorType.flux ↑p, time := cfg.region.t_o, timeType := DetectorTimeType.finalBoundary } ∈ finalBoundaryDetectors cfg

Final boundary detectors exist for flux operators

theorem SpacetimeCodeDetectors.final_boundary_detector_exists_deformedCheck (cfg : DetectorConfig) (j : Fin cfg.numOriginalChecks) : { operatorType := OperatorType.deformedCheck ↑j, time := cfg.region.t_o, timeType := DetectorTimeType.finalBoundary } ∈ finalBoundaryDetectors cfg

Final boundary detectors exist for deformed checks

Section 9: Main Generating Set Theorem

The main theorem establishes that the elementary detectors form a generating set. This follows from:

1. Each elementary detector has parity constraint satisfied (= 0) in error-free case
2. The detectors cover all possible consecutive measurement pairs (bulk)
3. The detectors cover all initialization/finalization transitions (boundary)

Any parity constraint that holds in the error-free gauging procedure can be expressed as an XOR of elementary detector constraints.

theorem SpacetimeCodeDetectors.detectors_generate_local : (∀ (m : MeasOutcome), bulkDetectorParity m m = 0) ∧ (have init_value := 0; have bp_value := 0; xorParity init_value bp_value = 0) ∧ (∀ (sj : MeasOutcome), have z_gamma := 0; have stilde := sj + z_gamma; xorParity sj stilde = 0) ∧ (∀ (bp ze : MeasOutcome), bp = ze → xorParity bp ze = 0) ∧ ∀ (stilde sj zgamma : MeasOutcome), stilde = sj + zgamma → stilde + sj + zgamma = 0

Main Theorem (Lemma 3): The elementary detector parities are all zero in the error-free case.

This establishes that each elementary detector is a valid detector:

• Bulk detectors: m(O,t) = m(O,t+1) by projective measurement
• Initial B_p: B_p = +1 on |0⟩^⊗|E| by Z eigenvalue
• Initial s̃_j: s̃_j = s_j when Z_γ = +1 on |0⟩
• Final detectors: B_p and s̃_j decompose into Z_e products

Section 10: Coverage by Time Region

theorem SpacetimeCodeDetectors.detectors_exist_before (cfg : DetectorConfig) (t : TimeStep) (_ht : cfg.region.isBefore t) (j : Fin cfg.numOriginalChecks) : ∃ e ∈ bulkOriginalCheckDetectors cfg t, e.operatorType = OperatorType.originalCheck ↑j ∧ e.timeType = DetectorTimeType.bulk

Detectors exist for times before deformation: bulk original check detectors

theorem SpacetimeCodeDetectors.detectors_exist_during (cfg : DetectorConfig) (t : TimeStep) (_ht : cfg.region.isDuring t) : (∀ (v : Fin cfg.numVertices), ∃ e ∈ bulkDeformationDetectors cfg t, e.operatorType = OperatorType.gaussLaw ↑v ∧ e.timeType = DetectorTimeType.bulk) ∧ (∀ (p : Fin cfg.numCycles), ∃ e ∈ bulkDeformationDetectors cfg t, e.operatorType = OperatorType.flux ↑p ∧ e.timeType = DetectorTimeType.bulk) ∧ ∀ (j : Fin cfg.numOriginalChecks), ∃ e ∈ bulkDeformationDetectors cfg t, e.operatorType = OperatorType.deformedCheck ↑j ∧ e.timeType = DetectorTimeType.bulk

Detectors exist during deformation: Gauss law, flux, and deformed check detectors

theorem SpacetimeCodeDetectors.detectors_exist_initial_boundary (cfg : DetectorConfig) : (∀ (p : Fin cfg.numCycles), ∃ e ∈ initialBoundaryDetectors cfg, e.operatorType = OperatorType.flux ↑p ∧ e.timeType = DetectorTimeType.initialBoundary) ∧ ∀ (j : Fin cfg.numOriginalChecks), ∃ e ∈ initialBoundaryDetectors cfg, e.operatorType = OperatorType.deformedCheck ↑j ∧ e.timeType = DetectorTimeType.initialBoundary

Detectors exist at initial boundary t_i

theorem SpacetimeCodeDetectors.detectors_exist_final_boundary (cfg : DetectorConfig) : (∀ (p : Fin cfg.numCycles), ∃ e ∈ finalBoundaryDetectors cfg, e.operatorType = OperatorType.flux ↑p ∧ e.timeType = DetectorTimeType.finalBoundary) ∧ ∀ (j : Fin cfg.numOriginalChecks), ∃ e ∈ finalBoundaryDetectors cfg, e.operatorType = OperatorType.deformedCheck ↑j ∧ e.timeType = DetectorTimeType.finalBoundary

Detectors exist at final boundary t_o

theorem SpacetimeCodeDetectors.detectors_exist_after (cfg : DetectorConfig) (t : TimeStep) (_ht : cfg.region.isAfter t) (j : Fin cfg.numOriginalChecks) : ∃ e ∈ bulkOriginalCheckDetectors cfg t, e.operatorType = OperatorType.originalCheck ↑j ∧ e.timeType = DetectorTimeType.bulk

Detectors exist for times after deformation: bulk original check detectors

Section 11: Fault Detection Properties

structure SpacetimeCodeDetectors.FaultLocation : Type

A fault location in spacetime

• time : TimeStep

  Time of the fault

• qubit : ℕ

  Qubit index affected

theorem SpacetimeCodeDetectors.bulk_detector_detects_fault (m_before m_after : MeasOutcome) (h_different : m_before ≠ m_after) : bulkDetectorParity m_before m_after ≠ 0

Bulk detectors detect faults: if measurements differ, parity is nonzero

theorem SpacetimeCodeDetectors.initial_boundary_detects_fault (init_outcome bp_outcome : MeasOutcome) (h_different : init_outcome ≠ bp_outcome) : xorParity init_outcome bp_outcome ≠ 0

Initial boundary detectors detect initialization faults

theorem SpacetimeCodeDetectors.final_boundary_detects_fault (bp_outcome ze_product : MeasOutcome) (h_mismatch : bp_outcome ≠ ze_product) : xorParity bp_outcome ze_product ≠ 0

Final boundary detectors detect measurement faults

Section 12: Detector Counting

def SpacetimeCodeDetectors.countBulkDetectorsBefore (cfg : DetectorConfig) : ℕ

Count of bulk detectors at a single time step before/after deformation

Equations

• SpacetimeCodeDetectors.countBulkDetectorsBefore cfg = cfg.numOriginalChecks

def SpacetimeCodeDetectors.countBulkDetectorsDuring (cfg : DetectorConfig) : ℕ

Count of bulk detectors at a single time step during deformation

Equations

• SpacetimeCodeDetectors.countBulkDetectorsDuring cfg = cfg.numVertices + cfg.numCycles + cfg.numOriginalChecks

def SpacetimeCodeDetectors.countInitialBoundaryDetectors (cfg : DetectorConfig) : ℕ

Count of boundary detectors at t = t_i

Equations

• SpacetimeCodeDetectors.countInitialBoundaryDetectors cfg = cfg.numCycles + cfg.numOriginalChecks

def SpacetimeCodeDetectors.countFinalBoundaryDetectors (cfg : DetectorConfig) : ℕ

Count of boundary detectors at t = t_o

Equations

• SpacetimeCodeDetectors.countFinalBoundaryDetectors cfg = cfg.numCycles + cfg.numOriginalChecks

Section 13: Non-Adjacent Detector Factorization (Part 2 of proof - Completeness)

Completeness proof - Away from boundaries: Detectors comparing non-adjacent times (t, t+k) factor as: (t, t+1) × (t+1, t+2) × ... × (t+k-1, t+k)

theorem SpacetimeCodeDetectors.nonadjacent_factors_to_adjacent (m₀ mₖ : MeasOutcome) (outcomes : ℕ → MeasOutcome) (k : ℕ) (_hk : k ≥ 1) (h₀ : outcomes 0 = m₀) (hₖ : outcomes k = mₖ) (h_all_equal : ∀ i < k, outcomes i = outcomes (i + 1)) : m₀ = mₖ

Non-adjacent time comparison factors into adjacent comparisons

theorem SpacetimeCodeDetectors.parity_telescope_nat (n : ℕ) (outcomes : ℕ → MeasOutcome) : ∑ i ∈ Finset.range (n + 1), bulkDetectorParity (outcomes i) (outcomes (i + 1)) = bulkDetectorParity (outcomes 0) (outcomes (n + 1))

XOR of consecutive parities telescopes to endpoints. This is a conceptual theorem about the telescoping property: in ZMod 2, (a₀ + a₁) + (a₁ + a₂) + ... + (aₙ + aₙ₊₁) = a₀ + aₙ₊₁ because middle terms appear twice and cancel (x + x = 0 in ZMod 2).

Section 14: Helper Lemmas

theorem SpacetimeCodeDetectors.boundary_not_interior (R : GaugingRegion) : ¬(R.isStart R.t_i ∧ R.isDuring R.t_i) ∧ ¬(R.isEnd R.t_o ∧ R.isDuring R.t_o)

Boundary times are distinct from interior times

theorem SpacetimeCodeDetectors.interior_nonempty (R : GaugingRegion) (h : R.t_o > R.t_i + 1) : ∃ (t : TimeStep), R.isDuring t

The time region has at least one interior point if t_o > t_i + 1

theorem SpacetimeCodeDetectors.detectorTimeType_trichotomy (tt : DetectorTimeType) : tt = DetectorTimeType.bulk ∨ tt = DetectorTimeType.initialBoundary ∨ tt = DetectorTimeType.finalBoundary

All three detector time types are distinct

theorem SpacetimeCodeDetectors.detectorTimeType_decidable (tt : DetectorTimeType) : tt = DetectorTimeType.bulk ∧ tt ≠ DetectorTimeType.initialBoundary ∧ tt ≠ DetectorTimeType.finalBoundary ∨ tt ≠ DetectorTimeType.bulk ∧ tt = DetectorTimeType.initialBoundary ∧ tt ≠ DetectorTimeType.finalBoundary ∨ tt ≠ DetectorTimeType.bulk ∧ tt ≠ DetectorTimeType.initialBoundary ∧ tt = DetectorTimeType.finalBoundary

The three detector time types exhaust all possibilities

Section 15: Summary Statement

Lemma (SpacetimeCodeDetectors): The following form a generating set of local detectors in the fault-tolerant gauging measurement procedure.

The proof consists of two parts:

Part 1 - Verification that each is a valid detector:

• bulk_detector_parity_zero: Repeated measurements give XOR = 0 (projective measurement)
• initial_Bp_parity_from_zero_init: B_p|0⟩ = +1|0⟩ (Z eigenvalue on |0⟩)
• initial_stilde_from_zero_init: s̃_j = s_j·Z_γ with Z_γ = +1 on |0⟩
• final_Bp_equals_product_Ze: B_p = ∏Z_e by definition
• final_stilde_parity: s̃_j = s_j·Z_γ decomposition

Part 2 - Completeness:

• detectors_exist_before/during/after: Coverage of all time regions
• detectors_exist_initial/final_boundary: Coverage of boundary transitions
• nonadjacent_factors_to_adjacent: Non-adjacent comparisons factor into adjacent ones
• parity_telescope: XOR of adjacent parities telescopes to endpoints

The local relations assumption (no space-only meta-checks in the original code) is implicit in the formalization.

theorem SpacetimeCodeDetectors.spacetime_code_detectors_generating : (∀ (m : MeasOutcome), bulkDetectorParity m m = 0) ∧ xorParity 0 0 = 0 ∧ (∀ (sj : MeasOutcome), xorParity sj (sj + 0) = 0) ∧ (∀ (bp ze : MeasOutcome), bp = ze → xorParity bp ze = 0) ∧ (∀ (stilde sj zgamma : MeasOutcome), stilde = sj + zgamma → stilde + sj + zgamma = 0) ∧ (∀ (cfg : DetectorConfig) (t : TimeStep) (j : Fin cfg.numOriginalChecks), cfg.region.isBefore t → ∃ e ∈ bulkOriginalCheckDetectors cfg t, e.operatorType = OperatorType.originalCheck ↑j) ∧ (∀ (cfg : DetectorConfig), (∀ (p : Fin cfg.numCycles), ∃ e ∈ initialBoundaryDetectors cfg, e.operatorType = OperatorType.flux ↑p) ∧ ∀ (j : Fin cfg.numOriginalChecks), ∃ e ∈ initialBoundaryDetectors cfg, e.operatorType = OperatorType.deformedCheck ↑j) ∧ ∀ (cfg : DetectorConfig), (∀ (p : Fin cfg.numCycles), ∃ e ∈ finalBoundaryDetectors cfg, e.operatorType = OperatorType.flux ↑p) ∧ ∀ (j : Fin cfg.numOriginalChecks), ∃ e ∈ finalBoundaryDetectors cfg, e.operatorType = OperatorType.deformedCheck ↑j

Summary theorem: The elementary detectors form a generating set

Summary

This formalization captures Lemma 3 (SpacetimeCodeDetectors) from the fault-tolerant gauging measurement procedure:

1. Detector Types:

• Original check detectors s_j^t (before/after deformation)
• Gauss law detectors A_v^t (during deformation)
• Flux detectors B_p^t (during deformation)
• Deformed check detectors s̃_j^t (during deformation)
• Initial boundary detectors B_p^{t_i} and s̃_j^{t_i}
• Final boundary detectors B_p^{t_o} and s̃_j^{t_o}

2. Verification (Part 1):

• Bulk detectors: Same observable measured twice gives same outcome
• B_p^{t_i}: |0⟩ is +1 eigenstate of all Z_e, so B_p|0⟩ = +1|0⟩
• s̃_j^{t_i}: Z_γ acts as +1 on |0⟩ edges, so s̃_j = s_j on initialized state
• B_p^{t_o}: B_p = ∏Z_e by definition, outcomes match
• s̃_j^{t_o}: s̃_j = s_j·Z_γ relates three measurements

3. Completeness (Part 2):

• Detectors cover all time regions (before, during, after)
• Boundary detectors cover initialization/finalization transitions
• Non-adjacent time comparisons factor into adjacent ones
• No space-only local relations assumed in original code

Key theorems:

• detectors_generate_local: Main generating set property
• bulk_detector_parity_zero: Bulk detector validity
• initial_Bp_parity_from_zero_init: Initial B_p validity
• initial_stilde_from_zero_init: Initial s̃_j validity
• final_Bp_equals_product_Ze: Final B_p validity
• final_stilde_parity: Final s̃_j validity
• spacetime_code_detectors_generating: Summary theorem