Rem_11: Initial and Final Boundary Conditions

Statement

Following standard practice, we use the convention that the initial and final round of stabilizer measurements are perfect. This is to facilitate clean statements of our results and should not be taken literally. The justification for why this convention does not fundamentally change results is due to the $d$ rounds of error correction in the original code before and after the gauging measurement. This ensures that any error process involving both the gauging measurement and the initial or final boundary condition must have distance greater than $d$. In practice, the gauging measurement is intended to be one component of a larger fault-tolerant quantum computation which determines the appropriate realistic boundary conditions to use.

Main Definitions

• BoundaryConditionConvention: The convention that initial/final measurements are perfect
• PerfectBoundaryAssumption: Structure for perfect boundary conditions
• ErrorCorrectionRounds: Configuration of d error correction rounds before/after gauging
• ErrorProcess: An error process with weight and boundary involvement flags

Main Results

• boundary_spanning_distance_gt_d: Any boundary-spanning error process has weight > d
• low_weight_cannot_span_boundary: Low-weight errors cannot span to boundaries
• boundary_convention_justification: Errors spanning to boundaries have distance > d
• boundary_irrelevance_for_fault_tolerance: In context of fault tolerance, boundary choice doesn't matter

Practical Note

This convention is for theoretical clarity. Real implementations determine boundary conditions based on the surrounding fault-tolerant computation context.

Section 1: Boundary Condition Types

We formalize the notion of boundary conditions for the gauging measurement procedure. The "boundary" refers to the initial and final rounds of stabilizer measurements.

inductive QEC1.BoundaryType : Type

A boundary type: either the initial or final boundary of the gauging procedure

• initial : BoundaryType
• final : BoundaryType

instance QEC1.instDecidableEqBoundaryType : DecidableEq BoundaryType

Equations

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

def QEC1.instReprBoundaryType.repr : BoundaryType → ℕ → Std.Format

Equations

• QEC1.instReprBoundaryType.repr QEC1.BoundaryType.initial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "QEC1.BoundaryType.initial")).group prec✝
• QEC1.instReprBoundaryType.repr QEC1.BoundaryType.final prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "QEC1.BoundaryType.final")).group prec✝

instance QEC1.instReprBoundaryType : Repr BoundaryType

Equations

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

def QEC1.BoundaryType.toString : BoundaryType → String

String representation for documentation

Equations

• QEC1.BoundaryType.initial.toString = "initial"
• QEC1.BoundaryType.final.toString = "final"

inductive QEC1.BoundaryConditionQuality : Type

A boundary condition describes the quality of measurements at the boundary. We consider two cases: perfect (idealized) or realistic (subject to errors).

• perfect : BoundaryConditionQuality
• realistic : BoundaryConditionQuality

instance QEC1.instDecidableEqBoundaryConditionQuality : DecidableEq BoundaryConditionQuality

Equations

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

instance QEC1.instReprBoundaryConditionQuality : Repr BoundaryConditionQuality

Equations

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

def QEC1.instReprBoundaryConditionQuality.repr : BoundaryConditionQuality → ℕ → Std.Format

Equations

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

Section 2: Perfect Boundary Assumption

The convention states that initial and final rounds of stabilizer measurements are perfect.

structure QEC1.PerfectBoundaryAssumption : Type

The Perfect Boundary Assumption: the boundary measurements are error-free. This is an idealization used for theoretical analysis.

• initialQuality : BoundaryConditionQuality

  Quality of initial boundary measurements

• finalQuality : BoundaryConditionQuality

  Quality of final boundary measurements

def QEC1.standardBoundaryConvention : PerfectBoundaryAssumption

The standard convention: both boundaries are perfect

Equations

• QEC1.standardBoundaryConvention = { }

def QEC1.PerfectBoundaryAssumption.isPerfect (pba : PerfectBoundaryAssumption) (bt : BoundaryType) : Bool

Check if a boundary is assumed perfect

Equations

• pba.isPerfect QEC1.BoundaryType.initial = decide (pba.initialQuality = QEC1.BoundaryConditionQuality.perfect)
• pba.isPerfect QEC1.BoundaryType.final = decide (pba.finalQuality = QEC1.BoundaryConditionQuality.perfect)

Section 3: Error Correction Rounds

The justification for the perfect boundary convention is that d rounds of error correction occur before and after the gauging measurement.

structure QEC1.ErrorCorrectionRounds : Type

Configuration of error correction rounds around the gauging measurement. The code distance d determines the number of rounds before and after.

• codeDistance : ℕ

  Code distance d

• distance_pos : 0 < self.codeDistance

  Distance is positive

• roundsBefore : ℕ

  Number of EC rounds before gauging (should be d for full protection)

• roundsAfter : ℕ

  Number of EC rounds after gauging (should be d for full protection)

def QEC1.standardErrorCorrectionRounds (d : ℕ) (hd : 0 < d) : ErrorCorrectionRounds

