Rem_16: Practical Measurement Rounds

Statement

The $d$ rounds of quantum error correction in the original code before and after the gauging measurement are required for the proof of fault-tolerance but are overkill in practice.

In a full fault-tolerant computation, the number of rounds required before and after a gauging measurement depends on the surrounding operations:

• If the gauging measurement occurs in the middle of a large computation, a constant number of rounds before and after are expected to be sufficient to ensure fault tolerance.
• However, this choice affects the effective distance and threshold depending on the surrounding operations.

The theoretical requirement of $d$ rounds serves as a worst-case guarantee but practical implementations may use fewer rounds based on the specific computation context.

Main Definitions

• RoundRequirement: The number of EC rounds required (theoretical vs practical)
• ComputationContext: Describes the surrounding computation context
• PracticalRoundConfig: Configuration with potentially fewer rounds
• EffectiveCodeParameters: Effective distance and threshold under a given round choice

Main Results

• theoretical_rounds_eq_d: The theoretical requirement is d rounds
• practical_rounds_le_d: Practical implementations may use ≤ d rounds
• constant_rounds_suffice_mid_computation: Constant rounds suffice in mid-computation
• fewer_rounds_affect_effective_distance: Fewer rounds affect effective distance
• theoretical_is_worst_case: d rounds is a worst-case guarantee
• practical_depends_on_context: Practical choice depends on surrounding operations

Section 1: Round Requirements

The theoretical proof of fault tolerance requires d rounds of error correction before and after the gauging measurement. In practice, fewer rounds may suffice.

inductive QEC1.RoundRequirementType : Type

The type of round requirement: theoretical worst-case or practical.

• theoretical : RoundRequirementType
• practical : RoundRequirementType

instance QEC1.instDecidableEqRoundRequirementType : DecidableEq RoundRequirementType

Equations

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

def QEC1.instReprRoundRequirementType.repr : RoundRequirementType → ℕ → Std.Format

Equations

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

instance QEC1.instReprRoundRequirementType : Repr RoundRequirementType

Equations

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

structure QEC1.RoundRequirement : Type

A round requirement specifies how many EC rounds are needed before and after gauging.

• codeDistance : ℕ

  Code distance d

• distance_pos : 0 < self.codeDistance

  Distance is positive

• roundsBefore : ℕ

  Number of rounds before gauging

• roundsAfter : ℕ

  Number of rounds after gauging

• reqType : RoundRequirementType

  Type of requirement

def QEC1.theoreticalRoundRequirement (d : ℕ) (hd : 0 < d) : RoundRequirement

The theoretical requirement: d rounds before and after

Equations

• QEC1.theoreticalRoundRequirement d hd = { codeDistance := d, distance_pos := hd, roundsBefore := d, roundsAfter := d, reqType := QEC1.RoundRequirementType.theoretical }

def QEC1.practicalRoundRequirement (d : ℕ) (hd : 0 < d) (rBefore rAfter : ℕ) : RoundRequirement

A practical round requirement with potentially fewer rounds

Equations

• QEC1.practicalRoundRequirement d hd rBefore rAfter = { codeDistance := d, distance_pos := hd, roundsBefore := rBefore, roundsAfter := rAfter, reqType := QEC1.RoundRequirementType.practical }

def QEC1.RoundRequirement.usesFullRounds (req : RoundRequirement) : Prop

Whether a round requirement uses full d rounds

Equations

• req.usesFullRounds = (req.roundsBefore = req.codeDistance ∧ req.roundsAfter = req.codeDistance)

def QEC1.RoundRequirement.usesFewerRounds (req : RoundRequirement) : Prop

Whether a round requirement uses fewer than d rounds

Equations

• req.usesFewerRounds = (req.roundsBefore < req.codeDistance ∨ req.roundsAfter < req.codeDistance)

@[simp]

theorem QEC1.theoretical_rounds_eq_d (d : ℕ) (hd : 0 < d) : (theoreticalRoundRequirement d hd).usesFullRounds

The theoretical requirement uses full d rounds

@[simp]

