Definition 5: Gauging Measurement Algorithm

Statement

The gauging measurement procedure measures a logical operator L = ∏_{v ∈ V} X_v by introducing auxiliary edge qubits, measuring Gauss's law operators A_v and edge qubits Z_e, and applying byproduct corrections.

We formalize the classical data and processing of the algorithm:

• Measurement outcomes (ε_v for Gauss's law, ω_e for edge qubits)
• The sign σ = ∏_v ε_v that gives the measurement result
• The byproduct correction rule based on walk parities
• Additivity of walk parity under concatenation and reversal
• The Gauss's law operators and edge Z operators being measured
• Commutativity of all measured operators

We use ZMod 2 for measurement outcomes: 0 ↔ +1, 1 ↔ -1. Products of ±1 values correspond to sums in ZMod 2.

Main Results

• GaugingInput : the input data for the gauging procedure
• GaugingOutcomes : the measurement outcomes (ε_v, ω_e)
• measurementSign : the sign σ = ∑_v ε_v (in ZMod 2)
• walkParity : the parity of ω along a walk
• byproductCorrectionAt : the correction at vertex v given a specific walk from v₀
• gaugingAlgorithm : the full classical output of the algorithm
• walkParity_append : additivity under concatenation
• walkParity_reverse : invariance under reversal
• walkParity_well_defined : two walks give the same parity when closed walks have zero parity
• gaussLaw_product_gives_logical : ∏_v A_v = L
• gaussLaw_measured_commute : Gauss measurements commute
• edgeZ_measured_commute : edge measurements commute

Corollaries

• Sign characterization lemmas
• Walk parity algebra
• Measurement operator identifications

Input Data

structure GaugingMeasurement.GaugingInput {V : Type u_1} (G : SimpleGraph V) : Type u_1

The input data for the gauging measurement procedure.

• A connected graph G = (V, E) with V = support of the logical operator L = ∏_v X_v
• A distinguished base vertex v₀ ∈ V for byproduct correction

• baseVertex : V

  The base vertex v₀ ∈ V

• connected : G.Connected

  The graph G is connected

Measurement Outcomes

structure GaugingMeasurement.GaugingOutcomes {V : Type u_1} (G : SimpleGraph V) : Type u_1

The measurement outcomes from the gauging procedure. We use ZMod 2 to represent ±1 outcomes: 0 ↔ +1, 1 ↔ -1. Products of ±1 correspond to sums in ZMod 2.

• gaussOutcome v : the outcome ε_v of measuring Gauss's law operator A_v
• edgeOutcome e : the outcome ω_e of measuring Z_e

• gaussOutcome : V → ZMod 2

  Gauss's law measurement outcomes: ε_v for each v ∈ V

• edgeOutcome : ↑G.edgeSet → ZMod 2

  Edge Z-measurement outcomes: ω_e for each e ∈ E

Sign Computation

def GaugingMeasurement.measurementSign {V : Type u_1} [Fintype V] (G : SimpleGraph V) (outcomes : GaugingOutcomes G) : ZMod 2

The measurement sign σ = ∏_v ε_v, encoded as ∑_v ε_v in ZMod 2. This is the measurement result of the logical L = ∏_v X_v: σ = 0 (in ZMod 2) means the +1 eigenvalue, σ = 1 means -1.

Equations

• GaugingMeasurement.measurementSign G outcomes = ∑ v : V, outcomes.gaussOutcome v

@[simp]

theorem GaugingMeasurement.measurementSign_def {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (outcomes : GaugingOutcomes G) : measurementSign G outcomes = ∑ v : V, outcomes.gaussOutcome v

Walk Parity

noncomputable def GaugingMeasurement.walkParity {V : Type u_1} (G : SimpleGraph V) (ω : ↑G.edgeSet → ZMod 2) {u v : V} (w : G.Walk u v) : ZMod 2

Given edge measurement outcomes ω and a walk in G, compute the parity of ω along the walk: the ZMod 2 sum of ω(e) over all edges e traversed. This is ∑_{d ∈ walk.darts} ω(d.edge) in ZMod 2.

An edge traversed by dart d has d.edge ∈ G.edgeSet (from d.adj).

Equations

• GaugingMeasurement.walkParity G ω w = (List.map (fun (d : G.Dart) => ω ⟨d.edge, ⋯⟩) w.darts).sum

@[simp]

theorem GaugingMeasurement.walkParity_nil {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (ω : ↑G.edgeSet → ZMod 2) (v : V) : walkParity G ω SimpleGraph.Walk.nil = 0

theorem GaugingMeasurement.walkParity_cons {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (ω : ↑G.edgeSet → ZMod 2) {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : walkParity G ω (SimpleGraph.Walk.cons h p) = ω ⟨s(u, v), ⋯⟩ + walkParity G ω p

Walk Parity Algebra

theorem GaugingMeasurement.walkParity_append {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (ω : ↑G.edgeSet → ZMod 2) {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : walkParity G ω (p.append q) = walkParity G ω p + walkParity G ω q

Walk parity is additive under concatenation.

theorem GaugingMeasurement.walkParity_reverse {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (ω : ↑G.edgeSet → ZMod 2) {u v : V} (p : G.Walk u v) : walkParity G ω p.reverse = walkParity G ω p

Walk parity is invariant under reversal (since we work in ZMod 2, and reversing traverses the same edges as Sym2 elements).

theorem GaugingMeasurement.walkParity_single {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (ω : ↑G.edgeSet → ZMod 2) {u v : V} (h : G.Adj u v) : walkParity G ω (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil) = ω ⟨s(u, v), ⋯⟩

Walk parity of a single-edge walk.

theorem GaugingMeasurement.walkParity_diff_eq_closed {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (ω : ↑G.edgeSet → ZMod 2) {u v : V} (p q : G.Walk u v) : walkParity G ω p + walkParity G ω q = walkParity G ω (p.append q.reverse)

The difference of walk parities along two paths from u to v equals the parity of the closed walk formed by going along p then back along q.

theorem GaugingMeasurement.walkParity_well_defined {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (ω : ↑G.edgeSet → ZMod 2) (hclosed : ∀ (v : V) (c : G.Walk v v), walkParity G ω c = 0) {u v : V} (p q : G.Walk u v) : walkParity G ω p = walkParity G ω q

If all closed walks have zero parity, then the walk parity from u to v is independent of the choice of walk.

Byproduct Correction

noncomputable def GaugingMeasurement.byproductCorrectionAt {V : Type u_1} (G : SimpleGraph V) (ω : ↑G.edgeSet → ZMod 2) {v₀ v : V} (γ : G.Walk v₀ v) : ZMod 2

The byproduct correction at vertex v, given a specific walk from v₀ to v. This is the parity of edge outcomes along the walk: c(v) = ∑_{e ∈ γ} ω_e (in ZMod 2).

c(v) = 1 means "apply X_v" (corresponding to ∏_{e ∈ γ} ω_e = -1 in ±1 notation).

Equations

• GaugingMeasurement.byproductCorrectionAt G ω γ = GaugingMeasurement.walkParity G ω γ

@[simp]

theorem GaugingMeasurement.byproductCorrectionAt_self {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (ω : ↑G.edgeSet → ZMod 2) (v₀ : V) : byproductCorrectionAt G ω SimpleGraph.Walk.nil = 0

The byproduct correction at the base vertex using the trivial walk is 0.

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

The byproduct correction is well-defined (independent of walk choice) when all closed walks have zero parity.

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

The byproduct correction Pauli operator for a given walk assignment: for each vertex v, apply X_v iff c(v) = 1.

Equations

• GaugingMeasurement.byproductCorrectionOp G walks ω = { xVec := fun (v : V) => GaugingMeasurement.byproductCorrectionAt G ω (walks v), zVec := 0 }

theorem GaugingMeasurement.byproductCorrectionOp_pure_X {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) : (byproductCorrectionOp G walks ω).zVec = 0

The byproduct correction operator is pure X-type.

theorem GaugingMeasurement.byproductCorrectionOp_mul_self {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) : byproductCorrectionOp G walks ω * byproductCorrectionOp G walks ω = 1

The byproduct correction operator is self-inverse (in the Pauli group).

The Gauging Measurement Algorithm

structure GaugingMeasurement.GaugingResult (V : Type u_2) : Type u_2

The classical output of the gauging measurement algorithm.

• sign : ZMod 2

  The measurement sign: 0 ↔ +1 eigenvalue of L, 1 ↔ -1 eigenvalue

• correction : V → ZMod 2

  The byproduct correction vector: c(v) = 1 means apply X_v

noncomputable def GaugingMeasurement.gaugingAlgorithm {V : Type u_1} [Fintype V] (G : SimpleGraph V) (input : GaugingInput G) (outcomes : GaugingOutcomes G) (walks : (v : V) → G.Walk input.baseVertex v) : GaugingResult V

The gauging measurement algorithm: given input data, measurement outcomes, and a choice of walks from v₀ to each vertex, computes the classical output.

• sign = ∑_v ε_v (the product of all Gauss outcomes in ZMod 2)
• correction(v) = walkParity(γ_v, ω) (the parity of edge outcomes along the walk)

Equations

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

@[simp]

theorem GaugingMeasurement.gaugingAlgorithm_sign {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (input : GaugingInput G) (outcomes : GaugingOutcomes G) (walks : (v : V) → G.Walk input.baseVertex v) : (gaugingAlgorithm G input outcomes walks).sign = ∑ v : V, outcomes.gaussOutcome v

The sign is the sum of all Gauss's law measurement outcomes.

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

Two different walk choices produce the same correction vector when all closed walks have zero parity.

Sign Characterization

def GaugingMeasurement.signIsPlus {V : Type u_1} [Fintype V] (G : SimpleGraph V) (outcomes : GaugingOutcomes G) : Prop

σ = 0 (mod 2) means the +1 eigenvalue of L was measured.

Equations

• GaugingMeasurement.signIsPlus G outcomes = (GaugingMeasurement.measurementSign G outcomes = 0)

def GaugingMeasurement.signIsMinus {V : Type u_1} [Fintype V] (G : SimpleGraph V) (outcomes : GaugingOutcomes G) : Prop

σ = 1 (mod 2) means the -1 eigenvalue of L was measured.

Equations

• GaugingMeasurement.signIsMinus G outcomes = (GaugingMeasurement.measurementSign G outcomes = 1)

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

The sign is always 0 or 1 in ZMod 2.

Measured Operators

@[reducible, inline]

abbrev GaugingMeasurement.gaussLawOperatorMeasured {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (v : V) : PauliOp (GaussFlux.ExtQubit G)

The Gauss's law operator measured at vertex v in step 3: A_v = X_v ∏_{e ∋ v} X_e on the extended qubit system V ⊕ E.

Equations

• GaugingMeasurement.gaussLawOperatorMeasured G v = GaussFlux.gaussLawOp G v

@[reducible, inline]

abbrev GaugingMeasurement.edgeZOperatorMeasured {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (e : ↑G.edgeSet) : PauliOp (GaussFlux.ExtQubit G)

The edge Z operator measured at edge e in step 4: Z_e on V ⊕ E.

Equations

• GaugingMeasurement.edgeZOperatorMeasured G e = PauliOp.pauliZ (Sum.inr e)

Commutativity of Measured Operators

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

All Gauss's law operators commute: they can be measured in any order in step 3.

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

All edge Z operators commute: they can be measured in any order in step 4.

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

The product of all Gauss's law operators equals the logical L = ∏_v X_v. This is why σ = ∏_v ε_v gives the measurement result of L.

Edge Z Operators are Pure Z-Type

@[simp]

theorem GaugingMeasurement.edgeZOperatorMeasured_xVec {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (e : ↑G.edgeSet) : (edgeZOperatorMeasured G e).xVec = 0

The edge Z operator Z_e is pure Z-type: no X-support.

@[simp]

theorem GaugingMeasurement.gaussLawOperatorMeasured_zVec {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : (gaussLawOperatorMeasured G v).zVec = 0

The Gauss's law operator A_v is pure X-type: no Z-support.

Self-Inverse Property of Measured Operators

theorem GaugingMeasurement.gaussLawOperatorMeasured_mul_self {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : gaussLawOperatorMeasured G v * gaussLawOperatorMeasured G v = 1

Each Gauss's law operator is self-inverse: A_v * A_v = 1.

theorem GaugingMeasurement.edgeZOperatorMeasured_mul_self {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (e : ↑G.edgeSet) : edgeZOperatorMeasured G e * edgeZOperatorMeasured G e = 1

Each edge Z operator is self-inverse: Z_e * Z_e = 1.