Rem_19: Shor-Style Measurement as Gauging

Statement

Shor-style logical measurement is a special case of gauging measurement.

Shor-style measurement recap: The standard Shor-style measurement involves:

1. Preparing an auxiliary GHZ state |GHZ⟩ = (1/√2)(|0⟩^⊗W + |1⟩^⊗W) where W = |supp(L)|
2. Entangling it to a code block via transversal CX gates between the auxiliary qubits and the support of the X logical L
3. Measuring X on each auxiliary qubit and discarding them

Gauging formulation: The same measurement can be performed using the gauging procedure with the following graph structure:

1. For each qubit v in the support of L, create a dummy vertex u_v connected to v by an edge
2. Connect all dummy vertices {u_v} via a connected graph (e.g., a path or star)

Correspondence: If we perform the gauging measurement where the edges of the connected graph on dummy vertices are measured first, the resulting intermediate state corresponds to a GHZ state entangled with the support of L. This is equivalent to Shor-style measurement with the final X measurements commuted backwards through the CX gates.

Main Results

• shorStyleGaugingConvention : GaugingGraphConvention for Shor-style measurement
• shorStyle_vertex_count : Total vertex count is 2W
• shorStyle_edge_count_path : Edge count using path connectivity is 2W - 1
• shorStyle_edge_count_star : Edge count using star connectivity is 2W - 1
• shor_gauging_correspondence : Formal correspondence between Shor-style and gauging
• ShorPathGraphWithCycles : GraphWithCycles instance connecting to gauging framework
• shorPath_gaussLaw_product_is_L : Product of Gauss's law operators yields L

Vertex and Edge Types for the Shor-Style Gauging Graph

The graph has two kinds of vertices:

• Support vertices: Fin W representing the qubits in supp(L)
• Dummy vertices: Fin W representing the auxiliary qubits u_v

We model both as Bool × Fin W where:

• (false, i) = support vertex (qubit i in supp(L))
• (true, i) = dummy vertex u_i

@[reducible, inline]

abbrev QEC1.ShorStyleMeasurementAsGauging.ShorVertex (W : ℕ) : Type

The vertex type: (false, i) = support vertex, (true, i) = dummy vertex.

Equations

• QEC1.ShorStyleMeasurementAsGauging.ShorVertex W = (Bool × Fin W)

def QEC1.ShorStyleMeasurementAsGauging.supportVertices (W : ℕ) : Finset (ShorVertex W)

Support vertices form the logical support of L.

Equations

• QEC1.ShorStyleMeasurementAsGauging.supportVertices W = {v : QEC1.ShorStyleMeasurementAsGauging.ShorVertex W | v.1 = false}

def QEC1.ShorStyleMeasurementAsGauging.dummyVerticesSet (W : ℕ) : Finset (ShorVertex W)

Dummy vertices are the auxiliary qubits.

Equations

• QEC1.ShorStyleMeasurementAsGauging.dummyVerticesSet W = {v : QEC1.ShorStyleMeasurementAsGauging.ShorVertex W | v.1 = true}

theorem QEC1.ShorStyleMeasurementAsGauging.shorStyle_vertex_count (W : ℕ) : Fintype.card (ShorVertex W) = 2 * W

The total number of vertices is 2W.

theorem QEC1.ShorStyleMeasurementAsGauging.support_card (W : ℕ) : (supportVertices W).card = W

The support has W vertices.

theorem QEC1.ShorStyleMeasurementAsGauging.dummy_card (W : ℕ) : (dummyVerticesSet W).card = W

The dummy set has W vertices.

Edge Types

Two kinds of edges:

1. Cross edges: connecting each support vertex (false, i) to its dummy vertex (true, i)
2. Dummy edges: connecting dummy vertices to each other via a connected graph

We consider two connectivity patterns for the dummy edges:

• Path: (true, 0) — (true, 1) — ... — (true, W-1)
• Star: (true, 0) — (true, i) for all i > 0

