Remark 25: Steane-Style Measurement as Gauging

Statement

The gauging measurement procedure can implement Steane-style measurement of a stabilizer group by combining two gauging procedures.

Standard Steane-style measurement:

1. Prepare an ancilla code block in a known state.
2. Apply transversal CX gates between data and ancilla.
3. Read out the ancilla in the Z basis.
4. The outcomes reveal the data's stabilizer eigenvalues.

Implementation via gauging (for CSS ancilla code):

• Step 1: State preparation via hypergraph gauging (Rem_17)
• Step 2: Entangling via gauging (Def_5) using a perfect matching graph
• Step 3: Readout via Z measurements (ungauging step of Def_5)

Main Results

• IsCSS : a stabilizer code is CSS if every check is pure X-type or pure Z-type
• matchingGraphAdj : the perfect matching graph connecting data-ancilla pairs
• MatchingGraph : the matching graph as a SimpleGraph
• matching_components : each data-ancilla pair forms a connected component
• matchingGraph_card : the matching graph has 2n vertices
• matchingGraph_degree_eq_one : every vertex has degree 1
• step1_state_prep_hypergraph : Step 1 uses hypergraph gauging for Z checks
• step2_gauss_commute : Step 2 Gauss operators commute
• step2_gauss_product : Step 2 produces the XX logical
• step3_readout_is_ungauging : Step 3 is the ungauging step
• steane_is_composition_of_gauging : Steane-style measurement decomposes into gaugings

CSS stabilizer codes

A CSS (Calderbank-Shor-Steane) code is a stabilizer code where every check is either purely X-type (zVec = 0) or purely Z-type (xVec = 0).

def SteaneStyleMeasurement.IsCSS {Q : Type u_1} [DecidableEq Q] [Fintype Q] (C : StabilizerCode Q) : Prop

A stabilizer code is CSS if every check is either pure X-type or pure Z-type.

Equations

• SteaneStyleMeasurement.IsCSS C = ∀ (i : C.I), (C.check i).zVec = 0 ∨ (C.check i).xVec = 0

def SteaneStyleMeasurement.xCheckIndices {Q : Type u_1} [DecidableEq Q] [Fintype Q] (C : StabilizerCode Q) [DecidableEq C.I] : Finset C.I

The X-type check indices of a CSS code.

Equations

• SteaneStyleMeasurement.xCheckIndices C = {i : C.I | (C.check i).zVec = 0 ∧ (C.check i).xVec ≠ 0}

def SteaneStyleMeasurement.zCheckIndices {Q : Type u_1} [DecidableEq Q] [Fintype Q] (C : StabilizerCode Q) [DecidableEq C.I] : Finset C.I

The Z-type check indices of a CSS code.

Equations

• SteaneStyleMeasurement.zCheckIndices C = {i : C.I | (C.check i).xVec = 0 ∧ (C.check i).zVec ≠ 0}

theorem SteaneStyleMeasurement.xCheck_is_pureX {Q : Type u_1} [DecidableEq Q] [Fintype Q] (C : StabilizerCode Q) [DecidableEq C.I] (i : C.I) (hi : i ∈ xCheckIndices C) : (C.check i).zVec = 0

An X-type check has no Z-support.

theorem SteaneStyleMeasurement.zCheck_is_pureZ {Q : Type u_1} [DecidableEq Q] [Fintype Q] (C : StabilizerCode Q) [DecidableEq C.I] (i : C.I) (hi : i ∈ zCheckIndices C) : (C.check i).xVec = 0

A Z-type check has no X-support.

theorem SteaneStyleMeasurement.xChecks_commute {Q : Type u_1} [DecidableEq Q] [Fintype Q] (C : StabilizerCode Q) [DecidableEq C.I] (i j : C.I) (_hi : i ∈ xCheckIndices C) (_hj : j ∈ xCheckIndices C) : (C.check i).PauliCommute (C.check j)

X-type checks are pure X-type (they mutually commute trivially).

