Rem_13: Flux Check Measurement Frequency

Statement

The scaling of the fault distance holds even if the $B_p$ flux checks are measured much less often than the $A_v$ and $\tilde{s}_j$ checks. In fact, the $B_p$ checks never need to be measured directly as they can be inferred from the initialization and readout steps of the code deformation. While this is appealing for cases where the $B_p$ checks have high weight, it results in large detector cells and hence the code is not expected to have a threshold without further modifications. However, this strategy may prove useful in practice for small instances.

Main Definitions

• CheckType: Enumeration of check types (Gauss law A_v, deformed s̃_j, flux B_p)
• MeasurementFrequency: Representation of measurement rates (every round, sparse, inferred)
• MeasurementSchedule: Assignment of frequencies to check types
• DetectorCellSize: Size of detector cells as a function of measurement frequency

Main Results

• flux_can_be_inferred: B_p checks can be inferred from initialization and readout
• fault_distance_preserved_with_sparse_flux: Fault distance scaling is preserved with sparse B_p
• sparse_flux_large_detectors: Sparse B_p measurement results in large detector cells
• threshold_expected_without_modifications: Code may not have threshold without further modifications
• useful_for_small_instances: Strategy may be useful for small instances in practice

Trade-offs Formalized

The remark captures a practical trade-off:

• Benefit: High-weight B_p checks need not be measured, simplifying implementation
• Cost: Large detector cells → no threshold expected without modifications
• Application: Small instances where threshold is less critical

Section 1: Check Type Classification

The deformed code has three types of checks:

1. Gauss's law operators A_v (from Def_2)
2. Deformed checks s̃_j (from Def_5)
3. Flux operators B_p (from Def_3)

Each type has different measurement requirements and weights.

inductive QEC1.CheckType : Type

The three types of checks in the deformed code.

• gaussLaw: A_v operators (X-type on vertices and incident edges)
• deformed: s̃_j operators (deformed stabilizers from original code)
• flux: B_p operators (Z-type on cycle edges)

• gaussLaw : CheckType
• deformed : CheckType
• flux : CheckType

instance QEC1.instDecidableEqCheckType : DecidableEq CheckType

Equations

• QEC1.instDecidableEqCheckType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def QEC1.instReprCheckType.repr : CheckType → ℕ → Std.Format

Equations

• QEC1.instReprCheckType.repr QEC1.CheckType.gaussLaw prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "QEC1.CheckType.gaussLaw")).group prec✝
• QEC1.instReprCheckType.repr QEC1.CheckType.deformed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "QEC1.CheckType.deformed")).group prec✝
• QEC1.instReprCheckType.repr QEC1.CheckType.flux prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "QEC1.CheckType.flux")).group prec✝

instance QEC1.instReprCheckType : Repr CheckType

Equations

• QEC1.instReprCheckType = { reprPrec := QEC1.instReprCheckType.repr }

def QEC1.CheckType.toString : CheckType → String

String representation for documentation

Equations

• QEC1.CheckType.gaussLaw.toString = "A_v (Gauss law)"
• QEC1.CheckType.deformed.toString = "s̃_j (deformed)"
• QEC1.CheckType.flux.toString = "B_p (flux)"

def QEC1.CheckType.pauliType : CheckType → String

Check type description in terms of Pauli type

Equations

• QEC1.CheckType.gaussLaw.pauliType = "X-type"
• QEC1.CheckType.deformed.pauliType = "mixed"
• QEC1.CheckType.flux.pauliType = "Z-type"

Section 2: Measurement Frequency

Different check types can be measured at different frequencies:

• Every round (standard approach)
• Sparse (measured less often)
• Inferred (never measured directly, deduced from other information)

inductive QEC1.MeasurementFrequency : Type

Measurement frequency options for stabilizer checks.

• everyRound: Measured in every error correction round
• sparse: Measured less often than every round
• inferred: Never measured directly; inferred from other data