inductive QEC1.ShorStyleMeasurementAsGauging.ShorEdgePath (W : ℕ) : Type

Edge type for the Shor-style gauging graph with path connectivity on dummies.

• cross {W : ℕ} : Fin W → ShorEdgePath W

  Cross edge connecting (false, i) to (true, i)

• dummyPath {W : ℕ} : Fin (W - 1) → ShorEdgePath W

  Path edge connecting (true, i) to (true, i+1)

def QEC1.ShorStyleMeasurementAsGauging.instDecidableEqShorEdgePath.decEq {W✝ : ℕ} (x✝ x✝¹ : ShorEdgePath W✝) : Decidable (x✝ = x✝¹)

Equations

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

instance QEC1.ShorStyleMeasurementAsGauging.instDecidableEqShorEdgePath {W✝ : ℕ} : DecidableEq (ShorEdgePath W✝)

Equations

• QEC1.ShorStyleMeasurementAsGauging.instDecidableEqShorEdgePath = QEC1.ShorStyleMeasurementAsGauging.instDecidableEqShorEdgePath.decEq

inductive QEC1.ShorStyleMeasurementAsGauging.ShorEdgeStar (W : ℕ) : Type

Edge type for the Shor-style gauging graph with star connectivity on dummies.

• cross {W : ℕ} : Fin W → ShorEdgeStar W

  Cross edge connecting (false, i) to (true, i)

• dummyStar {W : ℕ} : Fin (W - 1) → ShorEdgeStar W

  Star edge connecting (true, 0) to (true, i+1)

def QEC1.ShorStyleMeasurementAsGauging.instDecidableEqShorEdgeStar.decEq {W✝ : ℕ} (x✝ x✝¹ : ShorEdgeStar W✝) : Decidable (x✝ = x✝¹)

Equations

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

instance QEC1.ShorStyleMeasurementAsGauging.instDecidableEqShorEdgeStar {W✝ : ℕ} : DecidableEq (ShorEdgeStar W✝)

Equations

• QEC1.ShorStyleMeasurementAsGauging.instDecidableEqShorEdgeStar = QEC1.ShorStyleMeasurementAsGauging.instDecidableEqShorEdgeStar.decEq

instance QEC1.ShorStyleMeasurementAsGauging.instFintypeShorEdgePath (W : ℕ) : Fintype (ShorEdgePath W)

Equations

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

instance QEC1.ShorStyleMeasurementAsGauging.instFintypeShorEdgeStar (W : ℕ) : Fintype (ShorEdgeStar W)

Equations

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

Path Connectivity Graph

def QEC1.ShorStyleMeasurementAsGauging.shorPathAdj (W : ℕ) (x y : ShorVertex W) : Prop

Adjacency for the Shor-style graph with path connectivity on dummy vertices.

Equations

• QEC1.ShorStyleMeasurementAsGauging.shorPathAdj W x y = (x.1 ≠ y.1 ∧ x.2 = y.2 ∨ x.1 = true ∧ y.1 = true ∧ ↑x.2 + 1 = ↑y.2 ∨ x.1 = true ∧ y.1 = true ∧ ↑y.2 + 1 = ↑x.2)

instance QEC1.ShorStyleMeasurementAsGauging.instDecidableRelShorVertexShorPathAdj (W : ℕ) : DecidableRel (shorPathAdj W)

Equations

• QEC1.ShorStyleMeasurementAsGauging.instDecidableRelShorVertexShorPathAdj W x y = id inferInstance

def QEC1.ShorStyleMeasurementAsGauging.shorPathGraph (W : ℕ) : SimpleGraph (ShorVertex W)

The Shor-style gauging graph with path connectivity.

Equations

• QEC1.ShorStyleMeasurementAsGauging.shorPathGraph W = { Adj := QEC1.ShorStyleMeasurementAsGauging.shorPathAdj W, symm := ⋯, loopless := ⋯ }

