Def_12: Time Step Convention

Statement

We use a half-integer time step convention for the fault-tolerant gauging measurement procedure:

Integer time steps $t = 0, 1, 2, \ldots$: Associated with qubit states and Pauli space-errors. A Pauli error 'at time $t$' affects the state between measurement rounds at times $t - \frac{1}{2}$ and $t + \frac{1}{2}$.

Half-integer time steps $t + \frac{1}{2}$: Associated with measurements and measurement errors. A measurement 'at time $t + \frac{1}{2}$' occurs between qubit states at times $t$ and $t + 1$.

Key time points:

• $t_0$: Start of the procedure
• $t_i$: Time of the initial gauging code deformation (edge qubit initialization and first $A_v$ measurements at $t_i - \frac{1}{2}$ and $t_i + \frac{1}{2}$)
• $t_o$: Time of the final ungauging code deformation (last $A_v$ measurements and edge qubit readout at $t_o - \frac{1}{2}$ and $t_o + \frac{1}{2}$)

Main Definitions

• HalfIntegerTime : Represents both integer and half-integer time steps
• IntegerTimeStep : Integer times associated with qubit states
• HalfIntegerTimeStep : Half-integer times associated with measurements
• TimeStepConvention : The convention relating integer/half-integer times

Key Properties

• integerTime_isQubitStateTime : Integer times are for qubit states
• halfIntegerTime_isMeasurementTime : Half-integer times are for measurements
• measurement_between_states : Measurement at t+1/2 is between states at t and t+1
• error_between_measurements : Error at t is between measurements at t-1/2 and t+1/2

Half-Integer Time Representation

We represent time as either an integer (for qubit states) or a half-integer (for measurements). A half-integer n + 1/2 is represented by storing the integer n.

We use ℤ to allow negative times for generality (though in practice we mostly use t ≥ 0).

inductive HalfIntegerTime : Type

A half-integer time representation.

• integer n represents the integer time step n
• halfInteger n represents the half-integer time step n + 1/2

• integer : ℤ → HalfIntegerTime
• halfInteger : ℤ → HalfIntegerTime

instance instDecidableEqHalfIntegerTime : DecidableEq HalfIntegerTime

Equations

• instDecidableEqHalfIntegerTime = instDecidableEqHalfIntegerTime.decEq