The standard configuration with d rounds before and after

Equations

• QEC1.standardErrorCorrectionRounds d hd = { codeDistance := d, distance_pos := hd, roundsBefore := d, roundsAfter := d }

def QEC1.ErrorCorrectionRounds.providesFullProtection (ec : ErrorCorrectionRounds) : Prop

Check if the EC configuration provides full distance protection

Equations

• ec.providesFullProtection = (ec.roundsBefore = ec.codeDistance ∧ ec.roundsAfter = ec.codeDistance)

theorem QEC1.standardErrorCorrectionRounds_providesFullProtection (d : ℕ) (hd : 0 < d) : (standardErrorCorrectionRounds d hd).providesFullProtection

The standard configuration provides full protection

Section 4: Boundary-Spanning Error Processes

An error process that involves both the gauging measurement and a boundary condition must "span" the error correction rounds.

structure QEC1.ErrorProcess : Type

An error process in the fault-tolerant procedure. This abstractly represents a collection of faults that could occur.

• weight : ℕ

  Total weight of the error process (number of faults)

• involvesGauging : Bool

  Does this process involve the gauging measurement?

• involvesInitialBoundary : Bool

  Does this process involve the initial boundary?

• involvesFinalBoundary : Bool

  Does this process involve the final boundary?

def QEC1.ErrorProcess.spansToBoundary (ep : ErrorProcess) : Bool

An error process spans from the gauging measurement to a boundary if it involves both the gauging and at least one boundary.

Equations

• ep.spansToBoundary = (ep.involvesGauging && (ep.involvesInitialBoundary || ep.involvesFinalBoundary))

def QEC1.ErrorProcess.spansToInitialBoundary (ep : ErrorProcess) : Bool

An error process spans to the initial boundary

Equations

• ep.spansToInitialBoundary = (ep.involvesGauging && ep.involvesInitialBoundary)

def QEC1.ErrorProcess.spansToFinalBoundary (ep : ErrorProcess) : Bool

An error process spans to the final boundary

Equations

• ep.spansToFinalBoundary = (ep.involvesGauging && ep.involvesFinalBoundary)

Section 5: The Main Justification

The key insight: any error process that spans from the gauging measurement to a boundary must have weight greater than d, because it must propagate through d rounds of error correction.

theorem QEC1.boundary_spanning_distance_gt_d (ec : ErrorCorrectionRounds) (h_full : ec.providesFullProtection) (ep : ErrorProcess) (h_spans : ep.spansToBoundary = true) (_h_propagates : ep.weight > 0) (h_prop_init : ep.involvesGauging = true ∧ ep.involvesInitialBoundary = true → ep.weight ≥ ec.roundsBefore + 1) (h_prop_final : ep.involvesGauging = true ∧ ep.involvesFinalBoundary = true → ep.weight ≥ ec.roundsAfter + 1) : ep.weight > ec.codeDistance

Theorem: Boundary-spanning errors have distance > d

Any error process that involves both:

1. The gauging measurement, and
2. Either the initial or final boundary condition

must have weight greater than d (the code distance), because it must propagate through the d rounds of error correction that separate them.

This is the fundamental justification for why the perfect boundary convention does not change results: such high-weight errors are already correctable/detectable.

theorem QEC1.low_weight_cannot_span_boundary (ec : ErrorCorrectionRounds) (h_full : ec.providesFullProtection) (ep : ErrorProcess) (h_low_weight : ep.weight ≤ ec.codeDistance) (h_prop_init : ep.involvesGauging = true ∧ ep.involvesInitialBoundary = true → ep.weight ≥ ec.roundsBefore + 1) (h_prop_final : ep.involvesGauging = true ∧ ep.involvesFinalBoundary = true → ep.weight ≥ ec.roundsAfter + 1) : ep.spansToBoundary = false

Corollary: Low-weight errors cannot span to boundaries

If an error process has weight ≤ d, it cannot involve both the gauging measurement and a boundary condition (under the propagation model).

Section 6: The Convention's Purpose

The perfect boundary convention simplifies theorem statements without loss of generality for fault tolerance results.

structure QEC1.BoundaryConditionConvention : Type

The Boundary Condition Convention: a formal statement of the convention.

This structure captures the convention that:

1. Initial and final measurements are assumed perfect (for clean statements)
2. This is justified by d rounds of EC before and after gauging
3. The convention is for theoretical simplification, not literal interpretation

• assumption : PerfectBoundaryAssumption

  The perfect boundary assumption

• ecConfig : ErrorCorrectionRounds

  The error correction configuration

• fullProtection : self.ecConfig.providesFullProtection

  Full protection is provided

• isSimplification : Bool

  Documentation: this is a simplification

def QEC1.standardBoundaryConditionConvention (d : ℕ) (hd : 0 < d) : BoundaryConditionConvention

The standard boundary condition convention

Equations

