Definition 10: Fault-Tolerant Gauging Procedure

Statement

The fault-tolerant gauging measurement procedure for measuring a logical operator L in an [[n,k,d]] stabilizer code using a connected graph G = (V, E) consists of three phases:

1. Phase 1 (Pre-deformation): Measure original stabilizer checks for d rounds
2. Phase 2 (Deformed code): Initialize edge qubits, measure Gauss's law, flux, and deformed checks for d rounds
3. Phase 3 (Post-deformation): Measure Z_e on edge qubits to ungauge, resume original checks for d rounds

Main Results

• FaultTolerantGaugingProcedure: The procedure data with all three phases
• GaugingPhase: The three phases as an inductive type
• phaseOf: Which phase a given time step belongs to
• FTGaugingMeasurement: The type of all measurements across the procedure
• measurementPhase, measurementTime: Phase/time assignment for measurements
• Phase timing and measurement counting theorems

Phase Type

inductive GaugingPhase : Type

The three phases of the fault-tolerant gauging procedure.

• preDeformation : GaugingPhase
• deformedCode : GaugingPhase
• postDeformation : GaugingPhase

instance instDecidableEqGaugingPhase : DecidableEq GaugingPhase

Equations

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

def instReprGaugingPhase.repr : GaugingPhase → ℕ → Std.Format

Equations

• instReprGaugingPhase.repr GaugingPhase.preDeformation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "GaugingPhase.preDeformation")).group prec✝
• instReprGaugingPhase.repr GaugingPhase.deformedCode prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "GaugingPhase.deformedCode")).group prec✝
• instReprGaugingPhase.repr GaugingPhase.postDeformation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "GaugingPhase.postDeformation")).group prec✝

instance instReprGaugingPhase : Repr GaugingPhase

Equations

• instReprGaugingPhase = { reprPrec := instReprGaugingPhase.repr }

instance GaugingPhase.instFintype : Fintype GaugingPhase

Equations

• GaugingPhase.instFintype = { elems := {GaugingPhase.preDeformation, GaugingPhase.deformedCode, GaugingPhase.postDeformation}, complete := GaugingPhase.instFintype._proof_1 }

theorem GaugingPhase.card_eq : Fintype.card GaugingPhase = 3

Measurement Labels

structure PreDeformationMeasurement (J : Type u_1) (d : ℕ) : Type u_1

Phase 1 measurement: original check j at round r.

• checkIdx : J
• round : Fin d

def instDecidableEqPreDeformationMeasurement.decEq {J✝ : Type u_1} {d✝ : ℕ} [DecidableEq J✝] (x✝ x✝¹ : PreDeformationMeasurement J✝ d✝) : Decidable (x✝ = x✝¹)

Equations

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

instance instDecidableEqPreDeformationMeasurement {J✝ : Type u_1} {d✝ : ℕ} [DecidableEq J✝] : DecidableEq (PreDeformationMeasurement J✝ d✝)

Equations

• instDecidableEqPreDeformationMeasurement = instDecidableEqPreDeformationMeasurement.decEq

instance instFintypePreDeformationMeasurement {J : Type u_1} [Fintype J] {d : ℕ} : Fintype (PreDeformationMeasurement J d)

Equations

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

inductive DeformedCodeMeasurement (V : Type u_1) (C : Type u_2) (J : Type u_3) (d : ℕ) : Type (max (max u_1 u_2) u_3)

Phase 2 measurement: Gauss (V), flux (C), or deformed (J) at round r.

• gaussLaw {V : Type u_1} {C : Type u_2} {J : Type u_3} {d : ℕ} (v : V) (round : Fin d) : DeformedCodeMeasurement V C J d
• flux {V : Type u_1} {C : Type u_2} {J : Type u_3} {d : ℕ} (p : C) (round : Fin d) : DeformedCodeMeasurement V C J d
• deformed {V : Type u_1} {C : Type u_2} {J : Type u_3} {d : ℕ} (j : J) (round : Fin d) : DeformedCodeMeasurement V C J d