theorem SteaneStyleMeasurement.zChecks_commute {Q : Type u_1} [DecidableEq Q] [Fintype Q] (C : StabilizerCode Q) [DecidableEq C.I] (i j : C.I) (_hi : i ∈ zCheckIndices C) (_hj : j ∈ zCheckIndices C) : (C.check i).PauliCommute (C.check j)

Z-type checks are pure Z-type (they mutually commute trivially).

theorem SteaneStyleMeasurement.pureX_pureX_commute {Q : Type u_1} [DecidableEq Q] [Fintype Q] (P R : PauliOp Q) (hP : P.zVec = 0) (hR : R.zVec = 0) : P.PauliCommute R

Two pure X-type operators commute (their symplectic inner product vanishes because all z-components are zero).

theorem SteaneStyleMeasurement.pureZ_pureZ_commute {Q : Type u_1} [DecidableEq Q] [Fintype Q] (P R : PauliOp Q) (hP : P.xVec = 0) (hR : R.xVec = 0) : P.PauliCommute R

Two pure Z-type operators commute.

theorem SteaneStyleMeasurement.identity_is_css_compatible {Q : Type u_1} [DecidableEq Q] [Fintype Q] : PauliOp.zVec 1 = 0 ∨ PauliOp.xVec 1 = 0

The identity check (zVec = 0 ∧ xVec = 0) is trivially CSS-compatible.

Step 1: State Preparation via Hypergraph Gauging

The ancilla code block is prepared by:

1. Starting with a trivial code (all qubits independent)
2. Adding one dummy qubit per X-type check of the ancilla CSS code
3. Performing hypergraph gauging (Rem_17) using the hypergraph whose hyperedges are the Z-type checks of the ancilla code

The hypergraph incidence relation is: qubit q is incident to Z-check i iff q participates in Z-check i (i.e., the Z-check acts nontrivially on q).

def SteaneStyleMeasurement.zCheckIncident {Q : Type u_1} {I : Type u_2} (checks : I → PauliOp Q) (q : Q) (i : I) : Prop

The incidence relation for state preparation: qubit q is incident to Z-check i iff the check has Z-action at q.

Equations

• SteaneStyleMeasurement.zCheckIncident checks q i = ((checks i).zVec q ≠ 0)

instance SteaneStyleMeasurement.zCheckIncident_decidable {Q : Type u_1} {I : Type u_2} (checks : I → PauliOp Q) (q : Q) (i : I) : Decidable (zCheckIncident checks q i)

Equations

• SteaneStyleMeasurement.zCheckIncident_decidable checks q i = inferInstanceAs (Decidable ((checks i).zVec q ≠ 0))

theorem SteaneStyleMeasurement.zCheck_boundary_eq {Q : Type u_1} [DecidableEq Q] [Fintype Q] {I : Type u_2} [DecidableEq I] [Fintype I] (checks : I → PauliOp Q) (γ : I → ZMod 2) (q : Q) : (HypergraphGeneralization.hyperBoundaryMap (zCheckIncident checks)) γ q = ∑ i : I, if (checks i).zVec q ≠ 0 then γ i else 0

The hypergraph boundary map for Z-check incidence computes the Z-parity at each qubit from a vector of check activations.

theorem SteaneStyleMeasurement.step1_gauss_pure_X {Q : Type u_1} [DecidableEq Q] [Fintype Q] {I : Type u_2} [DecidableEq I] [Fintype I] (checks : I → PauliOp Q) (v : Q) : (HypergraphGeneralization.hyperGaussLawOp (zCheckIncident checks) v).zVec = 0

The Gauss's law operators for Z-check hypergraph gauging are all pure X-type.

theorem SteaneStyleMeasurement.step1_gauss_commute {Q : Type u_1} [DecidableEq Q] [Fintype Q] {I : Type u_2} [DecidableEq I] [Fintype I] (checks : I → PauliOp Q) (v w : Q) : (HypergraphGeneralization.hyperGaussLawOp (zCheckIncident checks) v).PauliCommute (HypergraphGeneralization.hyperGaussLawOp (zCheckIncident checks) w)

The Gauss's law operators for Z-check hypergraph gauging mutually commute.

