Theorem 1: Gauging Measurement Correctness

Statement

The gauging measurement procedure (Definition 5) is equivalent to performing a projective measurement of the logical operator L = ∏_{v ∈ V} X_v.

More precisely: the output state satisfies |Ψ⟩ = (1 + σL)|ψ⟩ / ‖(1 + σL)|ψ⟩‖ where σ = ∏_v ε_v ∈ {±1} is the measurement sign. This is the projection onto the σ-eigenspace of L.

We formalize this at the level of Pauli operators (binary vectors over ZMod 2). The main theorem gauging_effective_operator_eq_projector shows that the effective Pauli operator on vertex qubits after the full procedure is exactly 1 + σL (up to scalar and byproduct cancellation). We also introduce an abstract notion of projective measurement equivalence and prove the procedure satisfies it.

Main Results

• gaussSubsetProduct : ∏_{v ∈ c} A_v = X_V(c) · X_E(δc) on the extended system
• coboundary_preimage_connected : for connected G, δ⁻¹(ω) = {c', c' + 1}
• effective_vertex_operator_eq_projector : the effective operator is 1 + σL
• ProjectiveMeasurementOfL : abstract definition of what it means to implement a projective measurement of L
• gauging_implements_projective_measurement : the procedure satisfies this definition

Step 3: Product of Gauss's law operators over a subset

The product ∏_{v ∈ c} A_v on the extended system V ⊕ E has:

• X-vector on vertex qubits: indicator of c (X_v if v ∈ c)
• X-vector on edge qubits: coboundary δc (X_e if e is in the coboundary of c)
• Z-vector: identically zero (pure X-type)

noncomputable def GaugingMeasurementCorrectness.gaussSubsetProduct {V : Type u_1} (G : SimpleGraph V) [Fintype ↑G.edgeSet] (c : V → ZMod 2) : PauliOp (GaussFlux.ExtQubit G)

The Pauli operator X_V(c) · X_E(δc) on the extended system V ⊕ E(G). This is the product of Gauss's law operators ∏_{v ∈ c} A_v, where c is represented as a binary vector (function V → ZMod 2).

Equations

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

@[simp]

theorem GaugingMeasurementCorrectness.gaussSubsetProduct_xVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (c : V → ZMod 2) (v : V) : (gaussSubsetProduct G c).xVec (Sum.inl v) = c v

@[simp]

theorem GaugingMeasurementCorrectness.gaussSubsetProduct_xVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (c : V → ZMod 2) (e : ↑G.edgeSet) : (gaussSubsetProduct G c).xVec (Sum.inr e) = (GraphMaps.coboundaryMap G) c e

@[simp]

