Rem_6: Circuit Implementation of the Gauging Procedure

Statement

The gauging procedure can be implemented by a quantum circuit with no additional ancilla qubits beyond the edge qubits. After initializing the edge qubits in |0⟩, perform the entangling circuit ∏v ∏{e ∋ v} CX_{v→e} where CX_{v→e} is a controlled-X gate with control qubit v and target qubit e. Next, projectively measure X_v on all vertices v ∈ G and keep the post-measurement state. Then repeat the same entangling circuit ∏v ∏{e ∋ v} CX_{v→e}. Finally, measure Z_e on all edge qubits and discard them.

Main Definitions

• CircuitStep : The steps of the gauging circuit
• GaugingCircuit : The complete gauging circuit specification
• CXGate : A controlled-X (CNOT) gate specification
• EntanglingCircuit : The product ∏v ∏{e ∋ v} CX_{v→e}

Main Results

• no_additional_ancilla : The circuit uses only edge qubits as ancilla
• circuit_sequence : The complete circuit is init → entangle → measure X → entangle → measure Z
• entangling_circuit_eq : The two entangling circuits are identical

Key Properties

The circuit has five phases:

1. Initialize edge qubits in |0⟩
2. Apply entangling circuit ∏v ∏{e ∋ v} CX_{v→e}
3. Measure X_v on all vertices and keep post-measurement state
4. Apply the same entangling circuit again
5. Measure Z_e on all edges and discard

Controlled-X (CNOT) Gate

structure QEC1.CXGate (QubitType : Type u_1) : Type u_1

A controlled-X gate specification with control and target qubits

• control : QubitType

  The control qubit

• target : QubitType

  The target qubit

• control_ne_target : self.control ≠ self.target

  Control and target are different

instance QEC1.instDecidableEqCXGate {QubitType : Type u_1} [DecidableEq QubitType] : DecidableEq (CXGate QubitType)

Equations

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

Circuit Steps

inductive QEC1.CircuitPhase : Type

The phases of the gauging circuit

• InitializeEdges : CircuitPhase

  Phase 1: Initialize edge qubits in |0⟩

• FirstEntangling : CircuitPhase

  Phase 2: Apply first entangling circuit ∏v ∏{e ∋ v} CX_{v→e}

• MeasureXVertices : CircuitPhase

  Phase 3: Measure X_v on all vertices

• SecondEntangling : CircuitPhase

  Phase 4: Apply second entangling circuit (same as first)

• MeasureZEdges : CircuitPhase

  Phase 5: Measure Z_e on all edges and discard

instance QEC1.instDecidableEqCircuitPhase : DecidableEq CircuitPhase

Equations

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

def QEC1.instReprCircuitPhase.repr : CircuitPhase → ℕ → Std.Format

Equations

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

instance QEC1.instReprCircuitPhase : Repr CircuitPhase

Equations

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

def QEC1.CircuitPhase.toNat : CircuitPhase → ℕ

The natural ordering of circuit phases

Equations

• QEC1.CircuitPhase.InitializeEdges.toNat = 0
• QEC1.CircuitPhase.FirstEntangling.toNat = 1
• QEC1.CircuitPhase.MeasureXVertices.toNat = 2
• QEC1.CircuitPhase.SecondEntangling.toNat = 3
• QEC1.CircuitPhase.MeasureZEdges.toNat = 4

instance QEC1.CircuitPhase.instFintype : Fintype CircuitPhase

Equations

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

theorem QEC1.CircuitPhase.num_phases : Fintype.card CircuitPhase = 5

The circuit has exactly 5 phases

instance QEC1.CircuitPhase.instLT : LT CircuitPhase

Phase ordering

Equations

• QEC1.CircuitPhase.instLT = { lt := fun (p q : QEC1.CircuitPhase) => p.toNat < q.toNat }

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

Equations

• p.instDecidableRelLt q = p.toNat.decLt q.toNat

@[simp]

theorem QEC1.CircuitPhase.initializeEdges_first (p : CircuitPhase) : InitializeEdges.toNat ≤ p.toNat

InitializeEdges is the first phase

@[simp]

theorem QEC1.CircuitPhase.measureZEdges_last (p : CircuitPhase) : p.toNat ≤ MeasureZEdges.toNat

MeasureZEdges is the last phase

Entangling Circuit Structure