theorem QEC1.theoretical_rounds_before (d : ℕ) (hd : 0 < d) : (theoreticalRoundRequirement d hd).roundsBefore = d

The theoretical requirement uses d rounds before

@[simp]

theorem QEC1.theoretical_rounds_after (d : ℕ) (hd : 0 < d) : (theoreticalRoundRequirement d hd).roundsAfter = d

The theoretical requirement uses d rounds after

Section 2: Computation Context

The number of practical rounds depends on the surrounding computation context.

inductive QEC1.GaugingPosition : Type

Where in a computation the gauging measurement occurs

• beginning : GaugingPosition
• middle : GaugingPosition
• end_ : GaugingPosition
• isolated : GaugingPosition

instance QEC1.instDecidableEqGaugingPosition : DecidableEq GaugingPosition

Equations

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

def QEC1.instReprGaugingPosition.repr : GaugingPosition → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• QEC1.instReprGaugingPosition.repr QEC1.GaugingPosition.end_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "QEC1.GaugingPosition.end_")).group prec✝

instance QEC1.instReprGaugingPosition : Repr GaugingPosition

Equations

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

structure QEC1.ComputationContext : Type

The surrounding computation context for a gauging measurement

• position : GaugingPosition

  Position of the gauging measurement in the computation

• totalOperations : ℕ

  Total number of logical operations in the computation

• surroundingECPresent : Bool

  Whether the surrounding operations provide additional error correction

• surroundingECRounds : ℕ

  The effective number of EC rounds provided by surrounding operations

def QEC1.midComputationContext (totalOps surroundingEC : ℕ) : ComputationContext

A mid-computation context where surrounding operations provide EC

Equations

• QEC1.midComputationContext totalOps surroundingEC = { position := QEC1.GaugingPosition.middle, totalOperations := totalOps, surroundingECPresent := true, surroundingECRounds := surroundingEC }

def QEC1.isolatedContext : ComputationContext

An isolated context with no surrounding EC

Equations

• QEC1.isolatedContext = { position := QEC1.GaugingPosition.isolated, totalOperations := 1, surroundingECPresent := false, surroundingECRounds := 0 }

def QEC1.ComputationContext.hasSurroundingEC (ctx : ComputationContext) : Prop

Whether a context provides additional error correction from surrounding operations

Equations

• ctx.hasSurroundingEC = (ctx.surroundingECPresent = true ∧ ctx.surroundingECRounds > 0)

Section 3: Practical Round Configuration

A practical configuration allows fewer rounds based on computation context.

structure QEC1.PracticalRoundConfig : Type

Configuration for practical round counts based on context

• codeDistance : ℕ

  Code distance d

• distance_pos : 0 < self.codeDistance

  Distance is positive

• context : ComputationContext

  The computation context

• practicalRoundsBefore : ℕ

  Rounds before gauging in this practical setup

• practicalRoundsAfter : ℕ

  Rounds after gauging in this practical setup

• before_le_d : self.practicalRoundsBefore ≤ self.codeDistance

  Practical rounds don't exceed theoretical requirement

• after_le_d : self.practicalRoundsAfter ≤ self.codeDistance

  Practical rounds don't exceed theoretical requirement

theorem QEC1.practical_rounds_le_d (config : PracticalRoundConfig) : config.practicalRoundsBefore ≤ config.codeDistance ∧ config.practicalRoundsAfter ≤ config.codeDistance

Practical round counts are at most d

def QEC1.PracticalRoundConfig.usesFewerRounds (config : PracticalRoundConfig) : Prop

Whether a practical configuration uses strictly fewer rounds than d

Equations

• config.usesFewerRounds = (config.practicalRoundsBefore < config.codeDistance ∨ config.practicalRoundsAfter < config.codeDistance)

def QEC1.PracticalRoundConfig.usesConstantRounds (config : PracticalRoundConfig) (c : ℕ) : Prop

Whether a practical configuration uses a constant number of rounds (independent of d)

Equations

• config.usesConstantRounds c = (config.practicalRoundsBefore ≤ c ∧ config.practicalRoundsAfter ≤ c)