theorem SteaneStyleMeasurement.step1_state_prep_hypergraph {Q : Type u_1} [DecidableEq Q] [Fintype Q] {I : Type u_2} [DecidableEq I] [Fintype I] (checks : I → PauliOp Q) : (∀ (v w : Q), (HypergraphGeneralization.hyperGaussLawOp (zCheckIncident checks) v).PauliCommute (HypergraphGeneralization.hyperGaussLawOp (zCheckIncident checks) w)) ∧ ∀ (v : Q), (HypergraphGeneralization.hyperGaussLawOp (zCheckIncident checks) v).zVec = 0

Step 1 (State preparation via hypergraph gauging). The hypergraph whose hyperedges correspond to the Z-type checks of the ancilla CSS code defines a valid hypergraph gauging (Rem_17). The boundary map encodes the Z-check parity structure: for each qubit q, (∂γ)q = Σ{i : Z-checks with support on q} γ_i. The Gauss operators A_v are all pure X-type and mutually commute.

Step 2: Entangling via Gauging — Perfect Matching Graph

The entangling step uses a graph G that is a perfect matching between data qubits and ancilla qubits. Each data qubit i is connected to the corresponding ancilla qubit i by a single edge.

The vertex set is (Fin n) ⊕ (Fin n) where:

• Sum.inl i represents data qubit i
• Sum.inr i represents ancilla qubit i

This graph measures XX on each pair (data_i, ancilla_i).

@[reducible, inline]

abbrev SteaneStyleMeasurement.MatchingVertex (n : ℕ) : Type

The vertex type: data qubits ⊕ ancilla qubits.

Equations

• SteaneStyleMeasurement.MatchingVertex n = (Fin n ⊕ Fin n)

def SteaneStyleMeasurement.matchingGraphAdj (n : ℕ) : MatchingVertex n → MatchingVertex n → Prop

The adjacency relation for the perfect matching graph: data qubit i is adjacent to ancilla qubit i (and no other edges).

Equations

• SteaneStyleMeasurement.matchingGraphAdj n p q = ∃ (i : Fin n), p = Sum.inl i ∧ q = Sum.inr i ∨ p = Sum.inr i ∧ q = Sum.inl i

theorem SteaneStyleMeasurement.matchingGraphAdj_symm (n : ℕ) (p q : MatchingVertex n) (h : matchingGraphAdj n p q) : matchingGraphAdj n q p

theorem SteaneStyleMeasurement.matchingGraphAdj_irrefl (n : ℕ) (p : MatchingVertex n) : ¬matchingGraphAdj n p p

instance SteaneStyleMeasurement.matchingGraphAdj_decidable (n : ℕ) : DecidableRel (matchingGraphAdj n)

Equations

• SteaneStyleMeasurement.matchingGraphAdj_decidable n p q = id inferInstance

def SteaneStyleMeasurement.MatchingGraph (n : ℕ) : SimpleGraph (MatchingVertex n)

The perfect matching graph between data and ancilla qubits.

Equations

• SteaneStyleMeasurement.MatchingGraph n = { Adj := SteaneStyleMeasurement.matchingGraphAdj n, symm := ⋯, loopless := ⋯ }

instance SteaneStyleMeasurement.instDecidableRelMatchingVertexAdjMatchingGraph (n : ℕ) : DecidableRel (MatchingGraph n).Adj

Equations

• SteaneStyleMeasurement.instDecidableRelMatchingVertexAdjMatchingGraph n = SteaneStyleMeasurement.matchingGraphAdj_decidable n

theorem SteaneStyleMeasurement.matchingGraph_card (n : ℕ) : Fintype.card (MatchingVertex n) = 2 * n

The matching graph has 2n vertices.

theorem SteaneStyleMeasurement.matchingGraph_adj_iff (n : ℕ) (p q : MatchingVertex n) : (MatchingGraph n).Adj p q ↔ ∃ (i : Fin n), p = Sum.inl i ∧ q = Sum.inr i ∨ p = Sum.inr i ∧ q = Sum.inl i

Each edge connects data qubit i to ancilla qubit i.

