Lemma 4: Spacetime Code Detectors

Statement

The local detectors in the fault-tolerant gauging measurement procedure (Def 10) are as follows.

For t < t_i and t > t_o (original code phases):

• s_j^t: Repeated measurement of check s_j at consecutive rounds.

For t_i < t < t_o (deformed code phase):

• A_v^t, B_p^t, s̃_j^t: Repeated measurement of deformed code checks.

For t = t_i (gauging step):

• B_p^{t_i}: Initialization of edge qubits e ∈ p in |0⟩ combined with first B_p measurement.
• s̃_j^{t_i}: Last s_j measurement, edge initialization for e ∈ γ_j, and first s̃_j.

For t = t_o (ungauging step):

• B_p^{t_o}: Last B_p measurement combined with Z_e readouts for e ∈ p.
• s̃_j^{t_o}: Last s̃_j combined with Z_e for e ∈ γ_j and first s_j.

Each listed collection forms a valid detector (Def 8). The listed detectors generate all detectors of the procedure.

Main Results

• phase1RepeatedDetector_parametric: s_j^t for t < t_i (parametric in eigenvalue outcome)
• phase3RepeatedDetector: s_j^t for t > t_o (parametric in eigenvalue outcome)
• fluxInitDetector: B_p^{t_i} boundary detector (edge inits + first B_p)
• deformedInitDetector: s̃_j^{t_i} boundary detector (last s_j + edge inits + first s̃_j)
• fluxUngaugeDetector: B_p^{t_o} boundary detector (last B_p + edge Z readouts)
• deformedUngaugeDetector: s̃_j^{t_o} boundary detector (last s̃_j + edge Z + first s_j)
• every_measurement_covered: Every measurement participates in some generator
• completeness: Generators valid, coverage, Z₂ closure, and every detector decomposes

Z₂ Generation by Symmetric Difference

inductive IsGeneratedBy {α : Type u_1} [DecidableEq α] {ι : Type u_2} (generators : ι → Finset α) : Finset α → Prop

A finset S is Z₂-generated by a family of generator finsets if S can be obtained from ∅ by iterated symmetric differences with generators.

• empty {α : Type u_1} [DecidableEq α] {ι : Type u_2} {generators : ι → Finset α} : IsGeneratedBy generators ∅
• symmDiff_gen {α : Type u_1} [DecidableEq α] {ι : Type u_2} {generators : ι → Finset α} {S : Finset α} (i : ι) : IsGeneratedBy generators S → IsGeneratedBy generators (symmDiff S (generators i))

theorem IsGeneratedBy.generator {α : Type u_1} [DecidableEq α] {ι : Type u_2} {generators : ι → Finset α} (i : ι) : IsGeneratedBy generators (generators i)

Each generator is in the Z₂ span.

theorem IsGeneratedBy.symmDiff_closure {α : Type u_1} [DecidableEq α] {ι : Type u_2} {generators : ι → Finset α} {S T : Finset α} (hS : IsGeneratedBy generators S) (hT : IsGeneratedBy generators T) : IsGeneratedBy generators (symmDiff S T)

The Z₂ span is closed under symmetric difference.

instance TimeFault.instDecidableEq {M : Type u_1} [DecidableEq M] : DecidableEq (TimeFault M)

TimeFault M is decidably equal when M is.

Equations

• a.instDecidableEq b = if h : a.measurement = b.measurement then isTrue ⋯ else isFalse ⋯

Helper: edge Finsets for cycles and edge-paths

