Remark 9: Circuit Implementation

Statement

The gauging measurement procedure can be implemented by a quantum circuit with no additional qubits beyond the edge qubits:

1. Initialize each edge qubit e in state |0⟩_e.
2. Apply the entangling circuit ∏v ∏{e ∋ v} CX_{v → e}.
3. Measure X_v on all vertex qubits v ∈ V.
4. Apply the same entangling circuit again.
5. Measure Z_e on all edge qubits and discard them.
6. Apply byproduct corrections as in Definition 5.

Why this works: The entangling circuit transforms A_v = X_v ∏{e ∋ v} X_e into X_v (since CX{v → e} conjugates X_v → X_v X_e and X_e → X_e). So measuring X_v after the circuit is equivalent to measuring A_v before it.

Main Results

• cxConjugate : the CX conjugation action on Pauli operators
• cxConjugate_involutive : CX conjugation is involutive
• cxConjugate_mul : CX conjugation distributes over multiplication
• entanglingCircuitAction : conjugation by the full entangling circuit
• entanglingCircuitAction_involutive : applying the circuit twice = identity
• entanglingCircuit_transforms_gaussLaw : the circuit transforms A_v to X_v
• entanglingCircuit_transforms_pauliX_to_gaussLaw : inverse direction
• entanglingCircuit_preserves_symplecticInner : circuit preserves commutation
• transformed_gaussLaw_product : ∏_v X_v = L (consistency check)

CX Gate Conjugation on Pauli Operators

def CircuitImplementation.cxConjugate {W : Type u_2} [DecidableEq W] (c t : W) (_hne : c ≠ t) (P : PauliOp W) : PauliOp W

The conjugation action of CX_{control → target} on a Pauli operator.

Equations

• CircuitImplementation.cxConjugate c t _hne P = { xVec := fun (q : W) => if q = t then P.xVec q + P.xVec c else P.xVec q, zVec := fun (q : W) => if q = c then P.zVec q + P.zVec t else P.zVec q }

@[simp]

theorem CircuitImplementation.cxConjugate_xVec_control {W : Type u_2} [DecidableEq W] (c t : W) (hne : c ≠ t) (P : PauliOp W) : (cxConjugate c t hne P).xVec c = P.xVec c

@[simp]

theorem CircuitImplementation.cxConjugate_xVec_target {W : Type u_2} [DecidableEq W] (c t : W) (hne : c ≠ t) (P : PauliOp W) : (cxConjugate c t hne P).xVec t = P.xVec t + P.xVec c

@[simp]

theorem CircuitImplementation.cxConjugate_zVec_control {W : Type u_2} [DecidableEq W] (c t : W) (hne : c ≠ t) (P : PauliOp W) : (cxConjugate c t hne P).zVec c = P.zVec c + P.zVec t

@[simp]

theorem CircuitImplementation.cxConjugate_zVec_target {W : Type u_2} [DecidableEq W] (c t : W) (hne : c ≠ t) (P : PauliOp W) : (cxConjugate c t hne P).zVec t = P.zVec t

theorem CircuitImplementation.cxConjugate_involutive {W : Type u_2} [DecidableEq W] (c t : W) (hne : c ≠ t) (P : PauliOp W) : cxConjugate c t hne (cxConjugate c t hne P) = P

CX conjugation is involutive.

theorem CircuitImplementation.cxConjugate_mul {W : Type u_2} [DecidableEq W] (c t : W) (hne : c ≠ t) (P Q : PauliOp W) : cxConjugate c t hne (P * Q) = cxConjugate c t hne P * cxConjugate c t hne Q

CX conjugation distributes over Pauli multiplication.

@[simp]

theorem CircuitImplementation.cxConjugate_one {W : Type u_2} [DecidableEq W] (c t : W) (hne : c ≠ t) : cxConjugate c t hne 1 = 1

CX conjugation of basic Pauli operators

theorem CircuitImplementation.cxConjugate_pauliX_control {W : Type u_2} [DecidableEq W] (c t : W) (hne : c ≠ t) : cxConjugate c t hne (PauliOp.pauliX c) = PauliOp.pauliX c * PauliOp.pauliX t

CX_{c→t} maps X_c to X_c · X_t.

theorem CircuitImplementation.cxConjugate_pauliX_target {W : Type u_2} [DecidableEq W] (c t : W) (hne : c ≠ t) : cxConjugate c t hne (PauliOp.pauliX t) = PauliOp.pauliX t

CX_{c→t} maps X_t to X_t (unchanged).

theorem CircuitImplementation.cxConjugate_pauliZ_control {W : Type u_2} [DecidableEq W] (c t : W) (hne : c ≠ t) : cxConjugate c t hne (PauliOp.pauliZ c) = PauliOp.pauliZ c

CX_{c→t} maps Z_c to Z_c (unchanged).

theorem CircuitImplementation.cxConjugate_pauliZ_target {W : Type u_2} [DecidableEq W] (c t : W) (hne : c ≠ t) : cxConjugate c t hne (PauliOp.pauliZ t) = PauliOp.pauliZ c * PauliOp.pauliZ t

CX_{c→t} maps Z_t to Z_c · Z_t.

The Full Entangling Circuit Action

noncomputable def CircuitImplementation.entanglingCircuitAction {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] (P : PauliOp (GaussFlux.ExtQubit G)) : PauliOp (GaussFlux.ExtQubit G)

The conjugation action of the full entangling circuit ∏v ∏{e ∋ v} CX_{v→e}.

Equations

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

@[simp]

theorem CircuitImplementation.entanglingCircuitAction_xVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp (GaussFlux.ExtQubit G)) (w : V) : (entanglingCircuitAction G P).xVec (Sum.inl w) = P.xVec (Sum.inl w)