def instDecidableEqDeformedCodeMeasurement.decEq {V✝ : Type u_1} {C✝ : Type u_2} {J✝ : Type u_3} {d✝ : ℕ} [DecidableEq V✝] [DecidableEq C✝] [DecidableEq J✝] (x✝ x✝¹ : DeformedCodeMeasurement V✝ C✝ J✝ d✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqDeformedCodeMeasurement.decEq (DeformedCodeMeasurement.gaussLaw v round) (DeformedCodeMeasurement.flux p round_1) = isFalse ⋯
• instDecidableEqDeformedCodeMeasurement.decEq (DeformedCodeMeasurement.gaussLaw v round) (DeformedCodeMeasurement.deformed j round_1) = isFalse ⋯
• instDecidableEqDeformedCodeMeasurement.decEq (DeformedCodeMeasurement.flux p round) (DeformedCodeMeasurement.gaussLaw v round_1) = isFalse ⋯
• instDecidableEqDeformedCodeMeasurement.decEq (DeformedCodeMeasurement.flux p round) (DeformedCodeMeasurement.deformed j round_1) = isFalse ⋯
• instDecidableEqDeformedCodeMeasurement.decEq (DeformedCodeMeasurement.deformed j round) (DeformedCodeMeasurement.gaussLaw v round_1) = isFalse ⋯
• instDecidableEqDeformedCodeMeasurement.decEq (DeformedCodeMeasurement.deformed j round) (DeformedCodeMeasurement.flux p round_1) = isFalse ⋯

instance instDecidableEqDeformedCodeMeasurement {V✝ : Type u_1} {C✝ : Type u_2} {J✝ : Type u_3} {d✝ : ℕ} [DecidableEq V✝] [DecidableEq C✝] [DecidableEq J✝] : DecidableEq (DeformedCodeMeasurement V✝ C✝ J✝ d✝)

Equations

• instDecidableEqDeformedCodeMeasurement = instDecidableEqDeformedCodeMeasurement.decEq

instance instFintypeDeformedCodeMeasurement {V : Type u_1} {C : Type u_2} {J : Type u_3} [Fintype V] [Fintype C] [Fintype J] {d : ℕ} : Fintype (DeformedCodeMeasurement V C J d)

Equations

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

inductive PostDeformationMeasurement (J : Type u_1) (E : Type u_2) (d : ℕ) : Type (max u_1 u_2)

Phase 3 measurement: edge Z or original check at round r.

• edgeZ {J : Type u_1} {E : Type u_2} {d : ℕ} (e : E) : PostDeformationMeasurement J E d
• originalCheck {J : Type u_1} {E : Type u_2} {d : ℕ} (j : J) (round : Fin d) : PostDeformationMeasurement J E d

instance instDecidableEqPostDeformationMeasurement {J✝ : Type u_1} {E✝ : Type u_2} {d✝ : ℕ} [DecidableEq J✝] [DecidableEq E✝] : DecidableEq (PostDeformationMeasurement J✝ E✝ d✝)

Equations

• instDecidableEqPostDeformationMeasurement = instDecidableEqPostDeformationMeasurement.decEq

def instDecidableEqPostDeformationMeasurement.decEq {J✝ : Type u_1} {E✝ : Type u_2} {d✝ : ℕ} [DecidableEq J✝] [DecidableEq E✝] (x✝ x✝¹ : PostDeformationMeasurement J✝ E✝ d✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqPostDeformationMeasurement.decEq (PostDeformationMeasurement.edgeZ a) (PostDeformationMeasurement.edgeZ b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqPostDeformationMeasurement.decEq (PostDeformationMeasurement.edgeZ e) (PostDeformationMeasurement.originalCheck j round) = isFalse ⋯
• instDecidableEqPostDeformationMeasurement.decEq (PostDeformationMeasurement.originalCheck j round) (PostDeformationMeasurement.edgeZ e) = isFalse ⋯

structure EdgeInitialization (E : Type u_1) : Type u_1

Edge qubit initialization in |0⟩ (treated as measurement per Def 7).

• edge : E

instance instDecidableEqEdgeInitialization {E✝ : Type u_1} [DecidableEq E✝] : DecidableEq (EdgeInitialization E✝)

Equations

• instDecidableEqEdgeInitialization = instDecidableEqEdgeInitialization.decEq

def instDecidableEqEdgeInitialization.decEq {E✝ : Type u_1} [DecidableEq E✝] (x✝ x✝¹ : EdgeInitialization E✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqEdgeInitialization.decEq { edge := a } { edge := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance instFintypeEdgeInitialization {E : Type u_1} [Fintype E] : Fintype (EdgeInitialization E)

Equations

• instFintypeEdgeInitialization = Fintype.ofEquiv E { toFun := fun (e : E) => { edge := e }, invFun := fun (ei : EdgeInitialization E) => ei.edge, left_inv := ⋯, right_inv := ⋯ }

inductive FTGaugingMeasurement (V : Type u_1) (C : Type u_2) (J : Type u_3) (E : Type u_4) (d : ℕ) : Type (max (max (max u_1 u_2) u_3) u_4)

All measurement labels across the entire procedure.

• phase1 {V : Type u_1} {C : Type u_2} {J : Type u_3} {E : Type u_4} {d : ℕ} (m : PreDeformationMeasurement J d) : FTGaugingMeasurement V C J E d
• edgeInit {V : Type u_1} {C : Type u_2} {J : Type u_3} {E : Type u_4} {d : ℕ} (init : EdgeInitialization E) : FTGaugingMeasurement V C J E d
• phase2 {V : Type u_1} {C : Type u_2} {J : Type u_3} {E : Type u_4} {d : ℕ} (m : DeformedCodeMeasurement V C J d) : FTGaugingMeasurement V C J E d
• phase3 {V : Type u_1} {C : Type u_2} {J : Type u_3} {E : Type u_4} {d : ℕ} (m : PostDeformationMeasurement J E d) : FTGaugingMeasurement V C J E d

def instDecidableEqFTGaugingMeasurement.decEq {V✝ : Type u_1} {C✝ : Type u_2} {J✝ : Type u_3} {E✝ : Type u_4} {d✝ : ℕ} [DecidableEq V✝] [DecidableEq C✝] [DecidableEq J✝] [DecidableEq E✝] (x✝ x✝¹ : FTGaugingMeasurement V✝ C✝ J✝ E✝ d✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.phase1 a) (FTGaugingMeasurement.phase1 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.phase1 m) (FTGaugingMeasurement.edgeInit init) = isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.phase1 m) (FTGaugingMeasurement.phase2 m_1) = isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.phase1 m) (FTGaugingMeasurement.phase3 m_1) = isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.edgeInit init) (FTGaugingMeasurement.phase1 m) = isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.edgeInit a) (FTGaugingMeasurement.edgeInit b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.edgeInit init) (FTGaugingMeasurement.phase2 m) = isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.edgeInit init) (FTGaugingMeasurement.phase3 m) = isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.phase2 m) (FTGaugingMeasurement.phase1 m_1) = isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.phase2 m) (FTGaugingMeasurement.edgeInit init) = isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.phase2 a) (FTGaugingMeasurement.phase2 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.phase2 m) (FTGaugingMeasurement.phase3 m_1) = isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.phase3 m) (FTGaugingMeasurement.phase1 m_1) = isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.phase3 m) (FTGaugingMeasurement.edgeInit init) = isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.phase3 m) (FTGaugingMeasurement.phase2 m_1) = isFalse ⋯
• instDecidableEqFTGaugingMeasurement.decEq (FTGaugingMeasurement.phase3 a) (FTGaugingMeasurement.phase3 b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance instDecidableEqFTGaugingMeasurement {V✝ : Type u_1} {C✝ : Type u_2} {J✝ : Type u_3} {E✝ : Type u_4} {d✝ : ℕ} [DecidableEq V✝] [DecidableEq C✝] [DecidableEq J✝] [DecidableEq E✝] : DecidableEq (FTGaugingMeasurement V✝ C✝ J✝ E✝ d✝)

Equations

• instDecidableEqFTGaugingMeasurement = instDecidableEqFTGaugingMeasurement.decEq

Time Steps

def phaseOf (d t : ℕ) : GaugingPhase

Determine which phase a time step belongs to.

Equations

• phaseOf d t = if t < d then GaugingPhase.preDeformation else if t < 2 * d then GaugingPhase.deformedCode else GaugingPhase.postDeformation

@[simp]

theorem phaseOf_preDeformation {d t : ℕ} (ht : t < d) : phaseOf d t = GaugingPhase.preDeformation

@[simp]

theorem phaseOf_deformedCode {d t : ℕ} (h1 : d ≤ t) (h2 : t < 2 * d) : phaseOf d t = GaugingPhase.deformedCode

@[simp]

theorem phaseOf_postDeformation {d t : ℕ} (ht : 2 * d ≤ t) : phaseOf d t = GaugingPhase.postDeformation

Fault-Tolerant Gauging Procedure

structure FaultTolerantGaugingProcedure {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) : Type (max u_1 u_3)

The fault-tolerant gauging measurement procedure for measuring a logical operator L in an [[n,k,d]] stabilizer code using a connected graph G. Bundles: code distance d, original code data, gauging input, deformed code data, and cycle parity condition.

• d : ℕ

  The code distance d: number of rounds per phase

• d_pos : 0 < self.d

  d ≥ 1 (meaningful code distance)

• checks_commute (i j : J) : (checks i).PauliCommute (checks j)

  The original stabilizer code checks pairwise commute

• gaugingInput : GaugingMeasurement.GaugingInput G

  The gauging input: base vertex and connectivity

• deformedData : DeformedCode.DeformedCodeData G checks

  The deformed code data: edge-paths satisfying boundary conditions

• cycleParity (c : C) (v : V) : Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card

  Cycle parity: each vertex incident to even edges in each cycle

Phase Timing

def FaultTolerantGaugingProcedure.phase2Start {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) : ℕ

Phase 2 begins at time d.

Equations

• proc.phase2Start = proc.d

def FaultTolerantGaugingProcedure.phase3Start {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) : ℕ

Phase 3 begins at time 2d.

Equations

• proc.phase3Start = 2 * proc.d

def FaultTolerantGaugingProcedure.procedureEnd {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) : ℕ

The procedure ends at time 3d.

Equations

• proc.procedureEnd = 3 * proc.d

@[simp]

theorem FaultTolerantGaugingProcedure.phase2Start_eq {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.d

@[simp]

theorem FaultTolerantGaugingProcedure.phase3Start_eq {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.phase3Start = 2 * proc.d

@[simp]

theorem FaultTolerantGaugingProcedure.procedureEnd_eq {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.procedureEnd = 3 * proc.d

theorem FaultTolerantGaugingProcedure.phase1_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.d

theorem FaultTolerantGaugingProcedure.phase2_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.phase3Start - proc.phase2Start = proc.d

theorem FaultTolerantGaugingProcedure.phase3_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.procedureEnd - proc.phase3Start = proc.d

theorem FaultTolerantGaugingProcedure.total_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.procedureEnd = 3 * proc.d

theorem FaultTolerantGaugingProcedure.phase2Start_le_phase3Start {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

theorem FaultTolerantGaugingProcedure.phase3Start_le_procedureEnd {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.phase3Start ≤ proc.procedureEnd

Measurement Label Type

@[reducible, inline]

abbrev FaultTolerantGaugingProcedure.MeasLabel {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) : Type (max (max (max u_1 u_2) u_3) u_1)

The full measurement label type for this procedure.

Equations

• proc.MeasLabel = FTGaugingMeasurement V C J (↑G.edgeSet) proc.d

Measurement Phase Assignment

def FaultTolerantGaugingProcedure.measurementPhase {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.MeasLabel → GaugingPhase

Which phase a measurement belongs to.

Equations

• proc.measurementPhase (FTGaugingMeasurement.phase1 m) = GaugingPhase.preDeformation
• proc.measurementPhase (FTGaugingMeasurement.edgeInit init) = GaugingPhase.deformedCode
• proc.measurementPhase (FTGaugingMeasurement.phase2 m) = GaugingPhase.deformedCode
• proc.measurementPhase (FTGaugingMeasurement.phase3 m) = GaugingPhase.postDeformation

@[simp]

theorem FaultTolerantGaugingProcedure.measurementPhase_phase1 {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) (m : PreDeformationMeasurement J proc.d) : proc.measurementPhase (FTGaugingMeasurement.phase1 m) = GaugingPhase.preDeformation

@[simp]

theorem FaultTolerantGaugingProcedure.measurementPhase_edgeInit {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) (ei : EdgeInitialization ↑G.edgeSet) : proc.measurementPhase (FTGaugingMeasurement.edgeInit ei) = GaugingPhase.deformedCode

@[simp]

theorem FaultTolerantGaugingProcedure.measurementPhase_phase2 {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) (m : DeformedCodeMeasurement V C J proc.d) : proc.measurementPhase (FTGaugingMeasurement.phase2 m) = GaugingPhase.deformedCode

@[simp]

theorem FaultTolerantGaugingProcedure.measurementPhase_phase3 {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) (m : PostDeformationMeasurement J (↑G.edgeSet) proc.d) : proc.measurementPhase (FTGaugingMeasurement.phase3 m) = GaugingPhase.postDeformation

Integer Time Assignment

def FaultTolerantGaugingProcedure.measurementTime {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.MeasLabel → ℕ

The integer time associated with a measurement.

Equations

• proc.measurementTime (FTGaugingMeasurement.phase1 m) = ↑m.round
• proc.measurementTime (FTGaugingMeasurement.edgeInit init) = proc.d
• proc.measurementTime (FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.gaussLaw v r)) = proc.d + ↑r
• proc.measurementTime (FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.flux p r)) = proc.d + ↑r
• proc.measurementTime (FTGaugingMeasurement.phase2 (DeformedCodeMeasurement.deformed j r)) = proc.d + ↑r
• proc.measurementTime (FTGaugingMeasurement.phase3 (PostDeformationMeasurement.edgeZ e)) = 2 * proc.d + 0
• proc.measurementTime (FTGaugingMeasurement.phase3 (PostDeformationMeasurement.originalCheck j r)) = 2 * proc.d + ↑r

theorem FaultTolerantGaugingProcedure.measurementTime_phase1_lt {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) (pm : PreDeformationMeasurement J proc.d) : proc.measurementTime (FTGaugingMeasurement.phase1 pm) < proc.d

theorem FaultTolerantGaugingProcedure.measurementTime_phase2_ge {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) (dm : DeformedCodeMeasurement V C J proc.d) : proc.d ≤ proc.measurementTime (FTGaugingMeasurement.phase2 dm)

theorem FaultTolerantGaugingProcedure.measurementTime_phase2_lt {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) (dm : DeformedCodeMeasurement V C J proc.d) : proc.measurementTime (FTGaugingMeasurement.phase2 dm) < 2 * proc.d

theorem FaultTolerantGaugingProcedure.measurementTime_phase3_ge {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) (pm : PostDeformationMeasurement J (↑G.edgeSet) proc.d) : 2 * proc.d ≤ proc.measurementTime (FTGaugingMeasurement.phase3 pm)

theorem FaultTolerantGaugingProcedure.measurementTime_phase3_lt {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) (pm : PostDeformationMeasurement J (↑G.edgeSet) proc.d) : proc.measurementTime (FTGaugingMeasurement.phase3 pm) < 3 * proc.d

theorem FaultTolerantGaugingProcedure.measurementTime_edgeInit {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) (ei : EdgeInitialization ↑G.edgeSet) : proc.measurementTime (FTGaugingMeasurement.edgeInit ei) = proc.d

theorem FaultTolerantGaugingProcedure.measurementTime_consistent_with_phase {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) (m : proc.MeasLabel) : phaseOf proc.d (proc.measurementTime m) = proc.measurementPhase m

Measurement time is consistent with phase assignment.

Phase Predicates

def FaultTolerantGaugingProcedure.isPhase1 {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.MeasLabel → Bool

A measurement label belongs to Phase 1.

Equations

• proc.isPhase1 (FTGaugingMeasurement.phase1 m) = true
• proc.isPhase1 x✝ = false

def FaultTolerantGaugingProcedure.isPhase2 {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.MeasLabel → Bool

A measurement label belongs to Phase 2.

Equations

• proc.isPhase2 (FTGaugingMeasurement.phase2 m) = true
• proc.isPhase2 (FTGaugingMeasurement.edgeInit init) = true
• proc.isPhase2 x✝ = false

def FaultTolerantGaugingProcedure.isPhase3 {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.MeasLabel → Bool

A measurement label belongs to Phase 3.

Equations

• proc.isPhase3 (FTGaugingMeasurement.phase3 m) = true
• proc.isPhase3 x✝ = false

Qubit Types

@[reducible, inline]

abbrev FaultTolerantGaugingProcedure.ProcedureQubits {V : Type u_1} {G : SimpleGraph V} : Type u_1

The qubit type for the procedure: extended system V ⊕ E(G).

Equations

• FaultTolerantGaugingProcedure.ProcedureQubits = GaussFlux.ExtQubit G

Operators Being Measured in Phase 2

def FaultTolerantGaugingProcedure.phase2Operator {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) (dm : DeformedCodeMeasurement V C J proc.d) : PauliOp (GaussFlux.ExtQubit G)

The Pauli operator for a Phase 2 measurement.

Equations

• proc.phase2Operator (DeformedCodeMeasurement.gaussLaw v r) = DeformedCode.gaussLawChecks G v
• proc.phase2Operator (DeformedCodeMeasurement.flux p r) = DeformedCode.fluxChecks G cycles p
• proc.phase2Operator (DeformedCodeMeasurement.deformed j r) = DeformedCode.deformedOriginalChecks G checks proc.deformedData j

theorem FaultTolerantGaugingProcedure.phase2Operator_is_allChecks {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) (dm : DeformedCodeMeasurement V C J proc.d) : ∃ (ci : DeformedCode.CheckIndex V C J), proc.phase2Operator dm = DeformedCode.allChecks G cycles checks proc.deformedData ci

Each Phase 2 operator is a check of the deformed code.

theorem FaultTolerantGaugingProcedure.phase2Operators_commute {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) (dm₁ dm₂ : DeformedCodeMeasurement V C J proc.d) : (proc.phase2Operator dm₁).PauliCommute (proc.phase2Operator dm₂)

All Phase 2 measurements pairwise commute.

theorem FaultTolerantGaugingProcedure.phase2Operators_selfInverse {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) (dm : DeformedCodeMeasurement V C J proc.d) : proc.phase2Operator dm * proc.phase2Operator dm = 1

All Phase 2 operators are self-inverse.

Phase 2 Check Identification

theorem FaultTolerantGaugingProcedure.phase2_gaussLaw_eq {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) (r : Fin proc.d) : proc.phase2Operator (DeformedCodeMeasurement.gaussLaw v r) = DeformedCode.gaussLawChecks G v

theorem FaultTolerantGaugingProcedure.phase2_flux_eq {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 : Fin proc.d) : proc.phase2Operator (DeformedCodeMeasurement.flux p r) = DeformedCode.fluxChecks G cycles p

theorem FaultTolerantGaugingProcedure.phase2_deformed_eq {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) (j : J) (r : Fin proc.d) : proc.phase2Operator (DeformedCodeMeasurement.deformed j r) = DeformedCode.deformedOriginalChecks G checks proc.deformedData j

theorem FaultTolerantGaugingProcedure.phase2_gauss_product_eq_logical {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, proc.phase2Operator (DeformedCodeMeasurement.gaussLaw v ⟨0, ⋯⟩) = GaussFlux.logicalOp G

The product of all Gauss's law operators equals the logical L.

Detectors

def FaultTolerantGaugingProcedure.phase1RepeatedDetector {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) (j : J) (r r' : Fin proc.d) (_hr : ↑r + 1 = ↑r') : Detector proc.MeasLabel

Repeated measurement detector for consecutive Phase 1 rounds.

Equations

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

def FaultTolerantGaugingProcedure.phase2RepeatedDetector_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) (r r' : Fin proc.d) (_hr : ↑r + 1 = ↑r') : Detector proc.MeasLabel

Repeated measurement detector for Gauss's law in Phase 2.

Equations

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

def FaultTolerantGaugingProcedure.phase2RepeatedDetector_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) (p : C) (r r' : Fin proc.d) (_hr : ↑r + 1 = ↑r') : Detector proc.MeasLabel

Repeated measurement detector for flux in Phase 2.

Equations

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

def FaultTolerantGaugingProcedure.phase2RepeatedDetector_deformed {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) (j : J) (r r' : Fin proc.d) (_hr : ↑r + 1 = ↑r') : Detector proc.MeasLabel

Repeated measurement detector for deformed checks in Phase 2.

Equations

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

def FaultTolerantGaugingProcedure.edgeInitDetector {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) (e : ↑G.edgeSet) : Detector proc.MeasLabel

Edge initialization detector: init |0⟩ at t_i and Z_e measurement at t_o.

Equations

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

def FaultTolerantGaugingProcedure.phase1_to_phase2_detector {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) (j : J) (r_last r_first : Fin proc.d) (_h_last : ↑r_last + 1 = proc.d) (_h_first : ↑r_first = 0) : Detector proc.MeasLabel

Boundary detector: last Phase 1 round to first Phase 2 round.

Equations

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

def FaultTolerantGaugingProcedure.phase2_to_phase3_detector {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) (j : J) (r_last r_first : Fin proc.d) (_h_last : ↑r_last + 1 = proc.d) (_h_first : ↑r_first = 0) : Detector proc.MeasLabel

Boundary detector: last Phase 2 round to first Phase 3 round.

Equations

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

Key Properties

theorem FaultTolerantGaugingProcedure.phase1_measurement_count {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) : Fintype.card (PreDeformationMeasurement J proc.d) = Fintype.card J * proc.d

Phase 1 has |J| · d measurements.

theorem FaultTolerantGaugingProcedure.phase2_measurement_count {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) : Fintype.card (DeformedCodeMeasurement V C J proc.d) = (Fintype.card V + Fintype.card C + Fintype.card J) * proc.d

Phase 2 has (|V| + |C| + |J|) · d measurements.

theorem FaultTolerantGaugingProcedure.edgeInit_count {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : Fintype.card (EdgeInitialization ↑G.edgeSet) = Fintype.card ↑G.edgeSet

Edge initialization count is |E|.

Gauging Sign

def FaultTolerantGaugingProcedure.gaugingSign {V : Type u_1} [Fintype V] (gaussOutcomes : V → ZMod 2) : ZMod 2

The gauging measurement sign from Phase 2 Gauss outcomes.

Equations

• FaultTolerantGaugingProcedure.gaugingSign gaussOutcomes = ∑ v : V, gaussOutcomes v

theorem FaultTolerantGaugingProcedure.gaugingSign_zero_or_one {V : Type u_1} [Fintype V] [DecidableEq V] (gaussOutcomes : V → ZMod 2) : gaugingSign gaussOutcomes = 0 ∨ gaugingSign gaussOutcomes = 1

theorem FaultTolerantGaugingProcedure.gaugingSign_eq_measurementSign {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (gaussOutcomes : V → ZMod 2) (edgeOutcomes : ↑G.edgeSet → ZMod 2) : gaugingSign gaussOutcomes = GaugingMeasurement.measurementSign G { gaussOutcome := gaussOutcomes, edgeOutcome := edgeOutcomes }

The sign from the FT procedure agrees with the Def 5 measurement sign.

Spacetime Fault Model

@[reducible, inline]

abbrev FaultTolerantGaugingProcedure.ProcedureFault {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) : Type (max u_1 (max u_1 u_2) u_3)

A spacetime fault in the fault-tolerant gauging procedure.

Equations

• proc.ProcedureFault = SpacetimeFault (GaussFlux.ExtQubit G) ℕ proc.MeasLabel

Phase 2 Consistency

theorem FaultTolerantGaugingProcedure.phase2_gaussLaw_pure_X {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) (r : Fin proc.d) : (proc.phase2Operator (DeformedCodeMeasurement.gaussLaw v r)).zVec = 0

Gauss's law checks in Phase 2 are pure X-type.

theorem FaultTolerantGaugingProcedure.phase2_flux_pure_Z {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 : Fin proc.d) : (proc.phase2Operator (DeformedCodeMeasurement.flux p r)).xVec = 0

Flux checks in Phase 2 are pure Z-type.

theorem FaultTolerantGaugingProcedure.phase2_deformed_noXOnEdges {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) (j : J) (r : Fin proc.d) (e : ↑G.edgeSet) : (proc.phase2Operator (DeformedCodeMeasurement.deformed j r)).xVec (Sum.inr e) = 0

Deformed checks in Phase 2 have no X-support on edge qubits.