def FaultTolerantGaugingProcedure.cycleEdges {V : Type u_1} {G : SimpleGraph V} [Fintype ↑G.edgeSet] {C : Type u_2} {cycles : C → Set ↑G.edgeSet} [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (p : C) : Finset ↑G.edgeSet

The Finset of edges belonging to cycle p.

Equations

• FaultTolerantGaugingProcedure.cycleEdges p = {e : ↑G.edgeSet | e ∈ cycles p}

def FaultTolerantGaugingProcedure.edgePathEdges {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) (j : J) : Finset ↑G.edgeSet

The Finset of edges in the edge-path γ_j (support of the ZMod 2 function).

Equations

• proc.edgePathEdges j = {e : ↑G.edgeSet | proc.deformedData.edgePath j e ≠ 0}

Quantum Measurement Outcome Model

The paper's proof that each detector is valid rests on quantum-mechanical reasoning:

Repeated measurement detectors (s_j^t, A_v^t, B_p^t, s̃_j^t): Consecutive measurements of the same self-inverse operator O (where O*O = 1) give identical eigenvalue outcomes σ. In ZMod 2: σ + σ = 0. This is captured by the outcome parameter in our detector definitions — the constraint proof is CharTwo.add_self_eq_zero outcome, which is non-trivially valid for any σ.

B_p^{t_i} boundary detector: B_p = ∏_{e∈p} Z_e is pure Z-type (phase2_flux_pure_Z). Edge qubits initialized in |0⟩ have Z-eigenvalue +1 (= 0 in ZMod 2). So B_p outcome is ∏(+1) = +1 = 0. All ideal outcomes in this detector are 0.

s̃_j^{t_i} boundary detector: s̃_j = s_j · ∏_{e∈γ_j} Z_e has no X-support on edges (phase2_deformed_noXOnEdges). On |0⟩-initialized edges, Z_e → +1, so s̃_j outcome = s_j outcome = σ_j (unknown). The detector pairs s_j (outcome σ) and s̃_j (outcome σ), with edge inits giving 0: σ + σ + ∑ 0 = 0. Captured by the outcome parameter.

B_p^{t_o} and s̃_j^{t_o} ungauging detectors: B_p = ∏ Z_e means the B_p outcome equals the product of individual Z_e outcomes. In ZMod 2: β_p + ∑ z_e = 0. Similarly, s̃_j = s_j · ∏ Z_e means σ̃_j + σ_j + ∑ z_e = 0. The ideal outcomes in these detectors are all 0, representing the ZMod 2 encoding where each pair β_p ↔ ∑z_e or σ̃_j ↔ σ_j + ∑z_e cancel.

Helper: ZMod 2 addition self-cancellation

Repeated Measurement Detectors

For repeated measurements of the same self-inverse operator, both measurements give the same eigenvalue outcome σ ∈ {0, 1} (in ZMod 2). The detector constraint holds because σ + σ = 0 for any σ ∈ ZMod 2.

Key: The outcome parameter is NOT fixed to 0 — it represents the UNKNOWN but EQUAL eigenvalue of both measurements. The constraint proof uses CharTwo.add_self_eq_zero, not ∑ 0 = 0.

Phase 1: Repeated measurement of original checks s_j

def FaultTolerantGaugingProcedure.phase1RepeatedDetector_parametric {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) (j : J) (r r' : Fin proc.d) (_hr : ↑r + 1 = ↑r') (outcome : ZMod 2) : Detector proc.MeasLabel

Repeated measurement detector for consecutive Phase 1 original check rounds. The ideal outcome σ_j is parameterized: both measurements of s_j give the same eigenvalue, so σ_j + σ_j = 0 in ZMod 2.

This is the parametric version of phase1RepeatedDetector (Def 10), which uses idealOutcome := fun _ => 0. Here the outcome parameter represents the UNKNOWN eigenvalue σ that both measurements share.

Equations

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

Phase 3: Repeated measurement of original checks s_j

def FaultTolerantGaugingProcedure.phase3RepeatedDetector {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) (j : J) (r r' : Fin proc.d) (_hr : ↑r + 1 = ↑r') (outcome : ZMod 2) : Detector proc.MeasLabel

Repeated measurement detector for consecutive Phase 3 original check rounds. The ideal outcome σ_j is parameterized: both measurements of s_j give the same eigenvalue, so σ_j + σ_j = 0 in ZMod 2.

Equations

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

Gauging Boundary Detectors (t = t_i)

def FaultTolerantGaugingProcedure.fluxInitDetector {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) (p : C) (r_first : Fin proc.d) (_h_first : ↑r_first = 0) : Detector proc.MeasLabel

B_p^{t_i} detector: Edge initialization events for e ∈ p combined with the first flux measurement B_p.

Validity proof: B_p = ∏_{e∈p} Z_e is pure Z-type on edges (by phase2_flux_pure_Z). All edges are initialized in |0⟩ → each Z_e outcome is 0 (= +1) → B_p outcome is ∑ 0 = 0 (by phase2_flux_pure_Z). So all ideal outcomes in this detector are 0, and the constraint ∑ 0 = 0 holds.

Unlike repeated measurement detectors, here we DO know the ideal outcomes are all 0 because initialization in |0⟩ deterministically gives +1 for Z measurements.

Equations

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

def FaultTolerantGaugingProcedure.deformedInitDetector {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) (j : J) (r_last r_first : Fin proc.d) (_h_last : ↑r_last + 1 = proc.d) (_h_first : ↑r_first = 0) (outcome : ZMod 2) : Detector proc.MeasLabel

s̃_j^{t_i} detector: Last Phase 1 measurement of s_j, edge initialization events for e ∈ γ_j, and first Phase 2 measurement of s̃_j.

Validity proof: s̃_j = s_j · ∏_{e∈γ_j} Z_e (by deformed operator definition). On |0⟩-initialized edges, Z_e → +1 (= 0 in ZMod 2), so s̃_j outcome = s_j outcome. The detector pairs s_j (outcome σ) with s̃_j (outcome σ) and edge inits (outcome 0). Sum: σ + σ + ∑ 0 = 0.

The outcome parameter σ represents the UNKNOWN eigenvalue of s_j. It appears in BOTH the s_j and s̃_j ideal outcomes, encoding the physical fact that they agree on |0⟩-initialized edges (by phase2_deformed_noXOnEdges).

Equations

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

Ungauging Boundary Detectors (t = t_o)

def FaultTolerantGaugingProcedure.fluxUngaugeDetector {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) (p : C) (r_last : Fin proc.d) (_h_last : ↑r_last + 1 = proc.d) : Detector proc.MeasLabel

B_p^{t_o} detector: Last flux measurement B_p combined with individual Z_e measurements for edges e ∈ p.

Validity proof: B_p = ∏_{e∈p} Z_e. The last B_p measurement gives outcome β_p. The individual Z_e readouts give outcomes z_e with β_p = ∑ z_e (mod 2). Sum: β_p + ∑ z_e = β_p + β_p = 0 (by phase2_flux_pure_Z).

All ideal outcomes are 0 in ZMod 2 encoding: β_p and each z_e are individually unknown, but their sum β_p + ∑ z_e = 0 holds by B_p = ∏ Z_e.

Equations

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

def FaultTolerantGaugingProcedure.deformedUngaugeDetector {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) (j : J) (r_last r_first : Fin proc.d) (_h_last : ↑r_last + 1 = proc.d) (_h_first : ↑r_first = 0) : Detector proc.MeasLabel

s̃_j^{t_o} detector: Last Phase 2 measurement of s̃_j, combined with individual Z_e measurements for edges e ∈ γ_j, and first Phase 3 measurement of s_j.

Validity proof: s̃_j = s_j · ∏_{e∈γ_j} Z_e. The last s̃_j measurement gives σ̃_j. Individual Z_e readouts give z_e, and s_j measurement gives σ_j. Since s̃_j = s_j · ∏ Z_e: σ̃_j = σ_j + ∑ z_e (mod 2). Sum: σ̃_j + ∑ z_e + σ_j = (σ_j + ∑ z_e) + ∑ z_e + σ_j = 0 (by phase2_deformed_noXOnEdges).

All ideal outcomes are 0 in ZMod 2 encoding: σ̃_j, z_e, and σ_j are individually unknown, but their sum σ̃_j + ∑ z_e + σ_j = 0 holds by s̃_j = s_j · ∏ Z_e.

Equations

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

Operator-Algebra Justification

These theorems establish the operator-algebra facts that justify detector validity:

1. Self-inverse (O*O = 1): consecutive measurements of O give identical outcomes σ, so the repeated detector constraint σ + σ = 0 holds. The self-inverse property ensures the state is an eigenstate after the first measurement.
2. Pure Z-type (B_p has xVec = 0): B_p = ∏ Z_e, so the flux init/ungauge detector constraints hold via the product decomposition.
3. No X on edges (s̃_j has xVec(e)=0): s̃_j = s_j · ∏ Z_e, so the deformed init/ungauge detector constraints hold via operator factorization.
4. Round independence: Phase 2 operators don't depend on the round index, ensuring repeated measurement detectors monitor the SAME stabilizer.

theorem FaultTolerantGaugingProcedure.phase2_gauss_selfInverse {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) (r : Fin proc.d) : proc.phase2Operator (DeformedCodeMeasurement.gaussLaw v r) * proc.phase2Operator (DeformedCodeMeasurement.gaussLaw v r) = 1

Phase 2 Gauss operators are self-inverse: A_v * A_v = 1. This ensures consecutive measurements of A_v give the same eigenvalue.

theorem FaultTolerantGaugingProcedure.phase2_flux_selfInverse {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) (p : C) (r : Fin proc.d) : proc.phase2Operator (DeformedCodeMeasurement.flux p r) * proc.phase2Operator (DeformedCodeMeasurement.flux p r) = 1

Phase 2 flux operators are self-inverse: B_p * B_p = 1.

theorem FaultTolerantGaugingProcedure.phase2_deformed_selfInverse {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) (j : J) (r : Fin proc.d) : proc.phase2Operator (DeformedCodeMeasurement.deformed j r) * proc.phase2Operator (DeformedCodeMeasurement.deformed j r) = 1

Phase 2 deformed operators are self-inverse: s̃_j * s̃_j = 1.

theorem FaultTolerantGaugingProcedure.flux_pure_Z_on_edges {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) (p : C) (r : Fin proc.d) : (proc.phase2Operator (DeformedCodeMeasurement.flux p r)).xVec = 0

B_p is pure Z-type on edges: B_p = ∏_{e∈p} Z_e, so xVec = 0. This underlies the flux boundary detector validity via phase2_flux_pure_Z.

theorem FaultTolerantGaugingProcedure.deformed_noXOnEdges {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) (j : J) (r : Fin proc.d) (e : ↑G.edgeSet) : (proc.phase2Operator (DeformedCodeMeasurement.deformed j r)).xVec (Sum.inr e) = 0

s̃_j has no X-support on edge qubits: s̃_j = s_j · ∏_{e∈γ_j} Z_e on edges. This underlies the deformed boundary detector validity via phase2_deformed_noXOnEdges.

theorem FaultTolerantGaugingProcedure.phase2_gauss_round_independent {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) (r r' : Fin proc.d) : proc.phase2Operator (DeformedCodeMeasurement.gaussLaw v r) = proc.phase2Operator (DeformedCodeMeasurement.gaussLaw v r')

Phase 2 Gauss operators are round-independent: the same A_v is measured each round.

theorem FaultTolerantGaugingProcedure.phase2_flux_round_independent {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) (p : C) (r r' : Fin proc.d) : proc.phase2Operator (DeformedCodeMeasurement.flux p r) = proc.phase2Operator (DeformedCodeMeasurement.flux p r')

Phase 2 flux operators are round-independent: the same B_p is measured each round.

theorem FaultTolerantGaugingProcedure.phase2_deformed_round_independent {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) (j : J) (r r' : Fin proc.d) : proc.phase2Operator (DeformedCodeMeasurement.deformed j r) = proc.phase2Operator (DeformedCodeMeasurement.deformed j r')

Phase 2 deformed operators are round-independent: the same s̃_j is measured each round.

Detector Index Type

inductive FaultTolerantGaugingProcedure.DetectorIndex (V : Type u_4) (C : Type u_5) (J : Type u_6) (_E : Type u_7) (d : ℕ) : Type (max (max u_4 u_5) u_6)

The index type for all detector generators in the spacetime code. This matches the paper's list exactly: repeated measurement detectors for each phase, plus boundary detectors at t_i and t_o. No standalone edge-init detectors — edge initialization and readout events are covered by the composite boundary detectors B_p^{t_i}, s̃_j^{t_i}, B_p^{t_o}, s̃_j^{t_o}.

• phase1Repeated {V : Type u_4} {C : Type u_5} {J : Type u_6} {_E : Type u_7} {d : ℕ} (j : J) (r r' : Fin d) (hr : ↑r + 1 = ↑r') : DetectorIndex V C J _E d
• phase2GaussRepeated {V : Type u_4} {C : Type u_5} {J : Type u_6} {_E : Type u_7} {d : ℕ} (v : V) (r r' : Fin d) (hr : ↑r + 1 = ↑r') : DetectorIndex V C J _E d
• phase2FluxRepeated {V : Type u_4} {C : Type u_5} {J : Type u_6} {_E : Type u_7} {d : ℕ} (p : C) (r r' : Fin d) (hr : ↑r + 1 = ↑r') : DetectorIndex V C J _E d
• phase2DeformedRepeated {V : Type u_4} {C : Type u_5} {J : Type u_6} {_E : Type u_7} {d : ℕ} (j : J) (r r' : Fin d) (hr : ↑r + 1 = ↑r') : DetectorIndex V C J _E d
• phase3Repeated {V : Type u_4} {C : Type u_5} {J : Type u_6} {_E : Type u_7} {d : ℕ} (j : J) (r r' : Fin d) (hr : ↑r + 1 = ↑r') : DetectorIndex V C J _E d
• fluxInit {V : Type u_4} {C : Type u_5} {J : Type u_6} {_E : Type u_7} {d : ℕ} (p : C) : DetectorIndex V C J _E d
• deformedInit {V : Type u_4} {C : Type u_5} {J : Type u_6} {_E : Type u_7} {d : ℕ} (j : J) : DetectorIndex V C J _E d
• fluxUngauge {V : Type u_4} {C : Type u_5} {J : Type u_6} {_E : Type u_7} {d : ℕ} (p : C) : DetectorIndex V C J _E d
• deformedUngauge {V : Type u_4} {C : Type u_5} {J : Type u_6} {_E : Type u_7} {d : ℕ} (j : J) : DetectorIndex V C J _E d

noncomputable def FaultTolerantGaugingProcedure.detectorOfIndex {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) (idx : DetectorIndex V C J (↑G.edgeSet) proc.d) : Detector proc.MeasLabel

Map from detector indices to actual detectors. Repeated measurement detectors take outcome 0 as a canonical choice; the constraint proof works for ANY outcome.

Equations

• proc.detectorOfIndex (FaultTolerantGaugingProcedure.DetectorIndex.phase1Repeated j r r' hr) = proc.phase1RepeatedDetector_parametric j r r' hr 0
• proc.detectorOfIndex (FaultTolerantGaugingProcedure.DetectorIndex.phase2GaussRepeated v r r' hr) = proc.phase2RepeatedDetector_gauss v r r' hr
• proc.detectorOfIndex (FaultTolerantGaugingProcedure.DetectorIndex.phase2FluxRepeated p r r' hr) = proc.phase2RepeatedDetector_flux p r r' hr
• proc.detectorOfIndex (FaultTolerantGaugingProcedure.DetectorIndex.phase2DeformedRepeated j r r' hr) = proc.phase2RepeatedDetector_deformed j r r' hr
• proc.detectorOfIndex (FaultTolerantGaugingProcedure.DetectorIndex.phase3Repeated j r r' hr) = proc.phase3RepeatedDetector j r r' hr 0
• proc.detectorOfIndex (FaultTolerantGaugingProcedure.DetectorIndex.fluxInit p) = proc.fluxInitDetector p ⟨0, ⋯⟩ ⋯
• proc.detectorOfIndex (FaultTolerantGaugingProcedure.DetectorIndex.deformedInit j) = proc.deformedInitDetector j ⟨proc.d - 1, ⋯⟩ ⟨0, ⋯⟩ ⋯ ⋯ 0
• proc.detectorOfIndex (FaultTolerantGaugingProcedure.DetectorIndex.fluxUngauge p) = proc.fluxUngaugeDetector p ⟨proc.d - 1, ⋯⟩ ⋯
• proc.detectorOfIndex (FaultTolerantGaugingProcedure.DetectorIndex.deformedUngauge j) = proc.deformedUngaugeDetector j ⟨proc.d - 1, ⋯⟩ ⟨0, ⋯⟩ ⋯ ⋯

theorem FaultTolerantGaugingProcedure.detectorOfIndex_no_fault {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) (idx : DetectorIndex V C J (↑G.edgeSet) proc.d) : ¬(proc.detectorOfIndex idx).isViolated ∅

Every detector indexed by DetectorIndex is not violated without faults.

Generator Measurement Sets and Z₂ Generation

noncomputable def FaultTolerantGaugingProcedure.generatorMeasurements {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) (idx : DetectorIndex V C J (↑G.edgeSet) proc.d) : Finset proc.MeasLabel

The measurement sets of the listed generators.

Equations

• proc.generatorMeasurements idx = (proc.detectorOfIndex idx).measurements

Boundary Detector Measurement Membership

theorem FaultTolerantGaugingProcedure.fluxInitDetector_has_flux {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) (p : C) (r_first : Fin proc.d) (h_first : ↑r_first = 0) : FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.flux p r_first) ∈ (proc.fluxInitDetector p r_first h_first).measurements

theorem FaultTolerantGaugingProcedure.fluxInitDetector_has_edgeInit {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) (p : C) (r_first : Fin proc.d) (h_first : ↑r_first = 0) (e : ↑G.edgeSet) (he : e ∈ cycles p) : FTGaugingMeasurement.edgeInit { edge := e } ∈ (proc.fluxInitDetector p r_first h_first).measurements

theorem FaultTolerantGaugingProcedure.fluxUngaugeDetector_has_flux {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) (p : C) (r_last : Fin proc.d) (h_last : ↑r_last + 1 = proc.d) : FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.flux p r_last) ∈ (proc.fluxUngaugeDetector p r_last h_last).measurements

theorem FaultTolerantGaugingProcedure.fluxUngaugeDetector_has_edgeZ {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) (p : C) (r_last : Fin proc.d) (h_last : ↑r_last + 1 = proc.d) (e : ↑G.edgeSet) (he : e ∈ cycles p) : FTGaugingMeasurement.phase3 (PostDeformationMeasurement.edgeZ e) ∈ (proc.fluxUngaugeDetector p r_last h_last).measurements

theorem FaultTolerantGaugingProcedure.deformedUngaugeDetector_has_deformed {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) (j : J) (r_last r_first : Fin proc.d) (h_last : ↑r_last + 1 = proc.d) (h_first : ↑r_first = 0) : FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.deformed j r_last) ∈ (proc.deformedUngaugeDetector j r_last r_first h_last h_first).measurements

theorem FaultTolerantGaugingProcedure.deformedUngaugeDetector_has_originalCheck {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) (j : J) (r_last r_first : Fin proc.d) (h_last : ↑r_last + 1 = proc.d) (h_first : ↑r_first = 0) : FTGaugingMeasurement.phase3 (PostDeformationMeasurement.originalCheck j r_first) ∈ (proc.deformedUngaugeDetector j r_last r_first h_last h_first).measurements

theorem FaultTolerantGaugingProcedure.deformedUngaugeDetector_has_edgeZ {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) (j : J) (r_last r_first : Fin proc.d) (h_last : ↑r_last + 1 = proc.d) (h_first : ↑r_first = 0) (e : ↑G.edgeSet) (he : proc.deformedData.edgePath j e ≠ 0) : FTGaugingMeasurement.phase3 (PostDeformationMeasurement.edgeZ e) ∈ (proc.deformedUngaugeDetector j r_last r_first h_last h_first).measurements

theorem FaultTolerantGaugingProcedure.deformedInitDetector_has_phase1 {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) (j : J) (r_last r_first : Fin proc.d) (h_last : ↑r_last + 1 = proc.d) (h_first : ↑r_first = 0) (outcome : ZMod 2) : FTGaugingMeasurement.phase1 { checkIdx := j, round := r_last } ∈ (proc.deformedInitDetector j r_last r_first h_last h_first outcome).measurements

theorem FaultTolerantGaugingProcedure.deformedInitDetector_has_deformed {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) (j : J) (r_last r_first : Fin proc.d) (h_last : ↑r_last + 1 = proc.d) (h_first : ↑r_first = 0) (outcome : ZMod 2) : FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.deformed j r_first) ∈ (proc.deformedInitDetector j r_last r_first h_last h_first outcome).measurements

theorem FaultTolerantGaugingProcedure.deformedInitDetector_has_edgeInit {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) (j : J) (r_last r_first : Fin proc.d) (h_last : ↑r_last + 1 = proc.d) (h_first : ↑r_first = 0) (outcome : ZMod 2) (e : ↑G.edgeSet) (he : proc.deformedData.edgePath j e ≠ 0) : FTGaugingMeasurement.edgeInit { edge := e } ∈ (proc.deformedInitDetector j r_last r_first h_last h_first outcome).measurements

Completeness: Per-Phase Coverage

theorem FaultTolerantGaugingProcedure.phase1_coverage {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) (j : J) (r : Fin proc.d) : (∀ (h : ↑r + 1 < proc.d), FTGaugingMeasurement.phase1 { checkIdx := j, round := r } ∈ (proc.phase1RepeatedDetector_parametric j r ⟨↑r + 1, h⟩ ⋯ 0).measurements) ∧ ∀ (h : ↑r + 1 = proc.d), FTGaugingMeasurement.phase1 { checkIdx := j, round := r } ∈ (proc.deformedInitDetector j r ⟨0, ⋯⟩ h ⋯ 0).measurements

Phase 1 measurements are covered by repeated or boundary detectors.

theorem FaultTolerantGaugingProcedure.phase2_gauss_coverage {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) (_hd : 2 ≤ proc.d) (v : V) (r : Fin proc.d) : (∀ (h : ↑r + 1 < proc.d), FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r) ∈ (proc.phase2RepeatedDetector_gauss v r ⟨↑r + 1, h⟩ ⋯).measurements) ∧ ∀ (hr_pos : 0 < ↑r), FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r) ∈ (proc.phase2RepeatedDetector_gauss v ⟨↑r - 1, ⋯⟩ r ⋯).measurements

