Remark 15: Flux Check Measurement Frequency

Statement

The proof of Theorem 2 (fault-tolerance) holds even if the flux checks B_p are measured much less frequently than every round, or even not directly measured at all.

Why this works:

1. B_p can be inferred from initialization (|0⟩e at t_i) and final readout (Z_e at t_o) without direct measurement, since B_p = ∏{e ∈ p} Z_e and |0⟩_e is a +1 eigenstate of Z_e.
2. The distance bound from Lemma 3 does not require B_p measurements; it only requires B_p to be stabilizers of the code.
3. The time-fault analysis (Lemma 6) shows A_v measurement faults are the bottleneck for time-fault distance, not B_p.

Caveats:

1. Without frequent B_p measurements, detector cells become large (spanning t_i to t_o).
2. Large detectors prevent achieving a threshold against random noise.
3. For small fixed code instances, this approach may be practical.

Main Results

• flux_inferred_from_init_readout: B_p information is captured by boundary detectors
• space_distance_independent_of_flux_measurements: Lem 3 only needs B_p as stabilizers
• time_fault_bottleneck_is_gauss: A_v strings determine the time-fault distance
• flux_fault_preserves_sign: B_p faults cannot flip the gauging sign
• flux_boundary_detector_weight: Boundary detector has weight |p| + 1
• repeated_vs_boundary_detector_weight: Repeated detectors have weight 2

Point 1: B_p Information from Boundary Detectors

The flux check B_p = ∏_{e ∈ p} Z_e can be inferred from edge initialization and final Z_e readout. The boundary detectors from Lemma 4 encode this:

• fluxInitDetector: pairs edge init events with the first B_p measurement
• fluxUngaugeDetector: pairs the last B_p measurement with individual Z_e readouts

Even without any Phase 2 flux measurements, the composition of these two boundary detectors gives a detector pairing edge inits with edge readouts.

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

The flux init detector (B_p^{t_i}) captures the relationship between edge initialization and the first flux measurement. Edge init events for e ∈ p are included in this detector, encoding B_p = ∏_{e ∈ p} Z_e via |0⟩ initialization.

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

The flux ungauge detector (B_p^{t_o}) captures the relationship between the last flux measurement and individual Z_e readouts for e ∈ p.

theorem FluxCheckMeasurementFrequency.flux_init_contains_first_measurement {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) : FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.flux p ⟨0, ⋯⟩) ∈ (proc.fluxInitDetector p ⟨0, ⋯⟩ ⋯).measurements

The flux init detector also contains the first B_p measurement in Phase 2. This single measurement, together with the edge inits, suffices to capture B_p information — no repeated B_p measurements needed.

theorem FluxCheckMeasurementFrequency.flux_ungauge_contains_last_measurement {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) : FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.flux p ⟨proc.d - 1, ⋯⟩) ∈ (proc.fluxUngaugeDetector p ⟨proc.d - 1, ⋯⟩ ⋯).measurements

The flux ungauge detector contains the last B_p measurement.

Point 2: Lemma 3 (Space Distance) is Independent of Flux Measurements

The distance bound d* ≥ min(h(G), 1) · d from Lemma 3 depends only on the algebraic structure of the deformed code (flux operators being stabilizers), not on whether they are actively measured. The key inputs are:

• B_p ∈ stabilizer group (algebraic, from Lem_1 flux_mem_stabilizerGroup)
• Boundary/coboundary exactness (graph-theoretic)
• Cheeger expansion (graph-theoretic)

theorem FluxCheckMeasurementFrequency.space_distance_independent_of_flux_measurements {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} (origCode : StabilizerCode V) (hJ : origCode.I = J) (hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (hconn : G.Connected) (hcard : 2 ≤ Fintype.card V) (hexact : ∀ γ ∈ (GraphMaps.secondCoboundaryMap G cycles).ker, ∃ (c : V → ZMod 2), (GraphMaps.coboundaryMap G) c = γ) (hexact_boundary : ∀ δ ∈ (GraphMaps.boundaryMap G).ker, δ ∈ (GraphMaps.secondBoundaryMap G cycles).range) (hexp : DesiderataForGraphG.SufficientExpansion G) (hL_logical : origCode.isLogicalOp GaugingMeasurementCorrectness.logicalOpV) (hDeformedHasLogicals : ∃ (P : PauliOp (GaussFlux.ExtQubit G)), (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).isLogicalOp P) : origCode.distance ≤ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).distance

Lemma 3's distance bound requires only that B_p operators are elements of the deformed stabilizer group, which is an algebraic fact proven in Lem_1 (flux_mem_stabilizerGroup). No measurement of B_p is needed for d* ≥ d.

Point 3: Time-Fault Bottleneck is A_v, not B_p

Lemma 6 shows the time-fault distance equals d, determined entirely by A_v measurement strings. The proof uses:

• Repeated Gauss detectors enforce all-or-none for each A_v
• A full A_v string (all d rounds faulted) has weight d
• Only A_v faults can flip the gauging sign σ = ∑_v ε_v
• B_p faults cannot flip σ (they don't affect Gauss measurements)

theorem FluxCheckMeasurementFrequency.time_fault_bottleneck_is_gauss {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) : TimeFaultDistance.timeFaultDistance proc proc.detectorOfIndex (SpacetimeLogicalFault.PreservesGaugingSign proc) ≤ proc.d

The time-fault distance is determined by A_v measurement strings, not B_p. The canonical minimum-weight pure-time logical fault is a single A_v string of weight d. This is the upper bound from Lemma 6.

theorem FluxCheckMeasurementFrequency.gauss_string_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) (v : V) : (TimeFaultDistance.gaussStringFault proc v).weight = proc.d