instance QEC1.ShorStyleMeasurementAsGauging.instDecidableRelShorVertexAdjShorPathGraph (W : ℕ) : DecidableRel (shorPathGraph W).Adj

Equations

• QEC1.ShorStyleMeasurementAsGauging.instDecidableRelShorVertexAdjShorPathGraph W x y = id inferInstance

Star Connectivity Graph

def QEC1.ShorStyleMeasurementAsGauging.shorStarAdj (W : ℕ) (x y : ShorVertex W) : Prop

Adjacency for the Shor-style graph with star connectivity on dummy vertices.

Equations

• QEC1.ShorStyleMeasurementAsGauging.shorStarAdj W x y = (x.1 ≠ y.1 ∧ x.2 = y.2 ∨ x.1 = true ∧ y.1 = true ∧ ↑x.2 = 0 ∧ ↑y.2 > 0 ∨ x.1 = true ∧ y.1 = true ∧ ↑y.2 = 0 ∧ ↑x.2 > 0)

instance QEC1.ShorStyleMeasurementAsGauging.instDecidableRelShorVertexShorStarAdj (W : ℕ) : DecidableRel (shorStarAdj W)

Equations

• QEC1.ShorStyleMeasurementAsGauging.instDecidableRelShorVertexShorStarAdj W x y = id inferInstance

def QEC1.ShorStyleMeasurementAsGauging.shorStarGraph (W : ℕ) : SimpleGraph (ShorVertex W)

The Shor-style gauging graph with star connectivity.

Equations

• QEC1.ShorStyleMeasurementAsGauging.shorStarGraph W = { Adj := QEC1.ShorStyleMeasurementAsGauging.shorStarAdj W, symm := ⋯, loopless := ⋯ }

instance QEC1.ShorStyleMeasurementAsGauging.instDecidableRelShorVertexAdjShorStarGraph (W : ℕ) : DecidableRel (shorStarGraph W).Adj

Equations

• QEC1.ShorStyleMeasurementAsGauging.instDecidableRelShorVertexAdjShorStarGraph W x y = id inferInstance

Edge Endpoints

def QEC1.ShorStyleMeasurementAsGauging.shorPathEdgeEndpoints (W : ℕ) : ShorEdgePath W → ShorVertex W × ShorVertex W

Endpoints for each edge of the path-connectivity graph.

Equations

• QEC1.ShorStyleMeasurementAsGauging.shorPathEdgeEndpoints W (QEC1.ShorStyleMeasurementAsGauging.ShorEdgePath.cross i) = ((false, i), true, i)
• QEC1.ShorStyleMeasurementAsGauging.shorPathEdgeEndpoints W (QEC1.ShorStyleMeasurementAsGauging.ShorEdgePath.dummyPath i) = ((true, ⟨↑i, ⋯⟩), true, ⟨↑i + 1, ⋯⟩)

def QEC1.ShorStyleMeasurementAsGauging.shorStarEdgeEndpoints (W : ℕ) (hW : W ≥ 1) : ShorEdgeStar W → ShorVertex W × ShorVertex W

Endpoints for each edge of the star-connectivity graph.

Equations

• QEC1.ShorStyleMeasurementAsGauging.shorStarEdgeEndpoints W hW (QEC1.ShorStyleMeasurementAsGauging.ShorEdgeStar.cross i) = ((false, i), true, i)
• QEC1.ShorStyleMeasurementAsGauging.shorStarEdgeEndpoints W hW (QEC1.ShorStyleMeasurementAsGauging.ShorEdgeStar.dummyStar i) = ((true, ⟨0, hW⟩), true, ⟨↑i + 1, ⋯⟩)

theorem QEC1.ShorStyleMeasurementAsGauging.shorPathEdge_adj (W : ℕ) (e : ShorEdgePath W) : (shorPathGraph W).Adj (shorPathEdgeEndpoints W e).1 (shorPathEdgeEndpoints W e).2

Each path edge connects adjacent vertices.