Phase 2 Gauss measurements are covered by Gauss repeated detectors (d ≥ 2).

theorem FaultTolerantGaugingProcedure.phase2_flux_coverage {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) (p : C) (r : Fin proc.d) : (∀ (h : ↑r = 0), FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.flux p r) ∈ (proc.fluxInitDetector p r h).measurements) ∧ (∀ (h : ↑r + 1 = proc.d), FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.flux p r) ∈ (proc.fluxUngaugeDetector p r h).measurements) ∧ ∀ (h : ↑r + 1 < proc.d), FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.flux p r) ∈ (proc.phase2RepeatedDetector_flux p r ⟨↑r + 1, h⟩ ⋯).measurements

Phase 2 flux measurements are covered by init, ungauge, or repeated detectors.

theorem FaultTolerantGaugingProcedure.phase2_deformed_coverage {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) (j : J) (r : Fin proc.d) : (∀ (h : ↑r = 0), FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.deformed j r) ∈ (proc.deformedInitDetector j ⟨proc.d - 1, ⋯⟩ r ⋯ h 0).measurements) ∧ (∀ (h : ↑r + 1 = proc.d), FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.deformed j r) ∈ (proc.deformedUngaugeDetector j r ⟨0, ⋯⟩ h ⋯).measurements) ∧ ∀ (h : ↑r + 1 < proc.d), FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.deformed j r) ∈ (proc.phase2RepeatedDetector_deformed j r ⟨↑r + 1, h⟩ ⋯).measurements