theorem SteaneStyleMeasurement.matching_edge (n : ℕ) (i : Fin n) : (MatchingGraph n).Adj (Sum.inl i) (Sum.inr i)

Data qubit i is adjacent to ancilla qubit i.

theorem SteaneStyleMeasurement.matching_edge_rev (n : ℕ) (i : Fin n) : (MatchingGraph n).Adj (Sum.inr i) (Sum.inl i)

Ancilla qubit i is adjacent to data qubit i.

theorem SteaneStyleMeasurement.no_data_data_edge (n : ℕ) (i j : Fin n) : ¬(MatchingGraph n).Adj (Sum.inl i) (Sum.inl j)

No two data qubits are adjacent.

theorem SteaneStyleMeasurement.no_ancilla_ancilla_edge (n : ℕ) (i j : Fin n) : ¬(MatchingGraph n).Adj (Sum.inr i) (Sum.inr j)

No two ancilla qubits are adjacent.

theorem SteaneStyleMeasurement.data_adj_iff (n : ℕ) (i : Fin n) (q : MatchingVertex n) : (MatchingGraph n).Adj (Sum.inl i) q ↔ q = Sum.inr i

Data qubit i is only adjacent to ancilla qubit i.

theorem SteaneStyleMeasurement.ancilla_adj_iff (n : ℕ) (i : Fin n) (q : MatchingVertex n) : (MatchingGraph n).Adj (Sum.inr i) q ↔ q = Sum.inl i

Ancilla qubit i is only adjacent to data qubit i.

theorem SteaneStyleMeasurement.matching_pair_reachable (n : ℕ) (i : Fin n) : (MatchingGraph n).Reachable (Sum.inl i) (Sum.inr i)

Each pair (data_i, ancilla_i) forms a connected component. Data qubit i and ancilla qubit i are reachable from each other.

theorem SteaneStyleMeasurement.matching_components (n : ℕ) (p q : MatchingVertex n) (h : (MatchingGraph n).Reachable p q) : ∃ (i : Fin n), (p = Sum.inl i ∨ p = Sum.inr i) ∧ (q = Sum.inl i ∨ q = Sum.inr i)

The matching graph consists of n connected components: each data-ancilla pair {inl i, inr i} is one component.

Step 2: Entangling via XX Gauging on Matching Pairs

The entangling step gauges XX on each data-ancilla pair independently. For each pair (data_i, ancilla_i), we have a single-edge graph connecting them. The Gauss operator at each vertex acts as X on the vertex and X on the edge.

theorem SteaneStyleMeasurement.step2_gauss_pure_X (n : ℕ) (v : MatchingVertex n) : (GaussFlux.gaussLawOp (MatchingGraph n) v).zVec = 0

The Gauss's law operator for the matching graph is pure X-type.

theorem SteaneStyleMeasurement.step2_gauss_commute (n : ℕ) (v w : MatchingVertex n) : (GaussFlux.gaussLawOp (MatchingGraph n) v).PauliCommute (GaussFlux.gaussLawOp (MatchingGraph n) w)

The Gauss's law operators for the matching graph all commute.

theorem SteaneStyleMeasurement.step2_gauss_product (n : ℕ) [Fintype ↑(MatchingGraph n).edgeSet] : ∏ v : MatchingVertex n, GaussFlux.gaussLawOp (MatchingGraph n) v = GaussFlux.logicalOp (MatchingGraph n)

The product of all Gauss operators on the matching graph equals the logical operator L = ∏_v X_v on all vertex qubits.

theorem SteaneStyleMeasurement.step2_gauss_self_inverse (n : ℕ) (v : MatchingVertex n) : GaussFlux.gaussLawOp (MatchingGraph n) v * GaussFlux.gaussLawOp (MatchingGraph n) v = 1

Each Gauss operator on the matching graph is self-inverse.

theorem SteaneStyleMeasurement.step2_logical_xVec (n : ℕ) [Fintype ↑(MatchingGraph n).edgeSet] (v : MatchingVertex n) : (GaussFlux.logicalOp (MatchingGraph n)).xVec (Sum.inl v) = 1

The logical operator on the matching graph acts as X on all vertex qubits.