def instDecidableEqHalfIntegerTime.decEq (x✝ x✝¹ : HalfIntegerTime) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqHalfIntegerTime.decEq (HalfIntegerTime.integer a) (HalfIntegerTime.integer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqHalfIntegerTime.decEq (HalfIntegerTime.integer a) (HalfIntegerTime.halfInteger a_1) = isFalse ⋯
• instDecidableEqHalfIntegerTime.decEq (HalfIntegerTime.halfInteger a) (HalfIntegerTime.integer a_1) = isFalse ⋯
• instDecidableEqHalfIntegerTime.decEq (HalfIntegerTime.halfInteger a) (HalfIntegerTime.halfInteger b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def instReprHalfIntegerTime.repr : HalfIntegerTime → ℕ → Std.Format

Equations

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

instance instReprHalfIntegerTime : Repr HalfIntegerTime

Equations

• instReprHalfIntegerTime = { reprPrec := instReprHalfIntegerTime.repr }

def HalfIntegerTime.toRat : HalfIntegerTime → ℚ

Convert to a rational number for comparison

Equations

• (HalfIntegerTime.integer a).toRat = ↑a
• (HalfIntegerTime.halfInteger a).toRat = ↑a + 1 / 2

def HalfIntegerTime.isInteger : HalfIntegerTime → Bool

Check if this is an integer time

Equations

• (HalfIntegerTime.integer a).isInteger = true
• (HalfIntegerTime.halfInteger a).isInteger = false

def HalfIntegerTime.isHalfInteger : HalfIntegerTime → Bool

Check if this is a half-integer time

Equations

• (HalfIntegerTime.integer a).isHalfInteger = false
• (HalfIntegerTime.halfInteger a).isHalfInteger = true

@[simp]

theorem HalfIntegerTime.isInteger_integer (n : ℤ) : (integer n).isInteger = true

@[simp]

theorem HalfIntegerTime.isInteger_halfInteger (n : ℤ) : (halfInteger n).isInteger = false

@[simp]

theorem HalfIntegerTime.isHalfInteger_integer (n : ℤ) : (integer n).isHalfInteger = false

@[simp]

theorem HalfIntegerTime.isHalfInteger_halfInteger (n : ℤ) : (halfInteger n).isHalfInteger = true

def HalfIntegerTime.floor : HalfIntegerTime → ℤ

Get the integer part (floor)

Equations

• (HalfIntegerTime.integer a).floor = a
• (HalfIntegerTime.halfInteger a).floor = a

def HalfIntegerTime.ceil : HalfIntegerTime → ℤ

Get the integer part rounded up (ceiling)

Equations

• (HalfIntegerTime.integer a).ceil = a
• (HalfIntegerTime.halfInteger a).ceil = a + 1

@[simp]

theorem HalfIntegerTime.floor_integer (n : ℤ) : (integer n).floor = n

@[simp]

theorem HalfIntegerTime.floor_halfInteger (n : ℤ) : (halfInteger n).floor = n

@[simp]

theorem HalfIntegerTime.ceil_integer (n : ℤ) : (integer n).ceil = n

@[simp]

theorem HalfIntegerTime.ceil_halfInteger (n : ℤ) : (halfInteger n).ceil = n + 1

instance HalfIntegerTime.instLE : LE HalfIntegerTime

Linear ordering on half-integer times

Equations

• HalfIntegerTime.instLE = { le := fun (t₁ t₂ : HalfIntegerTime) => t₁.toRat ≤ t₂.toRat }

instance HalfIntegerTime.instLT : LT HalfIntegerTime

Equations

• HalfIntegerTime.instLT = { lt := fun (t₁ t₂ : HalfIntegerTime) => t₁.toRat < t₂.toRat }

instance HalfIntegerTime.instDecidableRelLe : DecidableRel fun (x1 x2 : HalfIntegerTime) => x1 ≤ x2

Equations

• t₁.instDecidableRelLe t₂ = inferInstanceAs (Decidable (t₁.toRat ≤ t₂.toRat))

instance HalfIntegerTime.instDecidableRelLt : DecidableRel fun (x1 x2 : HalfIntegerTime) => x1 < x2

Equations

• t₁.instDecidableRelLt t₂ = inferInstanceAs (Decidable (t₁.toRat < t₂.toRat))

theorem HalfIntegerTime.integer_lt_halfInteger_same (n : ℤ) : integer n < halfInteger n

Integer time n comes before half-integer time n + 1/2

theorem HalfIntegerTime.halfInteger_lt_integer_succ (n : ℤ) : halfInteger n < integer (n + 1)

Half-integer time n + 1/2 comes before integer time n + 1

def HalfIntegerTime.succ : HalfIntegerTime → HalfIntegerTime

Successor: move to the next time step

Equations

• (HalfIntegerTime.integer a).succ = HalfIntegerTime.halfInteger a
• (HalfIntegerTime.halfInteger a).succ = HalfIntegerTime.integer (a + 1)

def HalfIntegerTime.pred : HalfIntegerTime → HalfIntegerTime

Predecessor: move to the previous time step

Equations

• (HalfIntegerTime.integer a).pred = HalfIntegerTime.halfInteger (a - 1)
• (HalfIntegerTime.halfInteger a).pred = HalfIntegerTime.integer a

@[simp]

theorem HalfIntegerTime.succ_integer (n : ℤ) : (integer n).succ = halfInteger n

@[simp]

theorem HalfIntegerTime.succ_halfInteger (n : ℤ) : (halfInteger n).succ = integer (n + 1)

@[simp]

theorem HalfIntegerTime.pred_integer (n : ℤ) : (integer n).pred = halfInteger (n - 1)

@[simp]

theorem HalfIntegerTime.pred_halfInteger (n : ℤ) : (halfInteger n).pred = integer n

@[simp]

theorem HalfIntegerTime.pred_succ (t : HalfIntegerTime) : t.succ.pred = t

succ and pred are inverses

@[simp]

theorem HalfIntegerTime.succ_pred (t : HalfIntegerTime) : t.pred.succ = t

theorem HalfIntegerTime.lt_succ (t : HalfIntegerTime) : t < t.succ

t < t.succ

theorem HalfIntegerTime.pred_lt (t : HalfIntegerTime) : t.pred < t

t.pred < t

Integer Time Steps (Qubit States)

Integer time steps t = 0, 1, 2, ... are associated with qubit states and Pauli space-errors. A Pauli error 'at time t' affects the state between measurement rounds at times t - 1/2 and t + 1/2.

@[reducible, inline]

abbrev IntegerTimeStep : Type

An integer time step, associated with qubit states and space-errors

Equations

• IntegerTimeStep = ℤ

def TimeStep.toIntegerTime (t : TimeStep) : IntegerTimeStep

Convert a natural number time step to an integer time step

Equations

• t.toIntegerTime = ↑t

def IntegerTimeStep.toHalfIntegerTime (t : IntegerTimeStep) : HalfIntegerTime

Convert an integer time step to a HalfIntegerTime

Equations

• t.toHalfIntegerTime = HalfIntegerTime.integer t

Half-Integer Time Steps (Measurements)

Half-integer time steps t + 1/2 are associated with measurements and measurement errors. A measurement 'at time t + 1/2' occurs between qubit states at times t and t + 1.

@[reducible, inline]

abbrev MeasurementTimeStep : Type

A half-integer time step (measurements), represented by storing the integer part. Value n represents the time n + 1/2

Equations

• MeasurementTimeStep = ℤ

def MeasurementTimeStep.toHalfIntegerTime (t : MeasurementTimeStep) : HalfIntegerTime

Convert a measurement time step to a HalfIntegerTime

Equations

• t.toHalfIntegerTime = HalfIntegerTime.halfInteger t

def IntegerTimeStep.nextMeasurementTime (t : IntegerTimeStep) : MeasurementTimeStep

The measurement time immediately after integer time t is t + 1/2

Equations

• t.nextMeasurementTime = t

def IntegerTimeStep.prevMeasurementTime (t : IntegerTimeStep) : MeasurementTimeStep

The measurement time immediately before integer time t is t - 1/2

Equations

• t.prevMeasurementTime = t - 1

def MeasurementTimeStep.nextIntegerTime (t : MeasurementTimeStep) : IntegerTimeStep

The integer time immediately after measurement time t + 1/2 is t + 1

Equations

• t.nextIntegerTime = t + 1

def MeasurementTimeStep.prevIntegerTime (t : MeasurementTimeStep) : IntegerTimeStep

The integer time immediately before measurement time t + 1/2 is t

Equations

• t.prevIntegerTime = t

Key Properties: Time Ordering

theorem measurement_between_states (t : MeasurementTimeStep) : HalfIntegerTime.integer t < HalfIntegerTime.halfInteger t ∧ HalfIntegerTime.halfInteger t < HalfIntegerTime.integer (t + 1)

A measurement at time t + 1/2 occurs between qubit states at times t and t + 1

theorem error_between_measurements (t : IntegerTimeStep) : HalfIntegerTime.halfInteger (t - 1) < HalfIntegerTime.integer t ∧ HalfIntegerTime.integer t < HalfIntegerTime.halfInteger t

A Pauli error at integer time t affects state between measurements at t - 1/2 and t + 1/2

Key Time Points in Gauging Procedure

The gauging measurement procedure has three key time points:

• t₀: Start of the procedure
• tᵢ: Time of the initial gauging code deformation
• tₒ: Time of the final ungauging code deformation

structure GaugingTimeConfig : Type

Configuration of key time points in the gauging procedure

• t_start : IntegerTimeStep

  t₀: Start of the procedure

• t_initial : IntegerTimeStep

  tᵢ: Time of the initial gauging code deformation

• t_final : IntegerTimeStep

  tₒ: Time of the final ungauging code deformation

• start_le_initial : self.t_start ≤ self.t_initial

  The procedure proceeds in order: t₀ ≤ tᵢ ≤ tₒ

• initial_le_final : self.t_initial ≤ self.t_final

def GaugingTimeConfig.duration (config : GaugingTimeConfig) : ℕ

Duration of the gauging measurement procedure

Equations

• config.duration = Int.toNat (config.t_final - config.t_start)

def GaugingTimeConfig.gaugedPhaseDuration (config : GaugingTimeConfig) : ℕ

Duration of the gauged phase (from tᵢ to tₒ)

Equations

• config.gaugedPhaseDuration = Int.toNat (config.t_final - config.t_initial)

def GaugingTimeConfig.firstGaugeMeasurement (config : GaugingTimeConfig) : MeasurementTimeStep

First A_v measurement time: tᵢ - 1/2

Equations

• config.firstGaugeMeasurement = config.t_initial - 1

def GaugingTimeConfig.secondGaugeMeasurement (config : GaugingTimeConfig) : MeasurementTimeStep

Second A_v measurement time: tᵢ + 1/2

Equations

• config.secondGaugeMeasurement = config.t_initial

def GaugingTimeConfig.lastGaugeMeasurementBefore (config : GaugingTimeConfig) : MeasurementTimeStep

Last A_v measurement time: tₒ - 1/2

Equations

• config.lastGaugeMeasurementBefore = config.t_final - 1

def GaugingTimeConfig.finalGaugeMeasurement (config : GaugingTimeConfig) : MeasurementTimeStep

Final A_v measurement time: tₒ + 1/2

Equations

• config.finalGaugeMeasurement = config.t_final

theorem GaugingTimeConfig.firstGaugeMeasurement_before_initial (config : GaugingTimeConfig) : HalfIntegerTime.halfInteger config.firstGaugeMeasurement < HalfIntegerTime.integer config.t_initial

The first A_v measurement at tᵢ - 1/2 comes before the integer time tᵢ

theorem GaugingTimeConfig.secondGaugeMeasurement_after_initial (config : GaugingTimeConfig) : HalfIntegerTime.integer config.t_initial < HalfIntegerTime.halfInteger config.secondGaugeMeasurement

The second A_v measurement at tᵢ + 1/2 comes after the integer time tᵢ

Time Step Convention Summary

The convention establishes a clear relationship between:

1. Integer times (qubit states, Pauli errors)
2. Half-integer times (measurements, measurement errors)

This interleaving ensures that:

• Each measurement occurs between two consecutive state times
• Each Pauli error affects the state between two consecutive measurements

structure TimeStepConvention : Type

The time step convention type

• integerTimesForStates : Bool

  Integer times are for qubit states

• halfIntegerTimesForMeasurements : Bool

  Half-integer times are for measurements

def standardTimeConvention : TimeStepConvention

The standard half-integer convention

Equations

• standardTimeConvention = { }

Association of Fault Types with Time Types

def spaceFaultTime (t : TimeStep) : HalfIntegerTime

Space faults (Pauli errors) occur at integer times

Equations

• spaceFaultTime t = HalfIntegerTime.integer ↑t

def timeFaultTime (t : TimeStep) : HalfIntegerTime

Time faults (measurement errors) occur at half-integer times

Equations

• timeFaultTime t = HalfIntegerTime.halfInteger ↑t

theorem spaceFault_between_measurements (t : TimeStep) (_ht : 0 < t) : HalfIntegerTime.halfInteger (↑t - 1) < spaceFaultTime t ∧ spaceFaultTime t < HalfIntegerTime.halfInteger ↑t

A space fault at time t is between measurements at t - 1/2 and t + 1/2

theorem timeFault_between_states (t : TimeStep) : spaceFaultTime t < timeFaultTime t ∧ timeFaultTime t < spaceFaultTime (t + 1)

A measurement fault at time t + 1/2 is between states at t and t + 1

Ranges of Time Steps

Useful predicates and functions for working with ranges of integer and half-integer times.

def integerTimesInRange (t₁ t₂ : IntegerTimeStep) : Set IntegerTimeStep

The integer time steps in a range [t₁, t₂]

Equations

• integerTimesInRange t₁ t₂ = {t : IntegerTimeStep | t₁ ≤ t ∧ t ≤ t₂}

def measurementTimesInRange (t₁ t₂ : IntegerTimeStep) : Set MeasurementTimeStep

The measurement time steps in a range [t₁ + 1/2, t₂ - 1/2]

Equations

• measurementTimesInRange t₁ t₂ = {t : MeasurementTimeStep | t₁ ≤ t ∧ t < t₂}

def allTimesInRange (t₁ t₂ : IntegerTimeStep) : Set HalfIntegerTime

All half-integer times between integer times t₁ and t₂

Equations

• allTimesInRange t₁ t₂ = {t : HalfIntegerTime | HalfIntegerTime.integer t₁ ≤ t ∧ t ≤ HalfIntegerTime.integer t₂}

Simp Lemmas for Time Conversions

@[simp]

theorem IntegerTimeStep.toHalfIntegerTime_isInteger (t : IntegerTimeStep) : t.toHalfIntegerTime.isInteger = true

@[simp]

theorem MeasurementTimeStep.toHalfIntegerTime_isHalfInteger (t : MeasurementTimeStep) : t.toHalfIntegerTime.isHalfInteger = true

@[simp]

theorem IntegerTimeStep.nextMeasurementTime_prevIntegerTime (t : IntegerTimeStep) : t.nextMeasurementTime.prevIntegerTime = t

@[simp]

theorem MeasurementTimeStep.prevIntegerTime_nextMeasurementTime (t : MeasurementTimeStep) : t.prevIntegerTime.nextMeasurementTime = t

@[simp]

theorem IntegerTimeStep.prevMeasurementTime_nextIntegerTime (t : IntegerTimeStep) : t.prevMeasurementTime.nextIntegerTime = t

@[simp]

theorem MeasurementTimeStep.nextIntegerTime_prevMeasurementTime (t : MeasurementTimeStep) : t.nextIntegerTime.prevMeasurementTime = t

Summary

This formalization captures the half-integer time step convention for the fault-tolerant gauging measurement procedure:

1. Integer time steps (t = 0, 1, 2, ...):

   • Associated with qubit states and Pauli space-errors
   • A Pauli error 'at time t' affects the state between measurements at t - 1/2 and t + 1/2

2. Half-integer time steps (t + 1/2):

   • Associated with measurements and measurement errors
   • A measurement 'at time t + 1/2' occurs between qubit states at times t and t + 1

3. Key time points:

   • t₀: Start of the procedure
   • tᵢ: Time of initial gauging (edge initialization, first A_v measurements at tᵢ ± 1/2)
   • tₒ: Time of final ungauging (last A_v measurements, edge readout at tₒ ± 1/2)

Key properties proven:

• measurement_between_states: Measurement at t + 1/2 is between states at t and t + 1
• error_between_measurements: Error at t is between measurements at t - 1/2 and t + 1/2
• spaceFault_between_measurements: Space faults occur between measurement rounds
• timeFault_between_states: Time faults occur between state times
• Ordering and conversion lemmas for half-integer time arithmetic