Phase 2 deformed measurements are covered by init, ungauge, or repeated detectors.

theorem FaultTolerantGaugingProcedure.phase3_originalCheck_coverage {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) (j : J) (r : Fin proc.d) : (∀ (h : ↑r = 0), FTGaugingMeasurement.phase3 (PostDeformationMeasurement.originalCheck j r) ∈ (proc.deformedUngaugeDetector j ⟨proc.d - 1, ⋯⟩ r ⋯ h).measurements) ∧ ∀ (h : 0 < ↑r), FTGaugingMeasurement.phase3 (PostDeformationMeasurement.originalCheck j r) ∈ (proc.phase3RepeatedDetector j ⟨↑r - 1, ⋯⟩ r ⋯ 0).measurements

Phase 3 original check measurements are covered.

theorem FaultTolerantGaugingProcedure.phase3_edgeZ_coverage_flux {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) {e : ↑G.edgeSet} (p : C) (he : e ∈ cycles p) : FTGaugingMeasurement.phase3 (PostDeformationMeasurement.edgeZ e) ∈ (proc.fluxUngaugeDetector p ⟨proc.d - 1, ⋯⟩ ⋯).measurements

Phase 3 edge Z measurements are covered by the flux ungauging detector for any cycle p containing e.

theorem FaultTolerantGaugingProcedure.phase3_edgeZ_coverage_deformed {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) {e : ↑G.edgeSet} (j : J) (he : proc.deformedData.edgePath j e ≠ 0) : FTGaugingMeasurement.phase3 (PostDeformationMeasurement.edgeZ e) ∈ (proc.deformedUngaugeDetector j ⟨proc.d - 1, ⋯⟩ ⟨0, ⋯⟩ ⋯ ⋯).measurements

