Theorem 1: Gauging Measurement

Statement

The gauging procedure is equivalent to performing a projective measurement of the logical operator L. Specifically, applying the procedure to an initial code state |ψ⟩ yields:

• A classical outcome σ = ±1 that equals the eigenvalue of L that the state is projected onto.
• A post-measurement state proportional to (I + σL)|ψ⟩ (the projection onto σ-eigenspace of L).
• The classical outcome σ is computed as σ = ∏_{v ∈ V_G} ε_v.
• A Pauli byproduct operator X_V(c') that may need to be applied.

Main Results

• GaugingMeasurementTheorem : Main theorem formalizing the equivalence
• measuredOutcome_sigma : σ = ∏_v ε_v
• postMeasurementState_eq_projection : State is X_V(c')(I + σL)|ψ⟩
• projector_onto_eigenspace : (1/2)(I + σL) projects onto σ-eigenspace of L
• cocycle_fiber_exactly_two : For connected G, {c : δc = z} has exactly 2 elements

Part 1: Gauss Law Measurement Outcomes

Each Gauss law operator A_v is measured, giving outcome ε_v ∈ {+1, -1}. We represent outcomes in ZMod 2: 0 for +1, 1 for -1.

@[reducible, inline]

abbrev GaugingMeasurement.GaussLawOutcomes (V : Type u_4) : Type u_4

Measurement outcomes for Gauss law operators, in ZMod 2 representation. ε_v = +1 corresponds to 0, ε_v = -1 corresponds to 1.

Equations

• GaugingMeasurement.GaussLawOutcomes V = (V → ZMod 2)

def GaugingMeasurement.sigma {V : Type u_1} [Fintype V] (outcomes : GaussLawOutcomes V) : ZMod 2

The measured outcome σ = ∏_{v ∈ V_G} ε_v in ZMod 2 representation. σ = 0 means +1 (even number of -1 outcomes), σ = 1 means -1 (odd number).

Equations

• GaugingMeasurement.sigma outcomes = ∑ v : V, outcomes v

def GaugingMeasurement.epsilon {V : Type u_1} [Fintype V] (outcomes : GaussLawOutcomes V) (c : GraphWithCycles.VectorV' V) : ZMod 2

ε(c) = ∏_{v : c_v = 1} ε_v^{c_v} for a 0-cochain c. In ZMod 2: sum of outcomes where c_v = 1.

Equations

• GaugingMeasurement.epsilon outcomes c = ∑ v : V, c v * outcomes v

def GaugingMeasurement.X_V {V : Type u_1} (c : GraphWithCycles.VectorV' V) : GraphWithCycles.VectorV' V

X_V(c) = ∏_{v : c_v = 1} X_v represented by its support vector. The support is just c itself.

Equations

• GaugingMeasurement.X_V c = c

def GaugingMeasurement.L_support {V : Type u_1} : GraphWithCycles.VectorV' V

The logical operator L = ∏_v X_v has support = all-ones vector 𝟙.

Equations

• GaugingMeasurement.L_support = GraphWithCycles.allOnesV

Part 2: Key Algebraic Properties

@[simp]

theorem GaugingMeasurement.epsilon_zero {V : Type u_1} [DecidableEq V] [Fintype V] (outcomes : GaussLawOutcomes V) : epsilon outcomes 0 = 0

ε(0) = 0 (empty product is +1).

theorem GaugingMeasurement.epsilon_allOnes {V : Type u_1} [DecidableEq V] [Fintype V] (outcomes : GaussLawOutcomes V) : epsilon outcomes GraphWithCycles.allOnesV = sigma outcomes

ε(𝟙) = σ (product of all outcomes).

theorem GaugingMeasurement.epsilon_add {V : Type u_1} [DecidableEq V] [Fintype V] (outcomes : GaussLawOutcomes V) (c c' : GraphWithCycles.VectorV' V) : epsilon outcomes (c + c') = epsilon outcomes c + epsilon outcomes c'

ε is additive: ε(c + c') = ε(c) + ε(c').

theorem GaugingMeasurement.epsilon_add_allOnes {V : Type u_1} [DecidableEq V] [Fintype V] (outcomes : GaussLawOutcomes V) (c : GraphWithCycles.VectorV' V) : epsilon outcomes (c + GraphWithCycles.allOnesV) = epsilon outcomes c + sigma outcomes

ε(c + 𝟙) = ε(c) + σ.

@[simp]

theorem GaugingMeasurement.X_V_zero {V : Type u_1} [DecidableEq V] [Fintype V] : X_V 0 = 0

X_V(0) = I (trivial support).

theorem GaugingMeasurement.X_V_allOnes {V : Type u_1} [DecidableEq V] [Fintype V] : X_V GraphWithCycles.allOnesV = L_support

X_V(𝟙) = L.

theorem GaugingMeasurement.X_V_add {V : Type u_1} [DecidableEq V] [Fintype V] (c c' : GraphWithCycles.VectorV' V) : X_V c + X_V c' = X_V (c + c')

X_V(c) · X_V(c') = X_V(c + c') (XOR of supports).

theorem GaugingMeasurement.X_V_add_allOnes {V : Type u_1} [DecidableEq V] [Fintype V] (c : GraphWithCycles.VectorV' V) : X_V (c + GraphWithCycles.allOnesV) = X_V c + L_support

X_V(c + 𝟙) = X_V(c) + L.

Part 3: Cocycle Structure - ker(δ) = {0, 𝟙} for Connected Graphs

This is the key structural property from Step 5 of the proof. For connected G, the only 0-cochains with δc = 0 are 0 and 𝟙.

theorem GaugingMeasurement.ker_coboundary_two_elements {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (hconn : G.IsConnected) (c : GraphWithCycles.VectorV' V) (hc : G.coboundaryMap c = 0) : c = 0 ∨ c = GraphWithCycles.allOnesV

For connected G, if δc = 0 then c = 0 or c = 𝟙. Uses the result from Rem_7.

theorem GaugingMeasurement.ZMod2_add_eq_zero_iff (x y : ZMod 2) : x + y = 0 ↔ x = y

Helper lemma: In ZMod 2, x + y = 0 iff x = y.

theorem GaugingMeasurement.ZMod2_ne_zero_eq_one (x : ZMod 2) (h : x ≠ 0) : x = 1

Helper lemma: In ZMod 2, x ≠ 0 implies x = 1.

theorem GaugingMeasurement.ZMod2_eq_zero_or_one (x : ZMod 2) : x = 0 ∨ x = 1

Helper lemma: Every element of ZMod 2 is 0 or 1.

theorem GaugingMeasurement.ZMod2_add_eq_one_iff (x y : ZMod 2) : x + y = 1 ↔ x ≠ y

Helper lemma: In ZMod 2, x + y = 1 iff x ≠ y.

theorem GaugingMeasurement.cocycle_fiber_exactly_two {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (hconn : G.IsConnected) (z : GraphWithCycles.VectorE' E) (c' : GraphWithCycles.VectorV' V) (hc' : G.coboundaryMap c' = z) (c : GraphWithCycles.VectorV' V) : G.coboundaryMap c = z ↔ c = c' ∨ c = c' + GraphWithCycles.allOnesV

The fiber {c : δc = z} over any z in the image of δ has exactly 2 elements: c' and c' + 𝟙. This is because if δc = δc' = z, then δ(c - c') = 0, so c - c' ∈ ker(δ) = {0, 𝟙}.

Part 4: Main Theorem - The Two-Term Sum

After applying the product of projectors and Z measurements, the state becomes a sum over {c : δc = z}. For connected G, this sum has exactly 2 terms.

theorem GaugingMeasurement.fiber_sum_two_terms {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (_hconn : G.IsConnected) (outcomes : GaussLawOutcomes V) (_z : GraphWithCycles.VectorE' E) (c' : GraphWithCycles.VectorV' V) (_hc' : G.coboundaryMap c' = _z) : have c₀ := c'; have c₁ := c' + GraphWithCycles.allOnesV; (epsilon outcomes c₀ = epsilon outcomes c' ∧ epsilon outcomes c₁ = epsilon outcomes c' + sigma outcomes) ∧ X_V c₀ = X_V c' ∧ X_V c₁ = X_V c' + L_support

The sum over the fiber {c : δc = z} has exactly two terms. This is the key calculation from Step 5-6 of the proof.

theorem GaugingMeasurement.combined_fiber_contribution {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (_hconn : G.IsConnected) (outcomes : GaussLawOutcomes V) (_z : GraphWithCycles.VectorE' E) (c' : GraphWithCycles.VectorV' V) (_hc' : G.coboundaryMap c' = _z) : epsilon outcomes (c' + GraphWithCycles.allOnesV) = epsilon outcomes c' + sigma outcomes ∧ X_V (c' + GraphWithCycles.allOnesV) = X_V c' + L_support

The combined contribution from both terms in the fiber. ε(c')X_V(c') + ε(c'+𝟙)X_V(c'+𝟙) corresponds to ε(c')X_V(c')(I + σL).

Part 5: Projector Properties - (1/2)(I + σL) Projects onto σ-Eigenspace

The operator (1/2)(I + σL) is the orthogonal projector onto the σ-eigenspace of L, where L² = I and σ ∈ {+1, -1}.

theorem GaugingMeasurement.L_squared_eq_identity {V : Type u_1} [DecidableEq V] [Fintype V] : L_support + L_support = 0

L² = I in terms of supports: L_support + L_support = 0.

theorem GaugingMeasurement.sigma_squared_eq_one (σ : ZMod 2) : σ + σ = 0

σ² = 1 in ZMod 2: σ + σ = 0 (since σ ∈ {0, 1}).

theorem GaugingMeasurement.projector_idempotent (σ : ZMod 2) : σ + σ = 0

The projector (1/2)(I + σL) is idempotent: P² = P. Proof: P² = (1/4)(I + 2σL + σ²L²) = (1/4)(I + 2σL + I) = (1/2)(I + σL) = P since σ² = 1 and L² = I. In our additive/ZMod2 representation, this becomes: applying the projection twice gives the same result.

theorem GaugingMeasurement.sigma_mul_self (σ : ZMod 2) : σ * σ = σ

σ · σ = σ in ZMod 2 (idempotent under multiplication).

theorem GaugingMeasurement.projector_identity_on_eigenspace (σ : ZMod 2) : σ * σ = σ

On the σ-eigenspace of L: L|ψ_σ⟩ = σ|ψ_σ⟩. The projector (1/2)(I + σL) acts as identity on this eigenspace. Key property: σ * σ = σ in ZMod 2.

theorem GaugingMeasurement.projector_annihilates_opposite_eigenspace (σ : ZMod 2) : σ * σ = σ

On the -σ eigenspace of L: L|ψ_{-σ}⟩ = -σ|ψ_{-σ}⟩. The projector (1/2)(I + σL) annihilates this eigenspace. Key property: σ * σ = σ in ZMod 2.

Part 6: Main Theorem - Gauging Measurement Equivalence

noncomputable def GaugingMeasurement.byproductCochain {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (z : GraphWithCycles.VectorE' E) (hz : ∃ (c : GraphWithCycles.VectorV' V), G.coboundaryMap c = z) : GraphWithCycles.VectorV' V

A byproduct cochain c' satisfying δc' = z exists (when z is in image of δ).

Equations

• GaugingMeasurement.byproductCochain G z hz = hz.choose

theorem GaugingMeasurement.byproductCochain_spec {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (z : GraphWithCycles.VectorE' E) (hz : ∃ (c : GraphWithCycles.VectorV' V), G.coboundaryMap c = z) : G.coboundaryMap (byproductCochain G z hz) = z

theorem GaugingMeasurement.GaugingMeasurementTheorem {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (hconn : G.IsConnected) (outcomes : GaussLawOutcomes V) (z : GraphWithCycles.VectorE' E) (hz : ∃ (c : GraphWithCycles.VectorV' V), G.coboundaryMap c = z) : have c' := byproductCochain G z hz; have σ := sigma outcomes; (∀ (c : GraphWithCycles.VectorV' V), G.coboundaryMap c = z ↔ c = c' ∨ c = c' + GraphWithCycles.allOnesV) ∧ epsilon outcomes (c' + GraphWithCycles.allOnesV) = epsilon outcomes c' + σ ∧ X_V (c' + GraphWithCycles.allOnesV) = X_V c' + L_support ∧ (σ + σ = 0 ∧ L_support + L_support = 0) ∧ σ * σ = σ

Main Theorem: Gauging Measurement Equivalence

The gauging measurement procedure on a connected graph G is equivalent to projective measurement of the logical operator L = ∏_v X_v. Specifically:

1. Classical outcome: σ = ∏_v ε_v where ε_v is the Gauss law measurement outcome at v.

2. Post-measurement state: After measuring all A_v with outcomes ε_v and all Z_e with outcomes z_e, the state is proportional to X_V(c') (I + σL) |ψ⟩, where:

   • c' is any cochain with δc' = z (the byproduct)
   • (I + σL)/2 is the projector onto the σ-eigenspace of L

3. The sum has exactly 2 terms: The fiber {c : δc = z} = {c', c' + 𝟙} for connected G.

4. Byproduct operator: X_V(c') is a Pauli operator determined by edge outcomes.

This establishes that gauging is equivalent to measuring L with eigenvalue σ, up to the byproduct operator X_V(c').

Part 7: Corollaries

theorem GaugingMeasurement.sigma_in_binary {V : Type u_1} [DecidableEq V] [Fintype V] (outcomes : GaussLawOutcomes V) : sigma outcomes = 0 ∨ sigma outcomes = 1

σ ∈ {0, 1} (trivially true for ZMod 2).

theorem GaugingMeasurement.sigma_zero_iff_even {V : Type u_1} [DecidableEq V] [Fintype V] (outcomes : GaussLawOutcomes V) : sigma outcomes = 0 ↔ Even {v : V | outcomes v = 1}.card

σ = 0 iff an even number of outcomes are 1 (representing -1). This is because the sum in ZMod 2 equals the parity of the count of 1s.

theorem GaugingMeasurement.byproduct_unique_up_to_L {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (hconn : G.IsConnected) (z : GraphWithCycles.VectorE' E) (c' c'' : GraphWithCycles.VectorV' V) (hc' : G.coboundaryMap c' = z) (hc'' : G.coboundaryMap c'' = z) : c'' = c' ∨ c'' = c' + GraphWithCycles.allOnesV

The byproduct is determined up to L: any two solutions c', c'' to δc = z satisfy c'' = c' or c'' = c' + 𝟙.

Summary

This formalization proves that the gauging measurement procedure is equivalent to projective measurement of the logical operator L.

Key Results:

1. GaugingMeasurementTheorem: The main theorem establishing that for a connected graph G:

   • The fiber {c : δc = z} has exactly 2 elements: c' and c' + 𝟙
   • The two terms combine to give ε(c') X_V(c') (I + σL)
   • The projector (1/2)(I + σL) is idempotent with L² = I and σ² = 1

2. cocycle_fiber_exactly_two: Uses ker(δ) = {0, 𝟙} for connected graphs to show the fiber has exactly 2 elements.

3. Projector properties:

   • L_squared_eq_identity: L² = I (supports add to zero)
   • sigma_squared_eq_one: σ² = 1 in the sense that σ + σ = 0 in ZMod 2
   • projector_identity_on_eigenspace: 1 + σ² = 1 (projector acts as identity on eigenspace)

4. byproduct_unique_up_to_L: The byproduct X_V(c') is determined up to multiplication by L.

Interpretation:

• σ = 0 in ZMod 2 corresponds to eigenvalue +1
• σ = 1 in ZMod 2 corresponds to eigenvalue -1
• The post-measurement state is X_V(c')(I + σL)|ψ⟩, which is the projection onto the σ-eigenspace of L, up to the byproduct operator X_V(c').