• QEC1.standardBoundaryConditionConvention d hd = { assumption := QEC1.standardBoundaryConvention, ecConfig := QEC1.standardErrorCorrectionRounds d hd, fullProtection := ⋯ }

theorem QEC1.boundary_convention_justification (conv : BoundaryConditionConvention) (ep : ErrorProcess) : ep.spansToBoundary = true → (ep.involvesGauging = true ∧ ep.involvesInitialBoundary = true → ep.weight ≥ conv.ecConfig.roundsBefore + 1) → (ep.involvesGauging = true ∧ ep.involvesFinalBoundary = true → ep.weight ≥ conv.ecConfig.roundsAfter + 1) → ep.weight > conv.ecConfig.codeDistance

The justification for the convention: Boundary-spanning errors have weight > d, so they're already accounted for in the fault tolerance analysis.

Section 7: Practical Considerations

In practice, the gauging measurement is part of a larger fault-tolerant computation, which determines the realistic boundary conditions.

structure QEC1.RealisticBoundaryContext : Type

Realistic boundary conditions are determined by the surrounding computation context

• computationContext : String

  Description of the surrounding computation

• initialCondition : BoundaryConditionQuality

  The actual initial boundary condition

• finalCondition : BoundaryConditionQuality

  The actual final boundary condition

def QEC1.BoundaryConditionConvention.toRealistic (_conv : BoundaryConditionConvention) (ctx : RealisticBoundaryContext) : RealisticBoundaryContext

The theoretical convention can be replaced by realistic conditions without fundamentally changing fault tolerance results.

Equations

• _conv.toRealistic ctx = ctx

theorem QEC1.boundary_irrelevance_for_fault_tolerance (conv : BoundaryConditionConvention) (d : ℕ) (hd : conv.ecConfig.codeDistance = d) (ep : ErrorProcess) : ep.weight ≤ d → (ep.involvesGauging = true ∧ ep.involvesInitialBoundary = true → ep.weight ≥ conv.ecConfig.roundsBefore + 1) → (ep.involvesGauging = true ∧ ep.involvesFinalBoundary = true → ep.weight ≥ conv.ecConfig.roundsAfter + 1) → ep.spansToBoundary = false

Theorem: Boundary irrelevance for fault tolerance

In the context of fault tolerance analysis, the choice of boundary conditions (perfect vs realistic) doesn't fundamentally change results because:

1. Perfect boundaries simplify statements
2. Realistic boundary errors must propagate through d EC rounds
3. Such propagation requires weight > d errors

This captures the statement "should not be taken literally".

Section 8: Time Structure of Boundaries

Relating to the time step convention (Def_12), we establish when the boundaries occur.

def QEC1.initialBoundaryTime (config : GaugingTimeConfig) : IntegerTimeStep

The initial boundary occurs at time t₀ (start of procedure)

Equations

• QEC1.initialBoundaryTime config = config.t_start

def QEC1.finalBoundaryTime (config : GaugingTimeConfig) : IntegerTimeStep

The final boundary occurs at time after t_final

Equations

• QEC1.finalBoundaryTime config = config.t_final

def QEC1.gaugingTimeRange (config : GaugingTimeConfig) : Set IntegerTimeStep

The gauging measurement occurs at times t_initial through t_final

Equations

• QEC1.gaugingTimeRange config = {t : IntegerTimeStep | config.t_initial ≤ t ∧ t ≤ config.t_final}

def QEC1.initialBoundarySeparation (config : GaugingTimeConfig) : ℕ

Time separation between initial boundary and gauging start

Equations

• QEC1.initialBoundarySeparation config = Int.toNat (config.t_initial - config.t_start)

def QEC1.finalBoundarySeparation (_config : GaugingTimeConfig) : ℕ

Time separation between gauging end and final boundary

Equations

• QEC1.finalBoundarySeparation _config = 0

theorem QEC1.initialBoundary_separated_by_d (config : GaugingTimeConfig) (ec : ErrorCorrectionRounds) (h_before : config.t_initial - config.t_start = ↑ec.roundsBefore) : initialBoundarySeparation config = ec.roundsBefore

With d rounds before gauging, initial boundary is separated by d time steps

Summary

This formalization captures Remark 11's convention about perfect boundary conditions:

1. Convention: Initial and final rounds of stabilizer measurements are assumed perfect.

2. Purpose: This facilitates clean statements of fault tolerance results.

3. Justification: d rounds of error correction before and after the gauging measurement ensure that any error process spanning from gauging to a boundary must have weight > d.

4. Practical note: This is a theoretical simplification. Real implementations use boundary conditions determined by the surrounding fault-tolerant computation.

Key theorems proven:

• boundary_spanning_distance_gt_d: Boundary-spanning errors have weight > d
• low_weight_cannot_span_boundary: Low-weight errors cannot span to boundaries
• boundary_convention_justification: The formal justification for the convention
• boundary_irrelevance_for_fault_tolerance: Boundary choice doesn't affect fault tolerance