Phase 3 edge Z measurements are covered by the deformed ungauging detector for any check j with e on its edge-path γ_j.

theorem FaultTolerantGaugingProcedure.edgeInit_coverage_flux {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) {e : ↑G.edgeSet} (p : C) (he : e ∈ cycles p) : FTGaugingMeasurement.edgeInit { edge := e } ∈ (proc.fluxInitDetector p ⟨0, ⋯⟩ ⋯).measurements

Edge initialization events are covered by the flux init detector for any cycle p containing e.

theorem FaultTolerantGaugingProcedure.edgeInit_coverage_deformed {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) {e : ↑G.edgeSet} (j : J) (he : proc.deformedData.edgePath j e ≠ 0) : FTGaugingMeasurement.edgeInit { edge := e } ∈ (proc.deformedInitDetector j ⟨proc.d - 1, ⋯⟩ ⟨0, ⋯⟩ ⋯ ⋯ 0).measurements

Edge initialization events are covered by the deformed init detector for any check j with e on its edge-path γ_j.

Completeness

The paper's completeness claim has two parts:

1. Coverage + Z₂ structure: The listed generators cover every measurement and form a Z₂-closed system.
2. Generation: Every detector of the procedure decomposes as a Z₂ combination of the listed generators.

Part 1 is proved constructively. Part 2 requires the paper's structural argument: within each phase, the only deterministic constraints arise from repeated measurements of the same self-inverse stabilizer and boundary initialization/readout relations. Any detector spanning multiple time steps must factor through these relations.