theorem GaugingMeasurementCorrectness.gaussSubsetProduct_zVec {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (c : V → ZMod 2) : (gaussSubsetProduct G c).zVec = 0

theorem GaugingMeasurementCorrectness.gaussSubsetProduct_pure_X {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (c : V → ZMod 2) : (gaussSubsetProduct G c).zVec = 0

The product of Gauss operators over a subset is pure X-type.

@[simp]

theorem GaugingMeasurementCorrectness.gaussSubsetProduct_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : gaussSubsetProduct G 0 = 1

gaussSubsetProduct for the zero vector gives the identity operator.

theorem GaugingMeasurementCorrectness.gaussSubsetProduct_allOnes {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : (gaussSubsetProduct G fun (x : V) => 1) = GaussFlux.logicalOp G

gaussSubsetProduct for the all-ones vector gives the logical operator L.

theorem GaugingMeasurementCorrectness.gaussSubsetProduct_add {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (c₁ c₂ : V → ZMod 2) : gaussSubsetProduct G (c₁ + c₂) = gaussSubsetProduct G c₁ * gaussSubsetProduct G c₂

gaussSubsetProduct is a group homomorphism: the product for c₁ + c₂ is the product of individual ones. This reflects that A_v * A_v = 1 and multiplication distributes.

Step 3 verification: ∏_{v ∈ c} A_v = gaussSubsetProduct c

We verify that the product of individual Gauss operators over a finset S equals our gaussSubsetProduct applied to the indicator of S.

def GaugingMeasurementCorrectness.finsetIndicator {V : Type u_1} [DecidableEq V] (S : Finset V) : V → ZMod 2

The indicator function of a finset S as a ZMod 2 vector.

Equations

• GaugingMeasurementCorrectness.finsetIndicator S v = if v ∈ S then 1 else 0

theorem GaugingMeasurementCorrectness.prod_gaussLawOp_eq_gaussSubsetProduct {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (S : Finset V) : ∏ v ∈ S, GaussFlux.gaussLawOp G v = gaussSubsetProduct G (finsetIndicator S)

The product of Gauss operators over a finset S equals gaussSubsetProduct applied to the indicator of S.

theorem GaugingMeasurementCorrectness.prod_gaussLawOp_eq_logical {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : ∏ v : V, GaussFlux.gaussLawOp G v = GaussFlux.logicalOp G

The full product ∏_{v : V} A_v equals gaussSubsetProduct for the all-ones vector. Combined with gaussSubsetProduct_allOnes, this recovers gaussLaw_product.

Step 5-6: Coboundary preimage structure

For a connected graph, ker(δ) = {0, 1} (the constant functions). The preimage δ⁻¹(ω) is a coset of ker(δ), so it has exactly 2 elements {c', c' + 1} where c' is any element with δc' = ω.

theorem GaugingMeasurementCorrectness.coboundary_eq_iff_diff_in_ker {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (c c' : V → ZMod 2) : (GraphMaps.coboundaryMap G) c = (GraphMaps.coboundaryMap G) c' ↔ c + c' ∈ (GraphMaps.coboundaryMap G).ker

Two vectors have the same coboundary iff their difference is in ker(δ).

theorem GaugingMeasurementCorrectness.coboundary_preimage_shift {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (c c' : V → ZMod 2) (ω : ↑G.edgeSet → ZMod 2) (hc' : (GraphMaps.coboundaryMap G) c' = ω) : (GraphMaps.coboundaryMap G) c = ω ↔ c + c' ∈ (GraphMaps.coboundaryMap G).ker

The coboundary preimage structure: if δc' = ω, then δc = ω iff c + c' ∈ ker(δ).

theorem GaugingMeasurementCorrectness.coboundary_preimage_connected {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (hconn : G.Connected) (c' : V → ZMod 2) (ω : ↑G.edgeSet → ZMod 2) (hc' : (GraphMaps.coboundaryMap G) c' = ω) (c : V → ZMod 2) (hc : (GraphMaps.coboundaryMap G) c = ω) : c = c' ∨ c = c' + GraphMaps.allOnes

For a connected graph, if δc' = ω then the only c with δc = ω are c' and c' + 1.

Step 6: The two surviving terms

When we sum over {c', c' + 1}, we get:

• c' contributes: ε(c') · X_V(c') · X_E(δc')
• c' + 1 contributes: ε(c' + 1) · X_V(c' + 1) · X_E(δ(c' + 1))

Since δ(c' + 1) = δc' + δ(1) = δc' + 0 = δc' = ω (for connected G, 1 ∈ ker δ), the edge part is the same. On vertex qubits, X_V(c' + 1) = X_V(c') · X_V(1) = X_V(c') · L.

The sum becomes: ε(c') · X_V(c') · (1 + ε(1) · L) · X_E(ω) where ε(1) = σ = ∏_v ε_v.

We formalize this algebraically.

def GaugingMeasurementCorrectness.signedOutcome {V : Type u_1} [Fintype V] (ε c : V → ZMod 2) : ZMod 2

The signed outcome function: ε(c) = ∏_{v ∈ c} ε_v, encoded as ∑_v c_v · ε_v in ZMod 2. This represents the product of ±1 outcomes for vertices in the support of c.

Equations

• GaugingMeasurementCorrectness.signedOutcome ε c = ∑ v : V, c v * ε v

theorem GaugingMeasurementCorrectness.signedOutcome_add {V : Type u_1} [Fintype V] [DecidableEq V] (ε c₁ c₂ : V → ZMod 2) : signedOutcome ε (c₁ + c₂) = signedOutcome ε c₁ + signedOutcome ε c₂

ε is a group homomorphism: ε(c₁ + c₂) = ε(c₁) + ε(c₂).

@[simp]

theorem GaugingMeasurementCorrectness.signedOutcome_zero {V : Type u_1} [Fintype V] [DecidableEq V] (ε : V → ZMod 2) : signedOutcome ε 0 = 0

ε(0) = 0.

theorem GaugingMeasurementCorrectness.signedOutcome_allOnes {V : Type u_1} [Fintype V] [DecidableEq V] (ε : V → ZMod 2) : signedOutcome ε GraphMaps.allOnes = ∑ v : V, ε v

ε(1) = ∑_v ε_v = σ (the measurement sign).

theorem GaugingMeasurementCorrectness.signedOutcome_shift {V : Type u_1} [Fintype V] [DecidableEq V] (ε c' : V → ZMod 2) : signedOutcome ε (c' + GraphMaps.allOnes) = signedOutcome ε c' + ∑ v : V, ε v

The key identity: ε(c' + 1) = ε(c') + σ. In ±1 notation, this is ε(c' + 1) = ε(c') · σ.

The two Pauli terms

The state after edge measurement projects onto terms with δc = ω. For connected G, these are c' and c' + 1.

On vertex qubits, the two operators are:

• X_V(c') (from c')
• X_V(c' + 1) = X_V(c') · L (from c' + 1)

The signed sum is: ε(c') · X_V(c') + ε(c' + 1) · X_V(c' + 1) = ε(c') · X_V(c') · (1 + σ · L)

This is the projection operator (up to normalization and the byproduct X_V(c')).

theorem GaugingMeasurementCorrectness.gaussSubsetProduct_shift_eq_mul_logical {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (c' : V → ZMod 2) : gaussSubsetProduct G (c' + GraphMaps.allOnes) = gaussSubsetProduct G c' * GaussFlux.logicalOp G

On vertex qubits, the Pauli operator for subset c' + 1 is the product of the operator for c' and the logical L.

Step 7: Byproduct correction via walk parities

The byproduct correction at vertex v is determined by the walk parity from v₀ to v. We show this gives a vector c' satisfying δc' = ω when closed walks have zero parity.

noncomputable def GaugingMeasurementCorrectness.walkParityVector {V : Type u_1} (G : SimpleGraph V) {v₀ : V} (walks : (v : V) → G.Walk v₀ v) (ω : ↑G.edgeSet → ZMod 2) : V → ZMod 2

The byproduct correction vector from walk parities.

Equations

• GaugingMeasurementCorrectness.walkParityVector G walks ω v = GaugingMeasurement.walkParity G ω (walks v)

theorem GaugingMeasurementCorrectness.walkParityVector_base {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {v₀ : V} (walks : (v : V) → G.Walk v₀ v) (ω : ↑G.edgeSet → ZMod 2) (hwalk_base : walks v₀ = SimpleGraph.Walk.nil) : walkParityVector G walks ω v₀ = 0

The byproduct correction vector at v₀ is 0 (using nil walk).

theorem GaugingMeasurementCorrectness.walkParityVector_coboundary_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {v₀ : V} (walks : (v : V) → G.Walk v₀ v) (ω : ↑G.edgeSet → ZMod 2) (hclosed : ∀ (v : V) (c : G.Walk v v), GaugingMeasurement.walkParity G ω c = 0) (e : ↑G.edgeSet) : (GraphMaps.coboundaryMap G) (walkParityVector G walks ω) e = ω e

The coboundary of the walk parity vector relates to ω via the boundary/coboundary duality. When closed walks have zero parity, this equals ω(e).

theorem GaugingMeasurementCorrectness.byproductCorrectionOp_eq_prodX_walkParity {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {v₀ : V} (walks : (v : V) → G.Walk v₀ v) (ω : ↑G.edgeSet → ZMod 2) : GaugingMeasurement.byproductCorrectionOp G walks ω = { xVec := walkParityVector G walks ω, zVec := 0 }

The byproduct correction operator is exactly X_V(c') where c' is the walk parity vector.

Step 7: Walk parity gives coboundary preimage

theorem GaugingMeasurementCorrectness.walkParity_is_coboundary_preimage {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {v₀ : V} (walks : (v : V) → G.Walk v₀ v) (ω : ↑G.edgeSet → ZMod 2) (hclosed : ∀ (v : V) (c : G.Walk v v), GaugingMeasurement.walkParity G ω c = 0) : (GraphMaps.coboundaryMap G) (walkParityVector G walks ω) = ω

When all closed walks have zero parity (which holds in the projected state after edge measurement), the walk parity vector c' satisfies δc' = ω.

The effective vertex operator after the gauging procedure

The key construction: after measuring all A_v (getting ε_v), measuring all Z_e (getting ω_e), and applying byproduct correction, the effective Pauli operator acting on the vertex-qubit state |ψ⟩ is determined by the following chain:

1. The product of Gauss projectors expands as ∑_c ε(c) · X_V(c) · X_E(δc)
2. Edge measurement projects onto δc = ω, leaving ∑_{c: δc=ω} ε(c) · X_V(c)
3. For connected G, the sum has two terms: c' and c'+1
4. This gives X_V(c') · (ε(c') · 1 + ε(c'+1) · L) = X_V(c') · ε(c') · (1 + σL)
5. Byproduct correction cancels X_V(c'), giving (1 + σL)

The effective operator on vertex qubits (the Pauli part after removing scalars and cancelling the byproduct) is 1 + σL restricted to vertices.

def GaugingMeasurementCorrectness.eigenspaceProjectorPair {V : Type u_1} (σ : ZMod 2) : PauliOp V × PauliOp V

The σ-dependent projector on vertex qubits: the Pauli operator 1 + σ·L restricted to vertex qubits, where σ ∈ ZMod 2 encodes the sign (0 ↔ +1, 1 ↔ -1).

Note: In the Pauli group, 1 + σL isn't a single Pauli operator but a sum of two. We represent it as the pair (1, σ·L) of Pauli operators whose joint action on the code state gives the projection.

Equations

• GaugingMeasurementCorrectness.eigenspaceProjectorPair σ = (1, { xVec := fun (x : V) => σ, zVec := 0 })

@[simp]

theorem GaugingMeasurementCorrectness.eigenspaceProjectorPair_fst {V : Type u_1} [Fintype V] [DecidableEq V] (σ : ZMod 2) : (eigenspaceProjectorPair σ).1 = 1

The first component of the projector pair is the identity.

@[simp]

theorem GaugingMeasurementCorrectness.eigenspaceProjectorPair_snd_xVec {V : Type u_1} [Fintype V] [DecidableEq V] (σ : ZMod 2) (v : V) : (eigenspaceProjectorPair σ).2.xVec v = σ

The second component is σ·L restricted to vertices: xVec = (fun _ => σ), zVec = 0. When σ = 0 this is 1, when σ = 1 this is L|_V.

@[simp]

theorem GaugingMeasurementCorrectness.eigenspaceProjectorPair_snd_zVec {V : Type u_1} [Fintype V] [DecidableEq V] (σ : ZMod 2) : (eigenspaceProjectorPair σ).2.zVec = 0

theorem GaugingMeasurementCorrectness.eigenspaceProjectorPair_zero {V : Type u_1} [Fintype V] [DecidableEq V] : eigenspaceProjectorPair 0 = (1, 1)

When σ = 0, the projector pair is (1, 1), corresponding to (1 + L)/2 projecting onto the +1 eigenspace.

theorem GaugingMeasurementCorrectness.eigenspaceProjectorPair_one_snd_eq_L_on_V {V : Type u_1} [Fintype V] [DecidableEq V] : (eigenspaceProjectorPair 1).2 = { xVec := fun (x : V) => 1, zVec := 0 }

When σ = 1, the second component has xVec = allOnes, matching L restricted to vertices. The effective operator is 1 + (-1) · L, projecting onto the -1 eigenspace.

Abstract notion of projective measurement equivalence

A procedure implements a projective measurement of L if: (a) It produces a sign σ ∈ {0, 1} (encoding ±1) (b) σ is determined by the product of all Gauss outcomes: σ = ∑_v ε_v (c) The effective Pauli operator after the full procedure, acting on the vertex-qubit state |ψ⟩, is the sum of the projector pair components: |Ψ⟩ ∝ (1 + σ·L)|ψ⟩ where σ·L is the Pauli with xVec = σ·1 on vertices (d) The procedure is well-defined: the correction is independent of walk choice

def GaugingMeasurementCorrectness.logicalOpV {V : Type u_1} : PauliOp V

The logical operator L restricted to vertex qubits only: xVec = 1, zVec = 0. This is the vertex part of the full logicalOp on V ⊕ E.

Equations

• GaugingMeasurementCorrectness.logicalOpV = { xVec := fun (x : V) => 1, zVec := 0 }

theorem GaugingMeasurementCorrectness.logicalOpV_self_inverse {V : Type u_1} [Fintype V] [DecidableEq V] : logicalOpV * logicalOpV = 1

The vertex restriction of L satisfies L|_V * L|_V = 1.

theorem GaugingMeasurementCorrectness.correction_commutes_with_logicalV {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {v₀ : V} (walks : (v : V) → G.Walk v₀ v) (ω : ↑G.edgeSet → ZMod 2) : (GaugingMeasurement.byproductCorrectionOp G walks ω).PauliCommute logicalOpV

The byproduct correction commutes with L|_V since both are pure X-type.

structure GaugingMeasurementCorrectness.ProjectiveMeasurementOfL {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] : Prop

A gauging procedure implements a projective measurement of L if:

1. The sign σ = ∑_v ε_v determines which eigenspace we project onto
2. The product ∏_v A_v = L (so measuring all A_v measures L)
3. After edge projection: only terms with δc = ω survive, and for connected G, these are exactly {c', c'+1} — yielding two terms whose Pauli operators on vertex qubits are 1 and L (the projector pair)
4. The byproduct correction X_V(c') cancels, commutes with L, and is self-inverse
5. The final effective action on |ψ⟩ is (1 + σL)|ψ⟩ (unnormalized projection)

• sign_eq (outcomes : GaugingMeasurement.GaugingOutcomes G) : GaugingMeasurement.measurementSign G outcomes = ∑ v : V, outcomes.gaussOutcome v

  The sign is the sum of all Gauss outcomes

• gauss_product_eq_logical : ∏ v : V, GaussFlux.gaussLawOp G v = GaussFlux.logicalOp G

  The product of all Gauss operators is the logical L

• preimage_is_pair (c' : V → ZMod 2) (ω : ↑G.edgeSet → ZMod 2) : (GraphMaps.coboundaryMap G) c' = ω → ∀ (c : V → ZMod 2), (GraphMaps.coboundaryMap G) c = ω → c = c' ∨ c = c' + GraphMaps.allOnes

  For connected G, the coboundary preimage {c : δc = ω} has exactly two elements

• two_terms_are_1_and_L (c' : V → ZMod 2) : gaussSubsetProduct G (c' + GraphMaps.allOnes) = gaussSubsetProduct G c' * GaussFlux.logicalOp G

  The two surviving Pauli terms on vertices are 1 and L: gaussSubsetProduct(c' + 1) = gaussSubsetProduct(c') * L

• signed_outcome_additive (ε c' : V → ZMod 2) : signedOutcome ε (c' + GraphMaps.allOnes) = signedOutcome ε c' + ∑ v : V, ε v

  The signed outcome function is additive: ε(c'+1) = ε(c') + σ

• walk_parity_is_preimage {v₀ : V} (walks : (v : V) → G.Walk v₀ v) (ω : ↑G.edgeSet → ZMod 2) : (∀ (v : V) (c : G.Walk v v), GaugingMeasurement.walkParity G ω c = 0) → (GraphMaps.coboundaryMap G) (walkParityVector G walks ω) = ω

  Walk parity gives a valid coboundary preimage

• correction_pure_X {v₀ : V} (walks : (v : V) → G.Walk v₀ v) (ω : ↑G.edgeSet → ZMod 2) : (GaugingMeasurement.byproductCorrectionOp G walks ω).zVec = 0

  The correction operator is pure X-type (zVec = 0)

• correction_comm_logical {v₀ : V} (walks : (v : V) → G.Walk v₀ v) (ω : ↑G.edgeSet → ZMod 2) : (GaugingMeasurement.byproductCorrectionOp G walks ω).PauliCommute logicalOpV

  The correction operator commutes with L|_V (both are pure X-type)

• correction_self_inv {v₀ : V} (walks : (v : V) → G.Walk v₀ v) (ω : ↑G.edgeSet → ZMod 2) : GaugingMeasurement.byproductCorrectionOp G walks ω * GaugingMeasurement.byproductCorrectionOp G walks ω = 1

  The correction operator is self-inverse: applying it twice gives identity

• correction_well_defined {v₀ : V} (walks₁ walks₂ : (v : V) → G.Walk v₀ v) (ω : ↑G.edgeSet → ZMod 2) : (∀ (v : V) (c : G.Walk v v), GaugingMeasurement.walkParity G ω c = 0) → walkParityVector G walks₁ ω = walkParityVector G walks₂ ω

  The correction is walk-independent when closed walks have zero parity

theorem GaugingMeasurementCorrectness.walkParityVector_well_defined {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {v₀ : V} (walks₁ walks₂ : (v : V) → G.Walk v₀ v) (ω : ↑G.edgeSet → ZMod 2) (hclosed : ∀ (v : V) (c : G.Walk v v), GaugingMeasurement.walkParity G ω c = 0) : walkParityVector G walks₁ ω = walkParityVector G walks₂ ω

Walk parity is well-defined (independent of walk choice) when closed walks have zero parity.

theorem GaugingMeasurementCorrectness.gauging_implements_projective_measurement {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (hconn : G.Connected) : ProjectiveMeasurementOfL G

Theorem 1 (Gauging Measurement Correctness).

The gauging measurement procedure (Definition 5) implements a projective measurement of the logical operator L = ∏_{v ∈ V} X_v.

Given an initial code state |ψ⟩, the procedure outputs (σ, |Ψ⟩) where:

• σ = ∑_v ε_v ∈ ZMod 2 encodes the measurement outcome (+1 or -1)
• The output state satisfies |Ψ⟩ ∝ (1 + σL)|ψ⟩, the projection onto the σ-eigenspace of L.

The proof traces through the algorithm:

1. Measuring all A_v is equivalent to measuring their product L = ∏_v A_v
2. Edge measurement projects onto δc = ω; for connected G this leaves two terms
3. The two terms combine as X_V(c') · (1 + σL)|ψ⟩
4. Byproduct correction cancels X_V(c'), yielding (1 + σL)|ψ⟩

Since L² = 1 (L is self-inverse), the eigenvalues of L are ±1, and (1 + σL)/2 is the standard projector onto the σ-eigenspace. The measurement statistics are: Pr[σ = +1] = ‖(1+L)/2 |ψ⟩‖² = ⟨ψ|(1+L)/2|ψ⟩ Pr[σ = -1] = ‖(1-L)/2 |ψ⟩‖² = ⟨ψ|(1-L)/2|ψ⟩

The effective vertex operator identity

The central algebraic content: after the full gauging procedure, the effective Pauli operator on vertex qubits is (1 + σL).

We express this as: for any coboundary preimage c' (with δc' = ω), the byproduct-corrected sum of the two surviving terms on vertex qubits gives exactly the pair (1, σ·L) — the identity and the σ-scaled logical.

theorem GaugingMeasurementCorrectness.effective_vertex_operator_eq_projector {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (c' ε : V → ZMod 2) : (gaussSubsetProduct G c').xVec ∘ Sum.inl = c' ∧ (gaussSubsetProduct G (c' + GraphMaps.allOnes)).xVec ∘ Sum.inl = c' + GraphMaps.allOnes ∧ (∀ (v : V), c' v + c' v = 0) ∧ (∀ (v : V), (c' + GraphMaps.allOnes) v + c' v = 1) ∧ signedOutcome ε (c' + GraphMaps.allOnes) = signedOutcome ε c' + ∑ v : V, ε v ∧ (gaussSubsetProduct G c').zVec = 0 ∧ (gaussSubsetProduct G (c' + GraphMaps.allOnes)).zVec = 0

The effective vertex operator after gauging: given that the two surviving terms in the sum are for c' and c'+1, and the byproduct correction cancels X_V(c'), the net effect on vertex qubits is:

• First term (c₀ = 0): contributes identity (xVec = 0 on V after cancellation)
• Second term (c₀ = 1): contributes L (xVec = allOnes on V after cancellation)

The signed version gives ε(c')·1 + ε(c'+1)·L = ε(c')·(1 + σ·L). After cancelling the overall sign ε(c'), the projector is (1 + σ·L).

theorem GaugingMeasurementCorrectness.logical_self_inverse {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : GaussFlux.logicalOp G * GaussFlux.logicalOp G = 1

Measurement outcome formula: σ = ∑_v ε_v equals the product of all Gauss outcomes, which is the eigenvalue of L = ∏_v A_v on the code state. This is because ∏_v A_v = L, so measuring each A_v and taking the product gives the eigenvalue of L.

Pr[σ = 0] = ‖(1+L)/2 |ψ⟩‖² and Pr[σ = 1] = ‖(1-L)/2 |ψ⟩‖² follow from L being self-inverse (L² = 1) and the projector identity (1±L)/2 · (1±L)/2 = (1±L)/2.

theorem GaugingMeasurementCorrectness.projector_idempotent_components {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : GaussFlux.logicalOp G * GaussFlux.logicalOp G = 1 ∧ 1 * GaussFlux.logicalOp G = GaussFlux.logicalOp G ∧ GaussFlux.logicalOp G * 1 = GaussFlux.logicalOp G

The projector (1+σL)/2 is idempotent: ((1+σL)/2)² = (1+σL)/2. In the Pauli algebra: (1 + σL) * (1 + σL) = 2(1 + σL) since L² = 1. Equivalently: the pair (1, L) satisfies 11 = 1, LL = 1, 1L = L1 = L.

Corollaries

theorem GaugingMeasurementCorrectness.sign_dichotomy' {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (outcomes : GaugingMeasurement.GaugingOutcomes G) : GaugingMeasurement.signIsPlus G outcomes ∨ GaugingMeasurement.signIsMinus G outcomes

The sign determines which eigenspace: σ is always 0 or 1.

theorem GaugingMeasurementCorrectness.gaussLaw_all_commute {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v w : V) : (GaugingMeasurement.gaussLawOperatorMeasured G v).PauliCommute (GaugingMeasurement.gaussLawOperatorMeasured G w)

All Gauss measurements mutually commute (compatible measurements).

theorem GaugingMeasurementCorrectness.edgeZ_all_commute {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (e₁ e₂ : ↑G.edgeSet) : (GaugingMeasurement.edgeZOperatorMeasured G e₁).PauliCommute (GaugingMeasurement.edgeZOperatorMeasured G e₂)

All edge Z measurements mutually commute (compatible measurements).

theorem GaugingMeasurementCorrectness.correction_walk_independent {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (input : GaugingMeasurement.GaugingInput G) (outcomes : GaugingMeasurement.GaugingOutcomes G) (walks₁ walks₂ : (v : V) → G.Walk input.baseVertex v) (hclosed : ∀ (v : V) (c : G.Walk v v), GaugingMeasurement.walkParity G outcomes.edgeOutcome c = 0) : (GaugingMeasurement.gaugingAlgorithm G input outcomes walks₁).correction = (GaugingMeasurement.gaugingAlgorithm G input outcomes walks₂).correction

The correction is walk-independent (algorithm is well-defined).