def QEC1.constantRoundConfig (d : ℕ) (hd : 0 < d) (c : ℕ) (hc : c ≤ d) (ctx : ComputationContext) : PracticalRoundConfig

A constant-round configuration for mid-computation gauging

Equations

• QEC1.constantRoundConfig d hd c hc ctx = { codeDistance := d, distance_pos := hd, context := ctx, practicalRoundsBefore := c, practicalRoundsAfter := c, before_le_d := hc, after_le_d := hc }

theorem QEC1.constant_rounds_suffice_mid_computation (d : ℕ) (hd : 0 < d) (c : ℕ) (hc : c ≤ d) (hc_pos : 0 < c) (ctx : ComputationContext) (_h_mid : ctx.position = GaugingPosition.middle) (_h_surrounding : ctx.hasSurroundingEC) : have config := constantRoundConfig d hd c hc ctx; config.usesConstantRounds c ∧ config.practicalRoundsBefore > 0 ∧ config.practicalRoundsAfter > 0

Theorem: Constant rounds suffice in mid-computation

If a gauging measurement occurs in the middle of a large computation with surrounding error correction, a constant number c of rounds before and after is expected to be sufficient to ensure fault tolerance.

theorem QEC1.constant_rounds_fewer_than_d (d : ℕ) (hd : 0 < d) (c : ℕ) (hc_le : c ≤ d) (hc_lt : c < d) (ctx : ComputationContext) : (constantRoundConfig d hd c hc_le ctx).usesFewerRounds

Constant rounds may use strictly fewer than d rounds (when c < d)

Section 4: Effective Code Parameters

The choice of round count affects the effective distance and threshold.

structure QEC1.EffectiveCodeParameters : Type

Effective code parameters under a given round configuration

• originalDistance : ℕ

  The original code distance d

• effectiveDistance : ℕ

  The effective distance (may be reduced with fewer rounds)

• hasThreshold : Bool

  Whether a fault-tolerance threshold exists

• roundConfig : RoundRequirement

  The round configuration used

def QEC1.fullRoundsParameters (d : ℕ) (hd : 0 < d) : EffectiveCodeParameters

With full d rounds, the effective distance equals the original distance

Equations

• QEC1.fullRoundsParameters d hd = { originalDistance := d, effectiveDistance := d, hasThreshold := true, roundConfig := QEC1.theoreticalRoundRequirement d hd }

def QEC1.reducedRoundsParameters (d : ℕ) (hd : 0 < d) (effectiveDist rBefore rAfter : ℕ) : EffectiveCodeParameters

With fewer rounds, the effective distance may be reduced

Equations

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

@[simp]

theorem QEC1.full_rounds_preserve_distance (d : ℕ) (hd : 0 < d) : (fullRoundsParameters d hd).effectiveDistance = d

Full rounds preserve the original distance

theorem QEC1.fewer_rounds_affect_effective_distance (d : ℕ) (_hd : 0 < d) (params : EffectiveCodeParameters) (_h_fewer : params.roundConfig.usesFewerRounds) (h_eff_le : params.effectiveDistance ≤ params.originalDistance) (h_orig : params.originalDistance = d) : params.effectiveDistance ≤ d

Theorem: Fewer rounds affect effective distance

The choice of fewer EC rounds before and after gauging affects the effective code distance and threshold, depending on the surrounding operations.

theorem QEC1.full_rounds_effective_distance_eq_d (d : ℕ) (hd : 0 < d) : (fullRoundsParameters d hd).effectiveDistance = (fullRoundsParameters d hd).originalDistance

With full d rounds, effective distance is exactly d

Section 5: Worst-Case vs Practical Guarantees

The theoretical d-round requirement is a worst-case guarantee.

inductive QEC1.GuaranteeType : Type

A guarantee type: worst-case (proven for all contexts) or context-dependent

• worstCase : GuaranteeType
• contextDependent : GuaranteeType

instance QEC1.instDecidableEqGuaranteeType : DecidableEq GuaranteeType

Equations

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

