Remark 24: Shor-Style Measurement as Gauging #
Statement #
The gauging measurement procedure (Def_5) recovers Shor-style logical measurement as a special case. Let L be a Pauli logical operator with weight W = |supp(L)|.
Shor-style measurement uses an auxiliary GHZ state on W qubits, transversal CX gates, and X measurements on the auxiliary qubits.
Gauging measurement viewpoint: Choose a graph G with vertex set supp(L) ∪ {d_1, ..., d_W} where:
- W dummy vertices d_i (one per qubit in supp(L))
- A connected subgraph on the dummy vertices
- Each d_i connected by a single edge to the corresponding qubit i
After measuring the edges of the dummy subgraph first (ungauging step of Def_5), the remaining state on dummy qubits is equivalent to a GHZ state entangled with supp(L), recovering Shor-style measurement.
Main Results #
ShorVertex: the vertex type supp(L) ⊕ D (support qubits + dummy qubits)shorGraphAdj: adjacency relation for the Shor-style graphShorGraph: the Shor-style gauging graphshorGraph_connected: the graph is connected (when dummy subgraph is connected)shorGraph_card: the graph has 2W verticesshor_gauss_product_eq_logical: ∏_v A_v = L'shor_pairing_edge: d_i is adjacent to i in the Shor graphshor_style_structural_correspondence: structural summaryshor_dummy_degree_eq: deg(d_i) in ShorGraph = 1 + deg(d_i) in Gdummyshor_max_degree_bound: max degree in ShorGraph ≤ max_degree(Gdummy) + 1shor_edge_count_via_handshaking: 2|E| = W + (W + Σ deg_Gdummy(i))
Shor-style graph construction #
The vertex type is Q ⊕ Q where Q = Fin W represents the support of L. The first copy (Sum.inl i) represents the original support qubits. The second copy (Sum.inr i) represents the dummy vertices d_i.
The edge set consists of:
- Pairing edges: (Sum.inl i, Sum.inr i) connecting each support qubit to its dummy
- Dummy subgraph edges: edges among dummy vertices forming a connected subgraph
The vertex type for the Shor-style gauging graph: support qubits ⊕ dummy qubits. Both are indexed by Fin W, so the total vertex count is 2W.
Equations
- ShorStyleMeasurement.ShorVertex W = (Fin W ⊕ Fin W)
Instances For
The adjacency relation for the Shor-style gauging graph. Two vertices are adjacent if:
- A pairing edge: (inl i, inr i) connecting support qubit i to dummy d_i
- A dummy subgraph edge: (inr i, inr j) where i ~ j in Gdummy
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ShorStyleMeasurement.shorGraphAdj_decidable W Gdummy p q = id inferInstance
The Shor-style gauging graph on 2W vertices. Edges: W pairing edges {(inl i, inr i)} plus the dummy subgraph.
Equations
- ShorStyleMeasurement.ShorGraph W Gdummy = { Adj := ShorStyleMeasurement.shorGraphAdj W Gdummy, symm := ⋯, loopless := ⋯ }
Instances For
Equations
The Shor graph has 2W vertices.
Each pairing edge connects support qubit i to its dummy d_i.
Dummy subgraph edges are edges of the Shor graph.
The embedding of the dummy subgraph into the Shor graph via Sum.inr.
Equations
- ShorStyleMeasurement.shorDummyHom W Gdummy = { toFun := Sum.inr, map_rel' := ⋯ }
Instances For
The Shor graph is connected when the dummy subgraph is connected and W ≥ 1.
Each dummy vertex d_i has degree ≥ 1 in the Shor graph (the pairing edge to i).
Each support vertex has degree ≥ 1 in the Shor graph (the pairing edge to d_i).
The edge set trichotomy: every edge of the Shor graph is either a pairing edge or a dummy subgraph edge.
Extended logical operator on the Shor graph #
The vertex set of the Shor graph is (Fin W) ⊕ (Fin W), where the first copy represents supp(L) and the second copy represents the dummy vertices. The logical operator being measured is L' = ∏_v X_v over ALL vertices (both support and dummy), exactly as in Rem_10's extendedLogicalOp.
The logical operator L' on the Shor graph vertex set: L' = ∏_{v ∈ V ⊕ D} X_v. This is the extended logical from Rem_10 with V = D = Fin W.
Equations
- ShorStyleMeasurement.shorLogicalOp W = { xVec := fun (x : ShorStyleMeasurement.ShorVertex W) => 1, zVec := 0 }
Instances For
L' is pure X-type: no Z-support.
L' is self-inverse: L' · L' = 1.
L' has X-support on all vertices.
L' has no Z-support on any vertex.
The weight of L' is 2W.
The support-restricted logical: L on the original support qubits only. Acts as X on all Sum.inl qubits and I on Sum.inr qubits.
Equations
- ShorStyleMeasurement.shorOriginalLogical W = { xVec := fun (q : ShorStyleMeasurement.ShorVertex W) => match q with | Sum.inl val => 1 | Sum.inr val => 0, zVec := 0 }
Instances For
The dummy product: ∏_{d ∈ D} X_d on dummy qubits only.
Equations
- ShorStyleMeasurement.shorDummyProduct W = { xVec := fun (q : ShorStyleMeasurement.ShorVertex W) => match q with | Sum.inl val => 0 | Sum.inr val => 1, zVec := 0 }
Instances For
The factorization L' = L · ∏_d X_d. The full logical is the product of the support-restricted logical and dummy X product.
L restricted to support qubits is pure X-type.
Dummy product is pure X-type.
L and the dummy product commute (both pure X-type).
L restricted to support is self-inverse.
Dummy product is self-inverse.
Measurement sign and dummy vertices #
When dummy vertices are initialized in |+⟩ (eigenstate of X with eigenvalue +1), measuring A_v on a dummy vertex always gives outcome +1 (= 0 in ZMod 2). Therefore σ(L') = σ(L): the measurement sign of the extended logical equals that of the original logical. This is the same result as Rem_10.
Gauging structure on the Shor graph #
The gauging measurement on the Shor graph has the following structure:
- The Gauss's law operators A_v (Def_2) on V ⊕ E are pure X-type
- Their product equals L' = ∏_v X_v (the logical being measured)
- The CX circuit (Rem_9) transforms A_v to X_v
- Measuring X on the dummy vertices corresponds to the Shor-style X measurements
The key observation: after measuring the dummy subgraph edges in the ungauging step, the remaining state on dummy qubits is a GHZ-like state entangled with the support qubits via the pairing edges {d_i, i}. This is exactly the Shor-style structure.
The Gauss's law operator A_v on the Shor graph is pure X-type.
The product of all Gauss operators on the Shor graph equals the logical L'. This is the structural content of Def_2's gaussLaw_product applied to the Shor graph.
The logical operator on the Shor graph's extended system (V ⊕ E) acts as X on all vertex qubits and I on edge qubits. On vertex qubits, this is L' = ∏_{v ∈ V ⊕ D} X_v.
Circuit correspondence #
The CX entangling circuit (Rem_9) transforms A_v into X_v. On the Shor graph, this means:
- Measuring X on support vertex (inl i) after the circuit = measuring A_{inl i} before
- Measuring X on dummy vertex (inr i) after the circuit = measuring A_{inr i} before
- The dummy X measurements in Shor-style correspond to measuring A_{d_i}
- The product of all A_v measurements = L' measurement (by gaussLaw_product)
This is the content of Rem_9's entanglingCircuit_transforms_gaussLaw applied to the Shor graph.
The entangling circuit transforms A_v to X_v on the Shor graph. Here v is a vertex of the Shor graph (a ShorVertex W), and the result is pauliX (Sum.inl v) on the ExtQubit type.
The inverse: the CX circuit transforms X_v back to A_v.
The circuit is involutive: applying it twice gives the identity.
The circuit preserves Pauli commutation.
Edge structure of the Shor graph #
The edge set of the Shor graph decomposes into:
- W pairing edges {(inl i, inr i)} for i ∈ Fin W
- The edges of the dummy subgraph Gdummy (lifted to Sum.inr)
We prove properties about this decomposition.
Support-support edges don't exist: no two support qubits are adjacent.
Support-dummy edges are exactly pairing edges: (inl i) ~ (inr j) iff i = j.
Dummy-dummy edges are exactly the dummy subgraph edges.
The degree of a support vertex i in the Shor graph is exactly 1 (only the pairing edge to d_i).
The degree of each support vertex is exactly 1.
The neighbor set of a dummy vertex i in the Shor graph is {inl i} ∪ (Gdummy neighbors of i lifted to Sum.inr).
Structural correspondence with Shor-style measurement #
The Shor-style measurement protocol corresponds to the gauging procedure as follows:
| Shor-style step | Gauging step |
|---|---|
| GHZ state preparation on W dummy qubits | Connected dummy subgraph edges |
| Transversal CX_{d_i → i} | Pairing edges {d_i, i} |
| Measure X on each d_i | Measure A_{d_i} (Gauss operator at dummy vertex) |
| Product of outcomes = σ | σ = ∑_v ε_v (measurement sign) |
The key insight: after measuring the dummy subgraph edges (during ungauging), the remaining dummy qubits form a GHZ state entangled with support qubits via the W pairing edges. This is exactly the Shor-style entanglement structure.
The advantage of the gauging viewpoint: the dummy subgraph can be chosen freely (path graph, star graph, expander, etc.) to optimize for hardware constraints.
The Shor graph is connected.
All Gauss operators on the Shor graph mutually commute.
Each Gauss operator is self-inverse.
Measuring all A_v and taking the product gives the measurement of L'. This is the fundamental equivalence that makes the gauging procedure work.
The Gauss operator at a dummy vertex d_i is pure X-type.
The Gauss operator at a support vertex i is pure X-type.
Structural correspondence summary.
Degree sum and edge count analysis #
The Shor graph has a special structure: support vertices have degree 1, and dummy vertex degrees are determined by the dummy subgraph. We derive degree sums and edge count bounds from these structural properties.
The degree of dummy vertex i in the Shor graph is 1 + its degree in Gdummy.
The sum of degrees of support vertices is W (each has degree 1).
The sum of degrees of dummy vertices is W + ∑ deg_Gdummy(i).
Total degree sum of the Shor graph equals 2 × |E(ShorGraph)|.
The total degree sum decomposes as support + dummy contributions.
A connected dummy subgraph on W vertices has at least W-1 edges.
Optimization flexibility: degree bounds #
The key advantage of the gauging viewpoint over standard Shor-style measurement: the dummy subgraph can be optimized for specific constraints.
If Gdummy has maximum degree d, then every vertex in the Shor graph has degree at most max(1, d+1). For a path graph (d=2), the Shor graph has max degree 3. We formalize this max degree transfer property.
If every dummy vertex has degree ≤ d in Gdummy, then every dummy vertex has degree ≤ d + 1 in the Shor graph (adding the pairing edge).
Max degree of the entire Shor graph is bounded by d + 1.
The Shor graph edge count via the handshaking identity.
The handshaking lemma applied to the dummy subgraph.