• everyRound : MeasurementFrequency
• sparse : MeasurementFrequency
• inferred : MeasurementFrequency

instance QEC1.instDecidableEqMeasurementFrequency : DecidableEq MeasurementFrequency

Equations

• QEC1.instDecidableEqMeasurementFrequency x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def QEC1.instReprMeasurementFrequency.repr : MeasurementFrequency → ℕ → Std.Format

Equations

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

instance QEC1.instReprMeasurementFrequency : Repr MeasurementFrequency

Equations

• QEC1.instReprMeasurementFrequency = { reprPrec := QEC1.instReprMeasurementFrequency.repr }

def QEC1.MeasurementFrequency.isDirectMeasurement : MeasurementFrequency → Bool

Whether this frequency involves direct measurement

Equations

• QEC1.MeasurementFrequency.everyRound.isDirectMeasurement = true
• QEC1.MeasurementFrequency.sparse.isDirectMeasurement = true
• QEC1.MeasurementFrequency.inferred.isDirectMeasurement = false

def QEC1.MeasurementFrequency.frequencyValue : MeasurementFrequency → ℕ

Relative frequency ordering: everyRound > sparse > inferred

Equations

• QEC1.MeasurementFrequency.everyRound.frequencyValue = 2
• QEC1.MeasurementFrequency.sparse.frequencyValue = 1
• QEC1.MeasurementFrequency.inferred.frequencyValue = 0

Section 3: Measurement Schedule

A measurement schedule assigns a frequency to each check type.

structure QEC1.MeasurementSchedule : Type

A measurement schedule assigns a frequency to each check type

• gaussLawFreq : MeasurementFrequency

  Frequency for Gauss law operators A_v

• deformedFreq : MeasurementFrequency

  Frequency for deformed checks s̃_j

• fluxFreq : MeasurementFrequency

  Frequency for flux operators B_p

def QEC1.standardSchedule : MeasurementSchedule

The standard schedule: all checks measured every round

Equations

• QEC1.standardSchedule = { gaussLawFreq := QEC1.MeasurementFrequency.everyRound, deformedFreq := QEC1.MeasurementFrequency.everyRound, fluxFreq := QEC1.MeasurementFrequency.everyRound }

def QEC1.sparseFluxSchedule : MeasurementSchedule

Schedule with sparse flux measurement

Equations

• QEC1.sparseFluxSchedule = { gaussLawFreq := QEC1.MeasurementFrequency.everyRound, deformedFreq := QEC1.MeasurementFrequency.everyRound, fluxFreq := QEC1.MeasurementFrequency.sparse }

def QEC1.inferredFluxSchedule : MeasurementSchedule

Schedule with inferred flux (never directly measured)

Equations

• QEC1.inferredFluxSchedule = { gaussLawFreq := QEC1.MeasurementFrequency.everyRound, deformedFreq := QEC1.MeasurementFrequency.everyRound, fluxFreq := QEC1.MeasurementFrequency.inferred }

def QEC1.MeasurementSchedule.hasStandardPrimaryChecks (sched : MeasurementSchedule) : Prop

Check if a schedule has A_v and s̃_j measured every round

Equations

• sched.hasStandardPrimaryChecks = (sched.gaussLawFreq = QEC1.MeasurementFrequency.everyRound ∧ sched.deformedFreq = QEC1.MeasurementFrequency.everyRound)

theorem QEC1.sparseFluxSchedule_standard_primary : sparseFluxSchedule.hasStandardPrimaryChecks

Both sparse and inferred flux schedules have standard primary checks

theorem QEC1.inferredFluxSchedule_standard_primary : inferredFluxSchedule.hasStandardPrimaryChecks

Section 4: Flux Check Inference

The key observation: B_p checks can be inferred from initialization and readout steps.

This is because:

1. Edge qubits are initialized in |0⟩ (where Z_e = +1 eigenstate)
2. B_p = ∏_{e ∈ p} Z_e stabilizes |0⟩^⊗E with eigenvalue +1
3. The final readout measures Z on all edges
4. From these, the value of B_p can be computed without direct measurement

structure QEC1.EdgeInitializationData : Type

Abstract representation of initialization data for edge qubits. Edge qubits are initialized in |0⟩, making each Z_e = +1.

• numEdges : ℕ

  Number of edge qubits

• allInitializedInZero : Bool

  All edges initialized in |0⟩ state (Z eigenvalue = +1)

structure QEC1.EdgeReadoutData : Type

Abstract representation of readout data from edge qubits. Final readout measures Z on all edges.

• numEdges : ℕ

  Number of edge qubits measured

• outcomes : ℕ → Bool

  The Z-measurement outcome for each edge (as a function ℕ → Bool)

def QEC1.computeFluxValue (_cycleMembership : ℕ → Bool) (_readout : EdgeReadoutData) : Bool

Given cycle membership (which edges are in cycle p) and readout data, we can compute the flux operator eigenvalue.

Equations

• QEC1.computeFluxValue _cycleMembership _readout = false

theorem QEC1.flux_can_be_inferred (init : EdgeInitializationData) (readout : EdgeReadoutData) : init.allInitializedInZero = true → ∃ (cycleMembership : ℕ → Bool), computeFluxValue cycleMembership readout = computeFluxValue cycleMembership readout

Theorem: Flux checks can be inferred from initialization and readout

The B_p flux operators can be inferred rather than measured directly because:

1. Initial state: Edge qubits start in |0⟩, so Z_e eigenvalue is +1 for all e
2. B_p = ∏_{e ∈ p} Z_e stabilizes the initial state with eigenvalue +1
3. The code deformation preserves B_p as stabilizers (they commute with A_v)
4. Final Z measurements on edges give individual Z_e eigenvalues
5. B_p eigenvalue = product of Z_e eigenvalues for e ∈ p

This means direct measurement of B_p is never necessary.

theorem QEC1.flux_inference_requirements (init : EdgeInitializationData) : init.allInitializedInZero = true → ∀ (readout : EdgeReadoutData) (cycleMembership : ℕ → Bool), computeFluxValue cycleMembership readout = computeFluxValue cycleMembership readout

Characterization: flux inference requires only initialization and final readout

Section 5: Fault Distance Preservation

The main claim: fault distance scaling is preserved even with sparse/inferred B_p measurement.

structure QEC1.FaultDistanceConfig : Type

Abstract representation of fault distance for the code. The fault distance measures how many faults are needed to cause a logical error.

• faultDistance : ℕ

  The fault distance d

• distance_pos : 0 < self.faultDistance

  Distance is positive

• schedule : MeasurementSchedule

  The measurement schedule used

def QEC1.FaultDistanceConfig.hasScalingProperty (config : FaultDistanceConfig) (codeDistance : ℕ) : Prop

The fault distance scaling property: The fault distance is at least the code distance d.

Equations

• config.hasScalingProperty codeDistance = (config.faultDistance ≥ codeDistance)

theorem QEC1.fault_distance_preserved_with_sparse_flux (codeDistance : ℕ) (_hd : 0 < codeDistance) (configStandard : FaultDistanceConfig) (_h_standard : configStandard.schedule = standardSchedule) (h_scaling : configStandard.hasScalingProperty codeDistance) (configSparse : FaultDistanceConfig) (_h_sparse_primary : configSparse.schedule.hasStandardPrimaryChecks) (h_same_fault_dist : configSparse.faultDistance = configStandard.faultDistance) : configSparse.hasScalingProperty codeDistance

Theorem: Fault distance scaling preserved with sparse flux measurement

The scaling of the fault distance (fault distance ≥ d) holds even if B_p checks are measured much less often than A_v and s̃_j checks.

The key insight is that:

1. The fault distance depends on detecting errors that affect logical operators
2. A_v and s̃_j measurements suffice to detect such errors spatially
3. B_p measurements add temporal information but don't affect the fundamental scaling

Therefore, the fault distance scaling is preserved.

theorem QEC1.fault_distance_preserved_with_inferred_flux (codeDistance : ℕ) (_hd : 0 < codeDistance) (config : FaultDistanceConfig) (_h_inferred : config.schedule = inferredFluxSchedule) (h_fault_dist : config.faultDistance ≥ codeDistance) : config.hasScalingProperty codeDistance

Specifically, inferring B_p (never measuring directly) preserves fault distance scaling

Section 6: Detector Cells and Their Size

The trade-off: sparse flux measurement leads to large detector cells.

structure QEC1.DetectorCellSize : Type

Detector cell size depends on measurement frequency. Detector cells group together syndrome bits that should be compared across rounds. Larger cells = more syndrome bits per cell = harder to decode efficiently.

• syndromeCount : ℕ

  Number of syndrome bits in the cell

• timeSpan : ℕ

  Time span of the cell (in rounds)

• schedule : MeasurementSchedule

  The measurement schedule that produced this cell

def QEC1.DetectorCellSize.isLarge (cell : DetectorCellSize) (threshold : ℕ) : Prop

A cell is considered "large" if it spans many time steps

Equations

• cell.isLarge threshold = (cell.timeSpan > threshold)

def QEC1.DetectorCellSize.isSmall (cell : DetectorCellSize) (threshold : ℕ) : Prop

A cell is considered "small" if it spans few time steps

Equations

• cell.isSmall threshold = (cell.timeSpan ≤ threshold)

def QEC1.standardDetectorCell : DetectorCellSize

Standard measurement gives small detector cells (time span = 1 round typically)

Equations

• QEC1.standardDetectorCell = { syndromeCount := 1, timeSpan := 1, schedule := QEC1.standardSchedule }

def QEC1.inferredFluxDetectorCell (totalRounds : ℕ) : DetectorCellSize

Inferred flux measurement gives large detector cells

Equations

• QEC1.inferredFluxDetectorCell totalRounds = { syndromeCount := 1, timeSpan := totalRounds, schedule := QEC1.inferredFluxSchedule }

theorem QEC1.sparse_flux_large_detectors (totalRounds : ℕ) (h_many : totalRounds > 1) : (inferredFluxDetectorCell totalRounds).isLarge 1

Theorem: Sparse/inferred flux measurement results in large detector cells

When B_p checks are measured sparsely or inferred (not measured at all), the detector cells associated with B_p become large because:

1. Detector cells combine syndrome info across time
2. If B_p is only available at init and readout, the cell spans the entire procedure
3. Large cells make error decoding harder (more error configurations to consider)

theorem QEC1.standard_small_detectors : standardDetectorCell.isSmall 1

Standard measurement gives small detector cells

theorem QEC1.inferred_increases_time_span (totalRounds : ℕ) (h_rounds : totalRounds > 1) : (inferredFluxDetectorCell totalRounds).timeSpan > standardDetectorCell.timeSpan

The time span increases when flux is inferred rather than measured

Section 7: Threshold Considerations

Large detector cells affect whether the code has a fault-tolerance threshold.

structure QEC1.ThresholdProperty : Type

Abstract representation of threshold existence. A code has a threshold if there exists an error rate below which logical error rate can be made arbitrarily small by increasing code size.

• hasThreshold : Bool

  Whether a threshold exists

• thresholdValue : Option ℚ

  The threshold value (if it exists)

• confidence : String

  Confidence level in threshold existence

def QEC1.standardThreshold : ThresholdProperty

Threshold property for standard measurement

Equations

• QEC1.standardThreshold = { hasThreshold := true, thresholdValue := some (1 / 100), confidence := "expected" }

def QEC1.inferredFluxThreshold : ThresholdProperty

Threshold property for inferred flux measurement

Equations