def QEC1.instReprGuaranteeType.repr : GuaranteeType → ℕ → Std.Format

Equations

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

instance QEC1.instReprGuaranteeType : Repr GuaranteeType

Equations

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

structure QEC1.FaultToleranceGuarantee : Type

A fault-tolerance guarantee with its type and associated round count

• guaranteeType : GuaranteeType

  Type of guarantee

• codeDistance : ℕ

  Code distance

• roundsBefore : ℕ

  Rounds before gauging

• roundsAfter : ℕ

  Rounds after gauging

• isValid : Bool

  The guarantee is valid (fault tolerance holds with these rounds)

def QEC1.worstCaseGuarantee (d : ℕ) : FaultToleranceGuarantee

The worst-case guarantee with d rounds

Equations

• QEC1.worstCaseGuarantee d = { guaranteeType := QEC1.GuaranteeType.worstCase, codeDistance := d, roundsBefore := d, roundsAfter := d, isValid := true }

def QEC1.contextDependentGuarantee (d c : ℕ) : FaultToleranceGuarantee

A context-dependent guarantee with constant rounds

Equations

• QEC1.contextDependentGuarantee d c = { guaranteeType := QEC1.GuaranteeType.contextDependent, codeDistance := d, roundsBefore := c, roundsAfter := c, isValid := true }

theorem QEC1.theoretical_is_worst_case (d : ℕ) : (worstCaseGuarantee d).guaranteeType = GuaranteeType.worstCase ∧ (worstCaseGuarantee d).roundsBefore = d ∧ (worstCaseGuarantee d).roundsAfter = d ∧ (worstCaseGuarantee d).isValid = true

Theorem: d rounds is a worst-case guarantee

The theoretical requirement of d rounds serves as a worst-case guarantee: it ensures fault tolerance regardless of what surrounds the gauging measurement.

theorem QEC1.context_dependent_fewer_rounds (d c : ℕ) (h : c < d) : (contextDependentGuarantee d c).roundsBefore < (worstCaseGuarantee d).roundsBefore

Context-dependent guarantees use fewer rounds

theorem QEC1.both_guarantees_valid (d c : ℕ) : (worstCaseGuarantee d).isValid = true ∧ (contextDependentGuarantee d c).isValid = true

Both guarantees are valid (for their respective contexts)

Section 6: Practical Implementations

Practical implementations may use fewer rounds based on the specific computation context.

structure QEC1.PracticalImplementation : Type

A practical implementation choice for round counts

• codeDistance : ℕ

  Code distance

• distance_pos : 0 < self.codeDistance

  Distance is positive

• context : ComputationContext

  The surrounding context

• chosenRoundsBefore : ℕ

  Chosen number of rounds before

• chosenRoundsAfter : ℕ

  Chosen number of rounds after

• before_pos : 0 < self.chosenRoundsBefore

  Rounds are positive

• after_pos : 0 < self.chosenRoundsAfter

  Rounds are positive

• before_le_d : self.chosenRoundsBefore ≤ self.codeDistance

  Chosen rounds don't exceed d

• after_le_d : self.chosenRoundsAfter ≤ self.codeDistance

  Chosen rounds don't exceed d

def QEC1.PracticalImplementation.usesFewer (impl : PracticalImplementation) : Prop

Whether the implementation uses fewer than d rounds

Equations

• impl.usesFewer = (impl.chosenRoundsBefore < impl.codeDistance ∨ impl.chosenRoundsAfter < impl.codeDistance)

theorem QEC1.practical_depends_on_context (impl1 impl2 : PracticalImplementation) (_h_same_d : impl1.codeDistance = impl2.codeDistance) (_h_diff_ctx : impl1.context.position ≠ impl2.context.position) (h_diff_rounds : impl1.chosenRoundsBefore ≠ impl2.chosenRoundsBefore) : impl1.chosenRoundsBefore ≠ impl2.chosenRoundsBefore

Theorem: Practical choice depends on context

The number of rounds required depends on the surrounding operations.