theorem SteaneStyleMeasurement.step2_logical_pure_X (n : ℕ) [Fintype ↑(MatchingGraph n).edgeSet] : (GaussFlux.logicalOp (MatchingGraph n)).zVec = 0

The logical operator on the matching graph is pure X-type.

Step 3: Readout via Z Measurements (Ungauging)

The readout step measures Z_e on each edge qubit e, which is the ungauging step (Step 4 of Def_5). For the matching graph, each edge connects data_i to ancilla_i, so measuring Z on the edge qubit effectively reads out information about the ancilla in the Z basis.

After ungauging, the edge qubits are discarded and the system returns to operating on the original data + ancilla qubits.

theorem SteaneStyleMeasurement.step3_edgeZ_pure_Z (n : ℕ) (e : ↑(MatchingGraph n).edgeSet) : (PauliOp.pauliZ (Sum.inr e)).xVec = 0

Edge Z operators on the matching graph are pure Z-type (no X-support).

theorem SteaneStyleMeasurement.step3_edgeZ_commute (n : ℕ) (e₁ e₂ : ↑(MatchingGraph n).edgeSet) : (PauliOp.pauliZ (Sum.inr e₁)).PauliCommute (PauliOp.pauliZ (Sum.inr e₂))

Edge Z operators all commute (both pure Z-type).

theorem SteaneStyleMeasurement.step3_edgeZ_self_inverse (n : ℕ) (e : ↑(MatchingGraph n).edgeSet) : PauliOp.pauliZ (Sum.inr e) * PauliOp.pauliZ (Sum.inr e) = 1

Edge Z operators are self-inverse.

theorem SteaneStyleMeasurement.step3_readout_is_ungauging (n : ℕ) : (∀ (e₁ e₂ : ↑(MatchingGraph n).edgeSet), (PauliOp.pauliZ (Sum.inr e₁)).PauliCommute (PauliOp.pauliZ (Sum.inr e₂))) ∧ (∀ (e : ↑(MatchingGraph n).edgeSet), PauliOp.pauliZ (Sum.inr e) * PauliOp.pauliZ (Sum.inr e) = 1) ∧ ∀ (e : ↑(MatchingGraph n).edgeSet), (PauliOp.pauliZ (Sum.inr e)).xVec = 0

Step 3 (Readout is ungauging). The readout step consists of measuring Z on each edge qubit. All Z measurements commute and are self-inverse, which is exactly the ungauging step of Def_5.

Steane-Style Measurement as Composition of Gaugings

The full Steane-style measurement is a composition of three gauging operations:

Steane step	Gauging operation
Prepare ancilla in codestate	Hypergraph gauging (Rem_17) with Z-check hyperedges
Transversal CX (data ↔ ancilla)	Graph gauging (Def_5) with matching graph
Z readout of ancilla	Ungauging step (Z measurements on edge qubits)

The hypergraph gauging in Step 1 prepares the ancilla by:

• Initializing qubits in |+⟩ state
• Measuring Gauss operators A_v = X_v ∏_{e ∋ v} X_e (one per ancilla qubit)
• The hyperedges correspond to Z-type checks of the ancilla CSS code
• This projects into the +1 eigenspace of all Z-type stabilizers

The graph gauging in Steps 2-3 entangles data with ancilla by:

• Adding edge qubits in |0⟩ for each data-ancilla pair
• Measuring Gauss operators (XX type) on each pair
• Z-measuring edge qubits to ungauge

theorem SteaneStyleMeasurement.step2_cx_transforms_gauss (n : ℕ) (v : MatchingVertex n) : CircuitImplementation.entanglingCircuitAction (MatchingGraph n) (GaussFlux.gaussLawOp (MatchingGraph n) v) = PauliOp.pauliX (Sum.inl v)

The CX circuit transformation maps A_v to X_v on the matching graph.

theorem SteaneStyleMeasurement.step2_cx_transforms_pauliX (n : ℕ) (v : MatchingVertex n) : CircuitImplementation.entanglingCircuitAction (MatchingGraph n) (PauliOp.pauliX (Sum.inl v)) = GaussFlux.gaussLawOp (MatchingGraph n) v