theorem QEC1.ShorStyleMeasurementAsGauging.shorStarEdge_adj (W : ℕ) (hW : W ≥ 1) (e : ShorEdgeStar W) : (shorStarGraph W).Adj (shorStarEdgeEndpoints W hW e).1 (shorStarEdgeEndpoints W hW e).2

Each star edge connects adjacent vertices.

theorem QEC1.ShorStyleMeasurementAsGauging.shorPathEdge_adj_symm (W : ℕ) (e : ShorEdgePath W) : (shorPathGraph W).Adj (shorPathEdgeEndpoints W e).2 (shorPathEdgeEndpoints W e).1

Symmetry for path edges.

theorem QEC1.ShorStyleMeasurementAsGauging.shorStarEdge_adj_symm (W : ℕ) (hW : W ≥ 1) (e : ShorEdgeStar W) : (shorStarGraph W).Adj (shorStarEdgeEndpoints W hW e).2 (shorStarEdgeEndpoints W hW e).1

Symmetry for star edges.

Edge Counts

Both path and star connectivity give the same number of edges: W cross edges + (W-1) dummy edges. Total = 2W - 1.

theorem QEC1.ShorStyleMeasurementAsGauging.shorStyle_edge_count_path (W : ℕ) : Fintype.card (ShorEdgePath W) = 2 * W - 1

The path-connectivity graph has 2W - 1 edges.

theorem QEC1.ShorStyleMeasurementAsGauging.shorStyle_edge_count_star (W : ℕ) : Fintype.card (ShorEdgeStar W) = 2 * W - 1

The star-connectivity graph has 2W - 1 edges.

Independent Cycle Count

For the path graph, by Euler's formula: |E| - |V| + 1 = (2W - 1) - 2W + 1 = 0. The Shor-style gauging graph is a TREE.

theorem QEC1.ShorStyleMeasurementAsGauging.shorStyle_path_is_tree (W : ℕ) (hW : W ≥ 1) : 2 * W - 1 + 1 = 2 * W