The A_v measurement string has weight exactly d.

theorem FluxCheckMeasurementFrequency.gauss_string_is_syndrome_free {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) : SpacetimeLogicalFault.IsSyndromeFreeGauging proc proc.detectorOfIndex (TimeFaultDistance.gaussStringFault proc v)

The A_v string is syndrome-free: consecutive repeated Gauss detectors see paired flips that cancel. This does not involve any flux detectors.

theorem FluxCheckMeasurementFrequency.gauss_string_flips_sign {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)

The A_v string flips the gauging sign when d is odd.

theorem FluxCheckMeasurementFrequency.flux_fault_preserves_sign {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) (hflux : ∀ tf ∈ F.timeFaults, ∃ (p : C) (r : Fin proc.d), tf = { measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.flux p r) }) : SpacetimeLogicalFault.PreservesGaugingSign proc F

B_p measurement faults cannot flip the gauging sign σ. The sign σ = ∑_v ε_v is defined as a sum over Gauss measurement outcomes only (gaussSignFlip sums over v : V and r : Fin d, checking if A_v measurement at round r is faulted). A fault whose timeFaults contain only flux measurements contributes 0 to this sum: no A_v measurement is faulted.

theorem FluxCheckMeasurementFrequency.gaussSignFlip_ignores_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) (v : V) : SpacetimeLogicalFault.gaussSignFlip proc (TimeFaultDistance.gaussStringFault proc v) = ∑ w : V, ∑ r : Fin proc.d, if { measurement := FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw w r) } ∈ (TimeFaultDistance.gaussStringFault proc v).timeFaults then 1 else 0

The gauging sign is determined entirely by A_v measurement faults. This is expressed by the structure of gaussSignFlip: it sums indicators of A_v membership in timeFaults, ignoring all non-Gauss faults.

theorem FluxCheckMeasurementFrequency.time_fault_distance_eq_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) (v : V) (hodd : Odd proc.d) (hV : Nonempty V) : TimeFaultDistance.timeFaultDistance proc proc.detectorOfIndex (SpacetimeLogicalFault.PreservesGaugingSign proc) = proc.d

The full time-fault distance result from Lemma 6: timeFaultDistance = d.

Caveats: Large Detector Cells

Without frequent B_p measurements, the boundary detectors (fluxInitDetector, fluxUngaugeDetector) span from t_i to t_o rather than between consecutive rounds.

theorem FluxCheckMeasurementFrequency.repeated_vs_boundary_detector_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) (p : C) (r r' : Fin proc.d) (hr : ↑r + 1 = ↑r') : (proc.phase2RepeatedDetector_flux p r r' hr).measurements.card = 2

The key quantitative difference: repeated flux detectors have weight 2 (two consecutive B_p measurements), while boundary flux detectors have weight proportional to |p| + 1 (all edge inits/readouts plus one B_p measurement). This means removing repeated flux detectors enlarges the detector cells.

theorem FluxCheckMeasurementFrequency.flux_boundary_detector_spans_full_duration {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) : proc.phase2Start ≤ proc.phase3Start ∧ proc.phase3Start - proc.phase2Start = proc.d

Without repeated flux detectors, the boundary detectors span the full Phase 2 duration d. The init detector covers t_i to the first Phase 2 round, and the ungauge detector covers the last Phase 2 round to t_o.

theorem FluxCheckMeasurementFrequency.boundary_larger_than_repeated {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) (hr : ↑r + 1 = ↑r') (hcycle_large : 2 ≤ {e : ↑G.edgeSet | e ∈ cycles p}.card) : (proc.phase2RepeatedDetector_flux p r r' hr).measurements.card < {e : ↑G.edgeSet | e ∈ cycles p}.card + 1

Large detector cells: the number of measurements in a boundary detector (|p| + 1 for flux init) is strictly greater than a repeated detector (2), as soon as the cycle has at least 2 edges. This quantifies the caveat that large detectors accumulate more potential faults per detector cell.

Summary: Distance Proof Structure Without Flux Measurements

The spacetime fault-distance proof (Theorem 2) decomposes into:

1. Space distance (Lemma 3): d* ≥ min(h(G),1) · d — uses only algebraic properties of B_p as stabilizers, not measurements.
2. Time distance (Lemma 6): d_time = d — determined entirely by A_v measurement strings. B_p faults don't affect the gauging sign.

Therefore, omitting B_p measurements preserves d_spacetime = d. The only cost is larger detector cells, which affects the threshold but not the distance guarantee.

theorem FluxCheckMeasurementFrequency.space_distance_from_stabilizer_algebra {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} (origCode : StabilizerCode V) (hJ : origCode.I = J) (_hchecks_eq : ∀ (j : J), origCode.check (⋯ ▸ j) = checks j) (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (p : C) : DeformedCode.fluxChecks G cycles p ∈ (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).stabilizerGroup

The space-distance bound d* ≥ d (Lemma 3) requires h(G) ≥ 1 and exactness. No measurement of flux checks B_p is needed — only their algebraic presence as stabilizers of the deformed code.

theorem FluxCheckMeasurementFrequency.flux_in_centralizer_algebraically {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} (data : DeformedCode.DeformedCodeData G checks) (hcyc : ∀ (c₀ : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c₀ ∧ v ∈ ↑e}.card) (hcomm : ∀ (i j : J), (checks i).PauliCommute (checks j)) (p : C) : (DeformedCodeChecks.deformedStabilizerCode G cycles checks data hcyc hcomm).inCentralizer (DeformedCode.fluxChecks G cycles p)

Flux operators are also in the centralizer (commute with all checks), which is the property actually used in Lemma 3.