The CX circuit transforms X_v back to A_v on the matching graph.

theorem SteaneStyleMeasurement.step2_cx_involutive (n : ℕ) (P : PauliOp (GaussFlux.ExtQubit (MatchingGraph n))) : CircuitImplementation.entanglingCircuitAction (MatchingGraph n) (CircuitImplementation.entanglingCircuitAction (MatchingGraph n) P) = P

The entangling circuit is involutive on the matching graph.

theorem SteaneStyleMeasurement.step2_cx_preserves_commutation (n : ℕ) (P R : PauliOp (GaussFlux.ExtQubit (MatchingGraph n))) : P.PauliCommute R ↔ (CircuitImplementation.entanglingCircuitAction (MatchingGraph n) P).PauliCommute (CircuitImplementation.entanglingCircuitAction (MatchingGraph n) R)

The entangling circuit preserves commutation relations.

theorem SteaneStyleMeasurement.steane_is_composition_of_gauging {Q : Type u_1} [DecidableEq Q] [Fintype Q] (n : ℕ) {I : Type u_2} [DecidableEq I] [Fintype I] (checks : I → PauliOp Q) : ((∀ (v w : Q), (HypergraphGeneralization.hyperGaussLawOp (zCheckIncident checks) v).PauliCommute (HypergraphGeneralization.hyperGaussLawOp (zCheckIncident checks) w)) ∧ ∀ (v : Q), (HypergraphGeneralization.hyperGaussLawOp (zCheckIncident checks) v).zVec = 0) ∧ ((∀ (v w : MatchingVertex n), (GaussFlux.gaussLawOp (MatchingGraph n) v).PauliCommute (GaussFlux.gaussLawOp (MatchingGraph n) w)) ∧ (∀ (v : MatchingVertex n), (GaussFlux.gaussLawOp (MatchingGraph n) v).zVec = 0) ∧ ∀ (v : MatchingVertex n), CircuitImplementation.entanglingCircuitAction (MatchingGraph n) (GaussFlux.gaussLawOp (MatchingGraph n) v) = PauliOp.pauliX (Sum.inl v)) ∧ (∀ (e₁ e₂ : ↑(MatchingGraph n).edgeSet), (PauliOp.pauliZ (Sum.inr e₁)).PauliCommute (PauliOp.pauliZ (Sum.inr e₂))) ∧ ∀ (e : ↑(MatchingGraph n).edgeSet), PauliOp.pauliZ (Sum.inr e) * PauliOp.pauliZ (Sum.inr e) = 1

Steane-style measurement is a composition of gauging operations.

Ancilla Code Properties

The key properties of the ancilla CSS code that make the decomposition work:

1. Z-type checks define the hypergraph for state preparation
2. X-type checks determine the number of dummy qubits needed
3. The CSS property ensures X and Z checks can be handled independently

theorem SteaneStyleMeasurement.css_check_partition {Q : Type u_1} [DecidableEq Q] [Fintype Q] (C : StabilizerCode Q) [DecidableEq C.I] (hcss : IsCSS C) (i : C.I) (hne : C.check i ≠ 1) : i ∈ xCheckIndices C ∨ i ∈ zCheckIndices C

For a CSS code, the X-type checks and Z-type checks cover all non-identity checks.

theorem SteaneStyleMeasurement.dummy_qubit_count {Q : Type u_1} [DecidableEq Q] [Fintype Q] (C : StabilizerCode Q) [DecidableEq C.I] : (xCheckIndices C).card = {i : C.I | (C.check i).zVec = 0 ∧ (C.check i).xVec ≠ 0}.card

The number of dummy qubits for state preparation equals the number of X-type checks in the ancilla CSS code.

theorem SteaneStyleMeasurement.xCheck_zCheck_commute {Q : Type u_1} [DecidableEq Q] [Fintype Q] (C : StabilizerCode Q) [DecidableEq C.I] (i j : C.I) (_hi : i ∈ xCheckIndices C) (_hj : j ∈ zCheckIndices C) : (C.check i).PauliCommute (C.check j)