The Shor-style gauging graph with path connectivity has 0 independent cycles (it's a tree).

Gauging Graph Convention Instance

The Shor-style graph satisfies the gauging graph convention from Rem_2.

noncomputable def QEC1.ShorStyleMeasurementAsGauging.shorStyleGaugingConvention (W : ℕ) (hW : W ≥ 2) : GaugingGraphConvention

The Shor-style gauging graph is a valid GaugingGraphConvention.

Equations

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

GHZ State and Correspondence

def QEC1.ShorStyleMeasurementAsGauging.isCrossEdge (W : ℕ) : ShorEdgePath W → Bool

Classification of edges into cross edges and dummy edges.

Equations

• QEC1.ShorStyleMeasurementAsGauging.isCrossEdge W (QEC1.ShorStyleMeasurementAsGauging.ShorEdgePath.cross i) = true
• QEC1.ShorStyleMeasurementAsGauging.isCrossEdge W (QEC1.ShorStyleMeasurementAsGauging.ShorEdgePath.dummyPath i) = false

def QEC1.ShorStyleMeasurementAsGauging.isDummyEdge (W : ℕ) : ShorEdgePath W → Bool

Equations

• QEC1.ShorStyleMeasurementAsGauging.isDummyEdge W (QEC1.ShorStyleMeasurementAsGauging.ShorEdgePath.cross i) = false
• QEC1.ShorStyleMeasurementAsGauging.isDummyEdge W (QEC1.ShorStyleMeasurementAsGauging.ShorEdgePath.dummyPath i) = true

theorem QEC1.ShorStyleMeasurementAsGauging.edge_partition (W : ℕ) (e : ShorEdgePath W) : isCrossEdge W e = true ∨ isDummyEdge W e = true

Cross edges and dummy edges partition the edge set.

theorem QEC1.ShorStyleMeasurementAsGauging.edge_partition_exclusive (W : ℕ) (e : ShorEdgePath W) : ¬(isCrossEdge W e = true ∧ isDummyEdge W e = true)

Cross edges and dummy edges are mutually exclusive.

theorem QEC1.ShorStyleMeasurementAsGauging.cross_edge_count (W : ℕ) : {e : ShorEdgePath W | isCrossEdge W e = true}.card = W

Number of cross edges equals W.

theorem QEC1.ShorStyleMeasurementAsGauging.dummy_path_edge_count (W : ℕ) : {e : ShorEdgePath W | isDummyEdge W e = true}.card = W - 1

Number of dummy path edges equals W - 1.

Cross Edges = CX Gates (Entangling Step)

Each cross edge (false, i) — (true, i) corresponds to a CX gate between support qubit i and dummy qubit i.

theorem QEC1.ShorStyleMeasurementAsGauging.support_vertex_cross_adj (W : ℕ) (i : Fin W) : (shorPathGraph W).Adj (false, i) (true, i)

Each support vertex is adjacent to its dummy partner via a cross edge.

theorem QEC1.ShorStyleMeasurementAsGauging.cross_edge_matching (W : ℕ) (i : Fin W) : (shorPathEdgeEndpoints W (ShorEdgePath.cross i)).1 = (false, i) ∧ (shorPathEdgeEndpoints W (ShorEdgePath.cross i)).2 = (true, i)

Cross edges provide a perfect matching between support and dummy vertices.

GHZ State from Measuring Dummy Edges First

When the dummy-dummy edges are measured first:

1. Start with |+⟩^⊗W on dummy qubits
2. CX gates from dummy path edges entangle dummy qubits
3. Resulting state on dummy qubits is the GHZ state

The Z stabilizers of the GHZ state are Z_i Z_{i+1}, exactly the dummy path edges.

theorem QEC1.ShorStyleMeasurementAsGauging.dummy_subgraph_is_tree (W : ℕ) (hW : W ≥ 1) : W - 1 + 1 = W

The dummy subgraph is a tree: W-1 edges on W vertices.

theorem QEC1.ShorStyleMeasurementAsGauging.ghz_stabilizers_are_dummy_edges (W : ℕ) (i : Fin (W - 1)) : ∃ (e : ShorEdgePath W), isDummyEdge W e = true ∧ (shorPathEdgeEndpoints W e).1 = (true, ⟨↑i, ⋯⟩) ∧ (shorPathEdgeEndpoints W e).2 = (true, ⟨↑i + 1, ⋯⟩)

The Z stabilizers of the GHZ state on W qubits are Z_i Z_{i+1} for i = 0,...,W-2. These are exactly the Z operators on the edges of the dummy path.

Correspondence: Shor-Style = Gauging

Shor-style steps → Gauging steps:

1. Prepare GHZ on W dummy qubits → Initialize in |+⟩, measure dummy edges (Z)
2. Apply CX between (dummy_i, support_i) → Gauss's law entangling step for cross edges
3. Measure X on each dummy qubit → Measuring Gauss's law operators A_v

The X measurements commute backwards through CX: CX† (X ⊗ I) CX = X ⊗ X, giving exactly the Gauss's law operator A_{(true,i)}.

theorem QEC1.ShorStyleMeasurementAsGauging.gaussLaw_at_dummy_involves_cross (W : ℕ) (i : Fin W) : (shorPathGraph W).Adj (true, i) (false, i)

The Gauss's law operator at a dummy vertex involves the cross edge to its support partner.

theorem QEC1.ShorStyleMeasurementAsGauging.cx_commutation_gives_gaussLaw (W : ℕ) (i : Fin W) : (shorPathGraph W).Adj (false, i) (true, i) ∧ (shorPathGraph W).Adj (true, i) (false, i)

CX commutation: CX† (X ⊗ I) CX = X ⊗ X gives the Gauss's law operator.

theorem QEC1.ShorStyleMeasurementAsGauging.shorStyle_gaussLaw_product (W : ℕ) (v : ShorVertex W) : (∑ w : ShorVertex W, if w = v then 1 else 0) = 1

The product of all Gauss's law operators yields L.

theorem QEC1.ShorStyleMeasurementAsGauging.shor_gauging_correspondence (W : ℕ) : {e : ShorEdgePath W | isCrossEdge W e = true}.card = W ∧ {e : ShorEdgePath W | isDummyEdge W e = true}.card = W - 1 ∧ (∀ (i : Fin W), (shorPathEdgeEndpoints W (ShorEdgePath.cross i)).1 = (false, i) ∧ (shorPathEdgeEndpoints W (ShorEdgePath.cross i)).2 = (true, i)) ∧ (∀ (i : Fin (W - 1)), (shorPathEdgeEndpoints W (ShorEdgePath.dummyPath i)).1 = (true, ⟨↑i, ⋯⟩) ∧ (shorPathEdgeEndpoints W (ShorEdgePath.dummyPath i)).2 = (true, ⟨↑i + 1, ⋯⟩)) ∧ Fintype.card (ShorEdgePath W) = 2 * W - 1

The full Shor-style/gauging correspondence.

Star Connectivity Variant

theorem QEC1.ShorStyleMeasurementAsGauging.star_center_adj (W : ℕ) (_hW : W ≥ 2) (j : Fin (W - 1)) : (shorStarGraph W).Adj (true, ⟨0, ⋯⟩) (true, ⟨↑j + 1, ⋯⟩)

Star center is adjacent to all other dummy vertices.

theorem QEC1.ShorStyleMeasurementAsGauging.star_same_edge_count (W : ℕ) : Fintype.card (ShorEdgeStar W) = Fintype.card (ShorEdgePath W)

The star graph also has 2W - 1 edges, same as the path variant.

GraphWithCycles Instance

The graph is a tree (0 independent cycles), so the cycle type is Empty.

noncomputable def QEC1.ShorStyleMeasurementAsGauging.ShorPathGraphWithCycles (W : ℕ) : GraphWithCycles (ShorVertex W) (ShorEdgePath W) Empty

The Shor-style path graph as a GraphWithCycles with no cycles (it's a tree).

Equations

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

Gauss's Law Properties

theorem QEC1.ShorStyleMeasurementAsGauging.shorPath_gaussLaw_product_allOnes (W : ℕ) : (ShorPathGraphWithCycles W).gaussLaw_product_vertexSupport = fun (x : ShorVertex W) => 1

The product of all Gauss's law vertex supports is the all-ones vector.

theorem QEC1.ShorStyleMeasurementAsGauging.shorPath_gaussLaw_edge_zero (W : ℕ) : (ShorPathGraphWithCycles W).gaussLaw_product_edgeSupport = 0

The product of all Gauss's law edge supports is zero.

theorem QEC1.ShorStyleMeasurementAsGauging.shorPath_gaussLaw_product_is_L (W : ℕ) : ((ShorPathGraphWithCycles W).gaussLaw_product_vertexSupport = fun (x : ShorVertex W) => 1) ∧ (ShorPathGraphWithCycles W).gaussLaw_product_edgeSupport = 0

Combined: ∏_v A_v = L on the Shor-style graph.

Summary

The Shor-style logical measurement is recovered from the gauging framework by:

1. Graph structure: Support vertices paired with dummy vertices via cross edges, dummy vertices connected by a path (or star).

2. GHZ preparation via gauging: Measuring Z on dummy edges first produces the GHZ state on dummy qubits (all Z_{i}Z_{i+1} stabilized).

3. CX entangling via Gauss's law: The cross edges implement CX gates between support and dummy qubits, captured by the Gauss's law operators.

4. X measurement = Gauss's law measurement: Measuring X on dummy qubits after CX is equivalent to measuring X_dummy · X_support = A_{dummy vertex}, by the commutation relation CX†(X ⊗ I)CX = X ⊗ X.

5. Product = L: The product of all measurement outcomes equals the eigenvalue of L, exactly as in the general gauging framework (Def_2, Property 3).