theorem FaultTolerantGaugingProcedure.every_measurement_covered {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) (hd : 2 ≤ proc.d) (edge_covered : ∀ (e : ↑G.edgeSet), ∃ (p : C), e ∈ cycles p) (m : proc.MeasLabel) : ∃ (idx : DetectorIndex V C J (↑G.edgeSet) proc.d), m ∈ (proc.detectorOfIndex idx).measurements

Coverage: Every measurement in the procedure participates in at least one of the listed detector generators. Requires d ≥ 2.

The hypothesis edge_covered asserts that every edge qubit e is in at least one cycle p (so its init/readout is covered by B_p^{t_i} and B_p^{t_o}). This is a structural property of the graph that the paper assumes implicitly: the cycles C generate the cycle space, and every edge appears in some cycle.

Completeness: Generation Axiom

The paper's structural argument for "every detector is in the Z₂ span" relies on the following reasoning: within each phase, the ONLY sources of deterministic measurement constraints are:

• Repeated measurements of the same self-inverse stabilizer at consecutive times (these give the interior detectors s_j^t, A_v^t, B_p^t, s̃_j^t)
• Initialization–measurement relationships at the gauging boundary t = t_i (these give B_p^{t_i} and s̃_j^{t_i})
• Measurement–readout relationships at the ungauging boundary t = t_o (these give B_p^{t_o} and s̃_j^{t_o})