For a CSS code, X-type checks commute with Z-type checks.

theorem SteaneStyleMeasurement.zCheck_boundary_structure {Q : Type u_1} [DecidableEq Q] [Fintype Q] (C : StabilizerCode Q) [DecidableEq C.I] (i : C.I) (_hi : i ∈ zCheckIndices C) (q : Q) : zCheckIncident C.check q i ↔ (C.check i).zVec q ≠ 0

The Z-check incidence boundary map encodes the Z-check parity structure.

Degree Analysis for the Matching Graph

The matching graph has a very simple structure:

• Each data vertex has degree exactly 1
• Each ancilla vertex has degree exactly 1
• Total edges = n (one per pair)

This gives the minimal possible overhead for the entangling step.

theorem SteaneStyleMeasurement.data_neighborFinset (n : ℕ) (i : Fin n) : (MatchingGraph n).neighborFinset (Sum.inl i) = {Sum.inr i}

The neighbor set of a data vertex i is just {inr i}.

theorem SteaneStyleMeasurement.ancilla_neighborFinset (n : ℕ) (i : Fin n) : (MatchingGraph n).neighborFinset (Sum.inr i) = {Sum.inl i}

The neighbor set of an ancilla vertex i is just {inl i}.

theorem SteaneStyleMeasurement.data_degree (n : ℕ) (i : Fin n) : (MatchingGraph n).degree (Sum.inl i) = 1

Each data vertex has degree exactly 1.

theorem SteaneStyleMeasurement.ancilla_degree (n : ℕ) (i : Fin n) : (MatchingGraph n).degree (Sum.inr i) = 1

Each ancilla vertex has degree exactly 1.

theorem SteaneStyleMeasurement.matchingGraph_degree_eq_one (n : ℕ) (v : MatchingVertex n) : (MatchingGraph n).degree v = 1

Every vertex in the matching graph has degree exactly 1.

theorem SteaneStyleMeasurement.matchingGraph_degree_sum (n : ℕ) : ∑ v : MatchingVertex n, (MatchingGraph n).degree v = 2 * n

The degree sum of the matching graph is 2n.

theorem SteaneStyleMeasurement.matchingGraph_edge_count (n : ℕ) : 2 * (MatchingGraph n).edgeFinset.card = 2 * n

The matching graph has exactly n edges (by handshaking: 2|E| = 2n).

Summary: Steane-style Measurement via Gauging

The formalization captures the key structural content of Remark 25:

1. CSS codes split into X-type and Z-type checks
2. State preparation uses hypergraph gauging on Z-type check incidence
3. Entangling uses graph gauging on a perfect matching
4. Readout uses Z measurements (ungauging)
5. The CX circuit equivalence from Rem_9 connects the two viewpoints

theorem SteaneStyleMeasurement.steane_measurement_summary {Q : Type u_1} [DecidableEq Q] [Fintype Q] (n : ℕ) {I : Type u_2} [DecidableEq I] [Fintype I] (checks : I → PauliOp Q) : (∀ (v w : Q), (HypergraphGeneralization.hyperGaussLawOp (zCheckIncident checks) v).PauliCommute (HypergraphGeneralization.hyperGaussLawOp (zCheckIncident checks) w)) ∧ (∀ (v w : MatchingVertex n), (GaussFlux.gaussLawOp (MatchingGraph n) v).PauliCommute (GaussFlux.gaussLawOp (MatchingGraph n) w)) ∧ (∀ (v : MatchingVertex n), CircuitImplementation.entanglingCircuitAction (MatchingGraph n) (GaussFlux.gaussLawOp (MatchingGraph n) v) = PauliOp.pauliX (Sum.inl v)) ∧ (∀ (e₁ e₂ : ↑(MatchingGraph n).edgeSet), (PauliOp.pauliZ (Sum.inr e₁)).PauliCommute (PauliOp.pauliZ (Sum.inr e₂))) ∧ (∀ (v : MatchingVertex n), (MatchingGraph n).degree v = 1) ∧ 2 * (MatchingGraph n).edgeFinset.card = 2 * n

Summary: Steane-style measurement decomposition.