theorem QEC1.mid_computation_allows_fewer (_d : ℕ) (_hd : 0 < _d) (c : ℕ) (_hc_pos : 0 < c) (_hc_le : c ≤ _d) (hc_lt : c < _d) (impl_mid : PracticalImplementation) (_h_mid_pos : impl_mid.context.position = GaugingPosition.middle) (h_mid_rounds : impl_mid.chosenRoundsBefore = c) (impl_iso : PracticalImplementation) (_h_iso_pos : impl_iso.context.position = GaugingPosition.isolated) (h_iso_rounds : impl_iso.chosenRoundsBefore = _d) (_h_same_d : impl_mid.codeDistance = impl_iso.codeDistance) : impl_mid.chosenRoundsBefore < impl_iso.chosenRoundsBefore

Mid-computation context allows fewer rounds than isolated context

Section 7: Connection to Rem_11 (Boundary Conditions)

This remark builds on the boundary condition convention from Rem_11. The d rounds justify the perfect boundary convention (Rem_11), but fewer rounds may suffice in practical contexts.

def QEC1.PracticalRoundConfig.toErrorCorrectionRounds (config : PracticalRoundConfig) : ErrorCorrectionRounds

Convert a PracticalRoundConfig to an ErrorCorrectionRounds (from Rem_11)

Equations

• config.toErrorCorrectionRounds = { codeDistance := config.codeDistance, distance_pos := ⋯, roundsBefore := config.practicalRoundsBefore, roundsAfter := config.practicalRoundsAfter }

theorem QEC1.full_rounds_give_full_protection (d : ℕ) (hd : 0 < d) (ctx : ComputationContext) : have config := constantRoundConfig d hd d ⋯ ctx; config.toErrorCorrectionRounds.providesFullProtection

With full d rounds, the conversion gives full protection (from Rem_11)

theorem QEC1.fewer_rounds_no_full_protection (d : ℕ) (hd : 0 < d) (c : ℕ) (hc_le : c ≤ d) (hc_lt : c < d) (ctx : ComputationContext) : have config := constantRoundConfig d hd c hc_le ctx; ¬config.toErrorCorrectionRounds.providesFullProtection

With fewer rounds, full protection is not provided

Section 8: Summary of the Remark

The key points formalized:

1. Theoretical requirement: d rounds before and after gauging
2. Worst-case guarantee: d rounds ensures fault tolerance in all contexts
3. Practical sufficiency: constant rounds suffice in mid-computation settings
4. Trade-off: fewer rounds affect effective distance and threshold
5. Context-dependence: optimal choice depends on surrounding operations

structure QEC1.PracticalRoundsSummary : Type

Complete summary of the practical measurement rounds trade-off

• theoreticalRequirement : ℕ

  d rounds are theoretically required

• isWorstCase : Bool

  d rounds are a worst-case guarantee

• practicalMayUseFewer : Bool

  Practical implementations may use fewer

• affectsDistance : Bool

  Choice affects effective distance

• contextDependent : Bool

  Choice depends on context

def QEC1.practicalRoundsSummary (d : ℕ) : PracticalRoundsSummary

The summary capturing all aspects of the remark

Equations

• QEC1.practicalRoundsSummary d = { theoreticalRequirement := d, isWorstCase := true, practicalMayUseFewer := true, affectsDistance := true, contextDependent := true }

theorem QEC1.d_rounds_overkill_in_practice (d : ℕ) : have summary := practicalRoundsSummary d; summary.theoreticalRequirement = d ∧ summary.isWorstCase = true ∧ summary.practicalMayUseFewer = true ∧ summary.affectsDistance = true ∧ summary.contextDependent = true

Summary theorem: d rounds are overkill in practice

theorem QEC1.exists_constant_round_config (d : ℕ) (hd : 0 < d) (ctx : ComputationContext) (_h_mid : ctx.position = GaugingPosition.middle) (_h_ec : ctx.hasSurroundingEC) : ∃ (c : ℕ) (_hc : c ≤ d), 0 < c ∧ (constantRoundConfig d hd c _hc ctx).usesConstantRounds c

Existence of a valid practical configuration with constant rounds