structure QEC1.EntanglingCircuit {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Type u_1

The entangling circuit ∏v ∏{e ∋ v} CX_{v→e} for a graph G.

For each vertex v, for each edge e incident to v, apply CX with control v and target e. The edges are represented as Sym2 V elements from the graph's edge set.

• graph : SimpleGraph V

  The underlying graph

• gates_spec (v : V) (e : Sym2 V) : e ∈ G.incidenceFinset v → CXGate (V ⊕ Sym2 V)

  The CX gates are parameterized by (vertex, incident edge) pairs

theorem QEC1.EntanglingCircuit.num_gates_eq_twice_edges {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (_E : EntanglingCircuit G) : ∑ v : V, G.degree v = 2 * G.edgeFinset.card

The number of CX gates equals ∑_v deg(v) = 2|E|

theorem QEC1.EntanglingCircuit.vertex_contributes_degree {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (v : V) : (G.incidenceFinset v).card = G.degree v

Each vertex contributes deg(v) CX gates

Measurement Specifications

structure QEC1.XMeasurementSpec (QubitType : Type u_2) [DecidableEq QubitType] : Type u_2

Specification of measuring Pauli X on a set of qubits

• qubits : Finset QubitType

  The qubits to measure

• keep : QubitType → Bool

  Whether to keep or discard each qubit after measurement

structure QEC1.ZMeasurementSpec (QubitType : Type u_2) [DecidableEq QubitType] : Type u_2

Specification of measuring Pauli Z on a set of qubits

• qubits : Finset QubitType

  The qubits to measure

• keep : QubitType → Bool

  Whether to keep or discard each qubit after measurement

Complete Gauging Circuit

structure QEC1.GaugingCircuit {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : Type u_1

The complete gauging circuit implementing the gauging procedure.

The circuit uses:

• Vertex qubits (V): the original code qubits in supp(L)
• Edge qubits (E_G): auxiliary qubits, one per edge

No additional ancilla qubits are required beyond the edge qubits.

The circuit proceeds in 5 phases:

1. Initialize edge qubits in |0⟩
2. Apply ∏v ∏{e ∋ v} CX_{v→e}
3. Measure X_v on all vertices, keep post-measurement state
4. Apply ∏v ∏{e ∋ v} CX_{v→e} (same circuit as step 2)
5. Measure Z_e on all edges and discard

• graph : SimpleGraph V

  The underlying graph

• entangling1 : EntanglingCircuit G

  First entangling circuit

• xMeasurement : XMeasurementSpec V

  X measurement on vertices (keep the state)

• entangling2 : EntanglingCircuit G

  Second entangling circuit (should be identical to first)

• zMeasurement : ZMeasurementSpec (Sym2 V)

  Z measurement on edges (discard after)

• entangling_identical : self.entangling1 = self.entangling2

  The two entangling circuits are identical

• x_covers_all : self.xMeasurement.qubits = Finset.univ

  X measurement covers all vertices

• x_keeps (v : V) : self.xMeasurement.keep v = true

  X measurement keeps qubits

• z_covers_all : self.zMeasurement.qubits = G.edgeFinset

  Z measurement covers all edges

• z_discards (e : Sym2 V) : self.zMeasurement.keep e = false

  Z measurement discards qubits

Key Properties

theorem QEC1.GaugingCircuit.entangling_circuits_identical {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (C : GaugingCircuit G) : C.entangling1 = C.entangling2

The two entangling circuits are identical

theorem QEC1.GaugingCircuit.edge_qubits_initialized {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (_C : GaugingCircuit G) (_e : Sym2 V) (_he : _e ∈ G.edgeFinset) : QubitType.EdgeQubit.initialState = QubitType.InitialState.zero

All edge qubits are initialized (from Rem_2 convention)

theorem QEC1.GaugingCircuit.x_measurement_all_vertices {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (C : GaugingCircuit G) : C.xMeasurement.qubits = Finset.univ

X measurements are performed on all vertices

theorem QEC1.GaugingCircuit.x_measurement_keeps_state {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (C : GaugingCircuit G) (v : V) : C.xMeasurement.keep v = true

X measurement keeps the post-measurement state

theorem QEC1.GaugingCircuit.z_measurement_all_edges {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (C : GaugingCircuit G) : C.zMeasurement.qubits = G.edgeFinset

Z measurements are performed on all edges

theorem QEC1.GaugingCircuit.z_measurement_discards {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (C : GaugingCircuit G) (e : Sym2 V) : C.zMeasurement.keep e = false

Z measurement discards the edge qubits

No Additional Ancilla Property

inductive QEC1.GaugingCircuit.CircuitQubit {V : Type u_1} (G : SimpleGraph V) : Type u_1

The qubit types used in the circuit

• vertex {V : Type u_1} {G : SimpleGraph V} : V → CircuitQubit G

  Vertex qubit (original code qubit)

• edge {V : Type u_1} {G : SimpleGraph V} : Sym2 V → CircuitQubit G

  Edge qubit (auxiliary gauge qubit)

instance QEC1.GaugingCircuit.instDecidableEqCircuitQubit {V✝ : Type u_2} {G✝ : SimpleGraph V✝} [DecidableEq V✝] : DecidableEq (CircuitQubit G✝)

Equations

• QEC1.GaugingCircuit.instDecidableEqCircuitQubit = QEC1.GaugingCircuit.instDecidableEqCircuitQubit.decEq

def QEC1.GaugingCircuit.instDecidableEqCircuitQubit.decEq {V✝ : Type u_2} {G✝ : SimpleGraph V✝} [DecidableEq V✝] (x✝ x✝¹ : CircuitQubit G✝) : Decidable (x✝ = x✝¹)

Equations

• QEC1.GaugingCircuit.instDecidableEqCircuitQubit.decEq (QEC1.GaugingCircuit.CircuitQubit.vertex a) (QEC1.GaugingCircuit.CircuitQubit.vertex b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• QEC1.GaugingCircuit.instDecidableEqCircuitQubit.decEq (QEC1.GaugingCircuit.CircuitQubit.vertex a) (QEC1.GaugingCircuit.CircuitQubit.edge a_1) = isFalse ⋯
• QEC1.GaugingCircuit.instDecidableEqCircuitQubit.decEq (QEC1.GaugingCircuit.CircuitQubit.edge a) (QEC1.GaugingCircuit.CircuitQubit.vertex a_1) = isFalse ⋯
• QEC1.GaugingCircuit.instDecidableEqCircuitQubit.decEq (QEC1.GaugingCircuit.CircuitQubit.edge a) (QEC1.GaugingCircuit.CircuitQubit.edge b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def QEC1.GaugingCircuit.allQubits {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (_C : GaugingCircuit G) : Finset (CircuitQubit G)

The set of all qubits used in the circuit

Equations

• _C.allQubits = Finset.image QEC1.GaugingCircuit.CircuitQubit.vertex Finset.univ ∪ Finset.image QEC1.GaugingCircuit.CircuitQubit.edge G.edgeFinset

theorem QEC1.GaugingCircuit.no_additional_ancilla {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (C : GaugingCircuit G) (q : CircuitQubit G) : q ∈ C.allQubits → (∃ (v : V), q = CircuitQubit.vertex v) ∨ ∃ e ∈ G.edgeFinset, q = CircuitQubit.edge e

No additional ancilla beyond edge qubits: every qubit is either a vertex or edge qubit

def QEC1.GaugingCircuit.CircuitQubit.isEdge {V : Type u_1} {G : SimpleGraph V} : CircuitQubit G → Bool

Helper: check if a circuit qubit is an edge qubit

Equations

• (QEC1.GaugingCircuit.CircuitQubit.edge a).isEdge = true
• (QEC1.GaugingCircuit.CircuitQubit.vertex a).isEdge = false

theorem QEC1.GaugingCircuit.ancilla_are_edges {V : Type u_1} [DecidableEq V] [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (C : GaugingCircuit G) : {q ∈ C.allQubits | q.isEdge = true} = Finset.image CircuitQubit.edge G.edgeFinset

The ancilla qubits are exactly the edge qubits

Circuit Depth Analysis

theorem QEC1.GaugingCircuit.circuit_has_five_phases : Fintype.card CircuitPhase = 5

The circuit consists of exactly 5 phases

theorem QEC1.GaugingCircuit.phase_order : CircuitPhase.InitializeEdges.toNat < CircuitPhase.FirstEntangling.toNat ∧ CircuitPhase.FirstEntangling.toNat < CircuitPhase.MeasureXVertices.toNat ∧ CircuitPhase.MeasureXVertices.toNat < CircuitPhase.SecondEntangling.toNat ∧ CircuitPhase.SecondEntangling.toNat < CircuitPhase.MeasureZEdges.toNat

The phases execute in order

Default Circuit Construction

def QEC1.mkGaugingCircuit {V : Type u_1} [DecidableEq V] [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : GaugingCircuit G

Construct the default gauging circuit for a graph G

Equations

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

def QEC1.circuitSequence : List CircuitPhase

The circuit sequence as a list of phases

Equations

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

theorem QEC1.circuitSequence_length : circuitSequence.length = 5

theorem QEC1.circuitSequence_pairwise : List.Pairwise (fun (x1 x2 : CircuitPhase) => x1 < x2) circuitSequence

The circuit sequence is strictly increasing in phase order

CX Gate Count

noncomputable def QEC1.numCXGates {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ

Total number of CX gates in one entangling circuit

Equations

• QEC1.numCXGates G = ∑ v : V, G.degree v

theorem QEC1.numCXGates_eq_twice_edges {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : numCXGates G = 2 * G.edgeFinset.card

The number of CX gates equals 2|E| (each edge contributes 2 gates)

noncomputable def QEC1.totalCXGates {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : ℕ

Total CX gates in the full circuit (both entangling rounds)

Equations

• QEC1.totalCXGates G = 2 * QEC1.numCXGates G

theorem QEC1.totalCXGates_eq_four_times_edges {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : totalCXGates G = 4 * G.edgeFinset.card

Total CX gates equals 4|E|

Summary

The gauging procedure circuit implementation:

1. Initialization: Edge qubits start in |0⟩ (no extra work for logical qubits)
2. First Entangling: ∏v ∏{e ∋ v} CX_{v→e} creates correlations
3. X Measurement: Projectively measure X on all vertices, keep results
4. Second Entangling: Repeat the same CX pattern
5. Z Measurement: Measure Z on all edges and discard

Key efficiency:

• No additional ancilla beyond edge qubits
• Number of CX gates = 4|E| (twice 2|E| per entangling round)
• Circuit depth is constant (5 phases)