@[simp]

theorem CircuitImplementation.entanglingCircuitAction_xVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp (GaussFlux.ExtQubit G)) (e : ↑G.edgeSet) : (entanglingCircuitAction G P).xVec (Sum.inr e) = P.xVec (Sum.inr e) + ∑ v : V, if v ∈ ↑e then P.xVec (Sum.inl v) else 0

@[simp]

theorem CircuitImplementation.entanglingCircuitAction_zVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp (GaussFlux.ExtQubit G)) (w : V) : (entanglingCircuitAction G P).zVec (Sum.inl w) = P.zVec (Sum.inl w) + ∑ e ∈ GaussFlux.incidentEdges G w, P.zVec (Sum.inr e)

@[simp]

theorem CircuitImplementation.entanglingCircuitAction_zVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp (GaussFlux.ExtQubit G)) (e : ↑G.edgeSet) : (entanglingCircuitAction G P).zVec (Sum.inr e) = P.zVec (Sum.inr e)

theorem CircuitImplementation.entanglingCircuitAction_involutive {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp (GaussFlux.ExtQubit G)) : entanglingCircuitAction G (entanglingCircuitAction G P) = P

The entangling circuit action is involutive: applying it twice gives the identity.

theorem CircuitImplementation.entanglingCircuitAction_mul {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P Q : PauliOp (GaussFlux.ExtQubit G)) : entanglingCircuitAction G (P * Q) = entanglingCircuitAction G P * entanglingCircuitAction G Q

The entangling circuit action distributes over Pauli multiplication.

@[simp]

theorem CircuitImplementation.entanglingCircuitAction_one {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : entanglingCircuitAction G 1 = 1

Entangling circuit preserves symplectic inner product

theorem CircuitImplementation.entanglingCircuit_preserves_symplecticInner {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P Q : PauliOp (GaussFlux.ExtQubit G)) : (entanglingCircuitAction G P).symplecticInner (entanglingCircuitAction G Q) = P.symplecticInner Q

The entangling circuit preserves the symplectic inner product.

theorem CircuitImplementation.entanglingCircuit_preserves_commutation {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P Q : PauliOp (GaussFlux.ExtQubit G)) : (entanglingCircuitAction G P).PauliCommute (entanglingCircuitAction G Q) ↔ P.PauliCommute Q

The entangling circuit preserves Pauli commutation.

Main Theorem: Entangling Circuit Transforms A_v to X_v

theorem CircuitImplementation.entanglingCircuit_transforms_gaussLaw {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : entanglingCircuitAction G (GaussFlux.gaussLawOp G v) = PauliOp.pauliX (Sum.inl v)

Key result: The entangling circuit transforms A_v to X_v.

theorem CircuitImplementation.entanglingCircuit_transforms_pauliX_to_gaussLaw {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : entanglingCircuitAction G (PauliOp.pauliX (Sum.inl v)) = GaussFlux.gaussLawOp G v

The inverse direction: the circuit transforms X_v back to A_v.

theorem CircuitImplementation.measuring_Xv_after_circuit_eq_Av {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : entanglingCircuitAction G (GaussFlux.gaussLawOp G v) = PauliOp.pauliX (Sum.inl v)

Measuring X_v after the entangling circuit is equivalent to measuring A_v before it.

Effect on edge Z operators

theorem CircuitImplementation.entanglingCircuit_transforms_edgeZ {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (e : ↑G.edgeSet) : entanglingCircuitAction G (PauliOp.pauliZ (Sum.inr e)) = { xVec := 0, zVec := fun (q : GaussFlux.ExtQubit G) => match q with | Sum.inl w => if w ∈ ↑e then 1 else 0 | Sum.inr e' => if e' = e then 1 else 0 }

The entangling circuit transforms Z_e into Z on e and both its endpoints.

Circuit Protocol Steps

theorem CircuitImplementation.circuit_step2_transforms_Av_to_Xv {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : entanglingCircuitAction G (GaussFlux.gaussLawOp G v) = PauliOp.pauliX (Sum.inl v)

Step 2: The entangling circuit transforms A_v to X_v.

theorem CircuitImplementation.circuit_step4_undoes_step2 {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (P : PauliOp (GaussFlux.ExtQubit G)) : entanglingCircuitAction G (entanglingCircuitAction G P) = P

Step 4: Applying the entangling circuit again undoes the transformation.

theorem CircuitImplementation.steps234_equivalent_to_measuring_Av {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : entanglingCircuitAction G (PauliOp.pauliX (Sum.inl v)) = GaussFlux.gaussLawOp G v

Steps 2+3+4: Measuring X_v in the CX frame = measuring A_v in the original frame.

theorem CircuitImplementation.circuit_edge_measurement_in_original_frame {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (e : ↑G.edgeSet) : entanglingCircuitAction G (entanglingCircuitAction G (PauliOp.pauliZ (Sum.inr e))) = PauliOp.pauliZ (Sum.inr e)

After step 4, edge Z measurements are back in the original frame.

Simultaneous transformation of all Gauss operators

theorem CircuitImplementation.entanglingCircuit_transforms_all_gaussLaw {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : entanglingCircuitAction G (GaussFlux.gaussLawOp G v) = PauliOp.pauliX (Sum.inl v)

All Gauss operators are simultaneously transformed to X_v.

theorem CircuitImplementation.transformed_gaussLaw_product {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : ∏ v : V, PauliOp.pauliX (Sum.inl v) = GaussFlux.logicalOp G

The product of all transformed operators ∏_v X_v equals L (logical operator).

theorem CircuitImplementation.entanglingCircuit_preserves_logical {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : entanglingCircuitAction G (GaussFlux.logicalOp G) = GaussFlux.logicalOp G

The entangling circuit applied to L gives L.