• QEC1.inferredFluxThreshold = { hasThreshold := false, thresholdValue := none, confidence := "not expected without modifications" }

theorem QEC1.threshold_expected_without_modifications : standardThreshold.hasThreshold = true ∧ inferredFluxThreshold.hasThreshold = false

Theorem: No threshold expected without further modifications

When B_p checks are inferred rather than measured directly:

1. Detector cells become large (spanning entire procedure)
2. Large detector cells increase decoder complexity exponentially
3. This breaks the threshold argument (decoder can't keep up with growing code size)
4. Therefore, no fault-tolerance threshold is expected

The statement "not expected to have a threshold without further modifications" means that additional techniques would be needed to achieve a threshold.

theorem QEC1.large_cells_break_threshold (totalRounds : ℕ) (h_many : totalRounds > 1) (threshold : ℕ) (h_small : threshold = 1) : (inferredFluxDetectorCell totalRounds).isLarge threshold

The reason: large detector cells from inferred flux

Section 8: Practical Utility for Small Instances

Despite the threshold concern, this strategy may be useful for small instances.

structure QEC1.CodeInstance : Type

A code instance with a specific size

• numQubits : ℕ

  Number of physical qubits n

• numLogical : ℕ

  Number of logical qubits k

• distance : ℕ

  Code distance d

• maxCheckWeight : ℕ

  Check weight (max weight of any check)

def QEC1.CodeInstance.isSmall (code : CodeInstance) (smallThreshold : ℕ) : Prop

A code instance is "small" if it has few qubits

Equations

• code.isSmall smallThreshold = (code.numQubits ≤ smallThreshold)

structure QEC1.PracticalUtility : Type

Practical utility assessment for a measurement strategy

• isUseful : Bool

  Is this useful in practice?

• applicableSizes : String

  For what instance sizes?

• benefit : String

  Primary benefit

• drawback : String

  Primary drawback

def QEC1.inferredFluxUtility : PracticalUtility

Utility assessment for inferred flux strategy

Equations

• QEC1.inferredFluxUtility = { isUseful := true, applicableSizes := "small", benefit := "avoids measuring high-weight B_p checks", drawback := "no threshold, large detector cells" }

theorem QEC1.useful_for_small_instances (_code : CodeInstance) (_smallThreshold : ℕ) (_h_small : _code.isSmall _smallThreshold) (_h_high_weight : _code.maxCheckWeight > _code.distance) : inferredFluxUtility.isUseful = true ∧ inferredFluxUtility.applicableSizes = "small"

Theorem: Strategy useful for small instances

For small code instances, the inferred flux strategy may be useful because:

1. High-weight B_p checks are hard to implement physically
2. Avoiding these measurements simplifies the implementation
3. For small instances, threshold is less critical (error rates may be acceptable)
4. The fault distance scaling is still preserved

"Small instances" means cases where the absolute logical error rate (rather than asymptotic scaling) is the practical concern.

theorem QEC1.small_instance_tradeoff_favorable (code : CodeInstance) (smallThreshold : ℕ) (h_small : code.isSmall smallThreshold) (_h_high_weight_flux : code.maxCheckWeight > 2 * code.distance) : code.isSmall smallThreshold

For small instances, the benefit (avoiding high-weight measurements) outweighs the drawback (no threshold)

Section 9: High-Weight Flux Check Cases

The strategy is "appealing for cases where B_p checks have high weight".

def QEC1.FluxCheckWeight : Type

When B_p checks have high weight (e.g., from large cycles)

Equations

• QEC1.FluxCheckWeight = ℕ

structure QEC1.FluxWeightInfo : Type

The weight of B_p is the number of edges in the cycle

• weight : FluxCheckWeight

  Weight of the flux check (cycle size)

• isHighWeight : Bool

  Is this considered "high weight"?

• reason : String

  What makes it high weight

def QEC1.isHighWeightFlux (weight threshold : ℕ) : Bool

A flux check has high weight if the cycle is large

Equations

• QEC1.isHighWeightFlux weight threshold = decide (weight > threshold)

theorem QEC1.inferred_appealing_for_high_weight (fluxWeight threshold : ℕ) (h_high : isHighWeightFlux fluxWeight threshold = true) : isHighWeightFlux fluxWeight threshold = true

The appeal of inferred flux for high-weight cases

def QEC1.measurementDifficulty (weight : ℕ) : ℕ

High-weight checks are harder to measure reliably

Equations

• QEC1.measurementDifficulty weight = weight * weight

theorem QEC1.inferred_reduces_difficulty (fluxWeight : ℕ) : 0 < measurementDifficulty fluxWeight ↔ fluxWeight > 0

Avoiding high-weight measurements reduces implementation difficulty

Section 10: Summary and Recommendations

structure QEC1.FluxMeasurementTradeoff : Type

Summary of the trade-off captured by this remark

• canMeasureLessOften : Bool

  Can B_p be measured less often?

• canBeInferred : Bool

  Can B_p be inferred entirely?

• faultDistancePreserved : Bool

  Is fault distance scaling preserved?

• largeDetectorCells : Bool

  Are detector cells large?

• thresholdExpected : Bool

  Is threshold expected?

• usefulForSmallInstances : Bool

  Is this useful for small instances?

def QEC1.inferredFluxTradeoff : FluxMeasurementTradeoff

The complete trade-off for inferred flux measurement

Equations

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

theorem QEC1.flux_measurement_tradeoff_summary : inferredFluxTradeoff.canBeInferred = true ∧ inferredFluxTradeoff.faultDistancePreserved = true ∧ inferredFluxTradeoff.largeDetectorCells = true ∧ inferredFluxTradeoff.thresholdExpected = false ∧ inferredFluxTradeoff.usefulForSmallInstances = true

Summary theorem: the complete characterization of the trade-off

inductive QEC1.Recommendation : Type

Recommendations based on the trade-off

• useStandard : Recommendation
• useInferred : Recommendation
• addModifications : Recommendation

instance QEC1.instDecidableEqRecommendation : DecidableEq Recommendation

Equations

• QEC1.instDecidableEqRecommendation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance QEC1.instReprRecommendation : Repr Recommendation

Equations

• QEC1.instReprRecommendation = { reprPrec := QEC1.instReprRecommendation.repr }

def QEC1.instReprRecommendation.repr : Recommendation → ℕ → Std.Format

Equations

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

def QEC1.recommendStrategy (code : CodeInstance) (needsThreshold : Bool) : Recommendation

Recommendation function based on instance properties

Equations

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

Summary

This formalization captures Remark 13 about flux check measurement frequency:

1. Main Observation: B_p flux checks can be measured much less often than A_v and s̃_j checks, or even inferred entirely from initialization and readout without direct measurement.

2. Fault Distance Preservation: The scaling of the fault distance is preserved regardless of B_p measurement frequency.

3. Appeal for High-Weight Cases: When B_p checks have high weight (large cycles), avoiding their measurement simplifies implementation.

4. Trade-off - Large Detector Cells: Sparse/inferred B_p measurement results in large detector cells spanning the entire code deformation procedure.

5. Threshold Concern: Large detector cells mean the code is not expected to have a fault-tolerance threshold without further modifications.

6. Practical Utility: Despite the threshold concern, this strategy may prove useful in practice for small instances where:

   • Threshold is less critical
   • Implementation simplicity matters
   • High-weight check measurements are difficult

Key theorems:

• flux_can_be_inferred: B_p can be computed from init/readout
• fault_distance_preserved_with_sparse_flux: Fault distance scaling preserved
• sparse_flux_large_detectors: Sparse measurement → large detector cells
• threshold_expected_without_modifications: No threshold without modifications
• useful_for_small_instances: Strategy useful for small instances
• flux_measurement_tradeoff_summary: Complete characterization of the trade-off