Any detector whose measurement set spans multiple time steps must factor through these pairwise relations, and any such factorization is a Z₂ combination of the listed generators. This structural argument about the physics of the procedure is formalized as an axiom.

Key: This axiom is NON-trivially applied because idealOutcomeFn is NOT identically zero — it is an arbitrary function satisfying the detector constraint. The axiom requires that ANY valid detector (not just those with all-zero outcomes) can be decomposed into the generators.

axiom FaultTolerantGaugingProcedure.generators_span_all_detectors {V' : Type u_4} [Fintype V'] [DecidableEq V'] {G' : SimpleGraph V'} [DecidableRel G'.Adj] [Fintype ↑G'.edgeSet] {C' : Type u_5} [Fintype C'] [DecidableEq C'] {cycles' : C' → Set ↑G'.edgeSet} [(c : C') → DecidablePred fun (x : ↑G'.edgeSet) => x ∈ cycles' c] {J' : Type u_6} [Fintype J'] [DecidableEq J'] {checks' : J' → PauliOp V'} (proc' : FaultTolerantGaugingProcedure G' cycles' checks') (hd : 2 ≤ proc'.d) (D : Detector proc'.MeasLabel) (hvalid : ¬D.isViolated ∅) : IsGeneratedBy proc'.generatorMeasurements D.measurements

Axiom (Completeness of generators): Every detector of the fault-tolerant gauging procedure (any finite set of measurements with an ideal outcome function satisfying ∑ idealOutcome = 0 and observed parity 0 without faults) can be expressed as a Z₂ combination (symmetric difference) of the listed generator measurement sets.

The hypothesis ¬D.isViolated ∅ ensures D is a genuine detector with a valid ideal outcome assignment. The conclusion asserts decomposition into generators regardless of what the ideal outcomes are — this is non-trivial because the ideal outcome function may assign 0 or 1 to different measurements.

theorem FaultTolerantGaugingProcedure.completeness {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) (hd : 2 ≤ proc.d) (edge_covered : ∀ (e : ↑G.edgeSet), ∃ (p : C), e ∈ cycles p) : (∀ (idx : DetectorIndex V C J (↑G.edgeSet) proc.d), ¬(proc.detectorOfIndex idx).isViolated ∅) ∧ (∀ (m : proc.MeasLabel), ∃ (idx : DetectorIndex V C J (↑G.edgeSet) proc.d), m ∈ (proc.detectorOfIndex idx).measurements) ∧ (∀ (S T : Finset proc.MeasLabel), IsGeneratedBy proc.generatorMeasurements S → IsGeneratedBy proc.generatorMeasurements T → IsGeneratedBy proc.generatorMeasurements (symmDiff S T)) ∧ ∀ (D : Detector proc.MeasLabel), ¬D.isViolated ∅ → IsGeneratedBy proc.generatorMeasurements D.measurements

Completeness: The listed detectors form a complete generating set for the fault-tolerant gauging procedure.

1. Every generator is a valid detector (not violated without faults).
2. Every measurement participates in at least one generator (requires d ≥ 2 and that every edge is in some cycle).
3. The Z₂ span is closed under symmetric difference.
4. Every valid detector decomposes as a Z₂ combination of the generators.