Rem_21: CSS Code Initialization as Gauging

Statement

Standard CSS code initialization can be implemented via hypergraph gauging.

Standard initialization: A CSS code is typically initialized by preparing |0⟩^⊗n and measuring all X-type checks.

Gauging formulation:

1. Start with a trivial code having one dummy vertex for each X-type check of the target CSS code
2. Perform the generalized gauging measurement using the hypergraph corresponding to the Z-type checks of the CSS code
3. The ungauging step performs readout measurement of Z on all qubits

Steane-style measurement via gauging: The state preparation and readout gauging procedure can be combined with another gauging measurement to implement a Steane-style measurement of a stabilizer group:

1. Perform state preparation of an ancilla code block via gauging as described above
2. Perform a gauging measurement of XX on pairs of matching qubits between the data code block and the ancilla code block
3. Perform the ungauging step to read out Z on all ancilla qubits

This connection shows that many existing fault-tolerant gadgets can be unified under the gauging framework.

Formalization Approach

We formalize the algebraic content underlying CSS initialization as gauging:

1. CSS code structure with X-type and Z-type checks satisfying orthogonality
2. The Z-check initialization hypergraph
3. Core theorem: CSS orthogonality implies X-checks lie in ker(H_Z), making them measurable via the hypergraph gauging procedure
4. Dummy vertex structure for the trivial starting code
5. Steane-style measurement: data + ancilla blocks with pairwise XX operators

Main Results

• CSSCode : CSS code structure with X and Z type checks
• CSSCode.initHypergraph : The Z-check initialization hypergraph
• CSSCode.xCheckVector : X-check support as a binary vector
• CSSCode.xCheck_in_kernel : X-checks are in ker(H_Z) by CSS orthogonality
• CSSCode.xCheck_measurable : X-checks are measurable via hypergraph gauging
• CSSCode.xCheck_sum_measurable : Sums of X-checks are measurable (closure)
• CSSInitVertex : Vertex type for initialization (qubits + dummies)
• cssInitVertex_card : Total vertices = n + numXChecks
• SteaneVertex : Vertex type for Steane measurement (data + ancilla)
• steaneVertex_card : Total Steane vertices = 2n
• pairwiseXXSupport : Support of XX operator on matching qubit pairs
• pairwiseXX_weight : Each XX operator has weight 2

Section 1: CSS Code Structure

A CSS (Calderbank-Shor-Steane) code has two types of check generators:

• X-type checks: products of X operators (define X-stabilizers)
• Z-type checks: products of Z operators (define Z-stabilizers)

The CSS condition requires: every X-check commutes with every Z-check. In binary vector language: |supp(X_check) ∩ supp(Z_check)| ≡ 0 (mod 2).

structure QEC1.CSSCodeInitializationAsGauging.CSSCode : Type

A CSS code with separate X-type and Z-type checks satisfying orthogonality.

• numQubits : ℕ

  Number of physical qubits

• numXChecks : ℕ

  Number of X-type check generators

• numZChecks : ℕ

  Number of Z-type check generators

• numQubits_pos : 0 < self.numQubits

  At least one qubit

• xCheckSupport : Fin self.numXChecks → Finset (Fin self.numQubits)

  Support of X-type check i (qubits where X acts)

• zCheckSupport : Fin self.numZChecks → Finset (Fin self.numQubits)

  Support of Z-type check j (qubits where Z acts)

• xCheck_nonempty (i : Fin self.numXChecks) : (self.xCheckSupport i).Nonempty

  X-checks have non-empty support

• zCheck_nonempty (j : Fin self.numZChecks) : (self.zCheckSupport j).Nonempty

  Z-checks have non-empty support

• css_orthogonality (i : Fin self.numXChecks) (j : Fin self.numZChecks) : (self.xCheckSupport i ∩ self.zCheckSupport j).card % 2 = 0

  CSS orthogonality: |supp(X_i) ∩ supp(Z_j)| ≡ 0 (mod 2) for all i, j

def QEC1.CSSCodeInitializationAsGauging.CSSCode.xCheckWeight (C : CSSCode) (i : Fin C.numXChecks) : ℕ

Weight of the i-th X-type check

Equations

• C.xCheckWeight i = (C.xCheckSupport i).card

def QEC1.CSSCodeInitializationAsGauging.CSSCode.zCheckWeight (C : CSSCode) (j : Fin C.numZChecks) : ℕ

Weight of the j-th Z-type check

Equations

• C.zCheckWeight j = (C.zCheckSupport j).card

theorem QEC1.CSSCodeInitializationAsGauging.CSSCode.xCheckWeight_pos (C : CSSCode) (i : Fin C.numXChecks) : 0 < C.xCheckWeight i

X-check weights are positive

theorem QEC1.CSSCodeInitializationAsGauging.CSSCode.zCheckWeight_pos (C : CSSCode) (j : Fin C.numZChecks) : 0 < C.zCheckWeight j

Z-check weights are positive

Section 2: Initialization Hypergraph

For CSS initialization via gauging, the Z-type checks define the hypergraph:

• Vertices = physical qubits (Fin n)
• Hyperedges = supports of Z-type checks (Fin numZChecks)

This hypergraph encodes the "gauging structure" for initialization.

def QEC1.CSSCodeInitializationAsGauging.CSSCode.initHypergraph (C : CSSCode) : HypergraphGeneralization.Hypergraph (Fin C.numQubits) (Fin C.numZChecks)

The initialization hypergraph: vertices are qubits, hyperedges are Z-check supports.

Equations

• C.initHypergraph = { incidence := C.zCheckSupport }

theorem QEC1.CSSCodeInitializationAsGauging.CSSCode.initHypergraph_numVertices (C : CSSCode) : Fintype.card (Fin C.numQubits) = C.numQubits

The initialization hypergraph has numQubits vertices

theorem QEC1.CSSCodeInitializationAsGauging.CSSCode.initHypergraph_numEdges (C : CSSCode) : Fintype.card (Fin C.numZChecks) = C.numZChecks

The initialization hypergraph has numZChecks hyperedges

Section 3: X-Checks in Kernel of H_Z

The key algebraic fact: CSS orthogonality ensures that every X-type check is in the kernel of the Z-check parity-check map (H_Z).

This is why gauging with the Z-check hypergraph allows measuring X-checks: operators in ker(H_Z) commute with all Z-type hyperedge operators.

def QEC1.CSSCodeInitializationAsGauging.CSSCode.xCheckVector (C : CSSCode) (i : Fin C.numXChecks) : HypergraphGeneralization.Hypergraph.VectorV (Fin C.numQubits)

The i-th X-check as a binary vector on qubits: 1 at qubit v if v ∈ supp(X_i)

Equations

• C.xCheckVector i v = if v ∈ C.xCheckSupport i then 1 else 0

@[simp]

theorem QEC1.CSSCodeInitializationAsGauging.CSSCode.xCheckVector_at_support (C : CSSCode) (i : Fin C.numXChecks) (v : Fin C.numQubits) (hv : v ∈ C.xCheckSupport i) : C.xCheckVector i v = 1

@[simp]

theorem QEC1.CSSCodeInitializationAsGauging.CSSCode.xCheckVector_outside_support (C : CSSCode) (i : Fin C.numXChecks) (v : Fin C.numQubits) (hv : v ∉ C.xCheckSupport i) : C.xCheckVector i v = 0

theorem QEC1.CSSCodeInitializationAsGauging.CSSCode.xCheck_in_kernel (C : CSSCode) (i : Fin C.numXChecks) : C.xCheckVector i ∈ C.initHypergraph.operatorKernel

Core Theorem: X-checks are in the kernel of the initialization hypergraph.

H_Z(x_i)j = ∑{v ∈ supp(Z_j)} x_i(v) = |supp(X_i) ∩ supp(Z_j)| (mod 2) = 0

This follows directly from CSS orthogonality.

theorem QEC1.CSSCodeInitializationAsGauging.CSSCode.xCheck_measurable (C : CSSCode) (i : Fin C.numXChecks) : C.xCheckVector i ∈ C.initHypergraph.operatorKernel

X-checks are measurable via the hypergraph gauging procedure.

theorem QEC1.CSSCodeInitializationAsGauging.CSSCode.xCheck_sum_in_kernel (C : CSSCode) (i j : Fin C.numXChecks) : C.xCheckVector i + C.xCheckVector j ∈ C.initHypergraph.operatorKernel

Sum (XOR) of X-checks is also in the kernel (closure under addition).

theorem QEC1.CSSCodeInitializationAsGauging.CSSCode.zero_in_kernel (C : CSSCode) : 0 ∈ C.initHypergraph.operatorKernel

The zero vector is always in the kernel.

Section 4: Dummy Vertex Structure

In the gauging interpretation, we start with a "trivial code" having one dummy vertex per X-type check. Each dummy corresponds to an X-check measurement. The dummy vertices are initialized in |+⟩ and have no effect on the gauging outcome (measuring X on |+⟩ always returns +1).

inductive QEC1.CSSCodeInitializationAsGauging.CSSInitVertex (C : CSSCode) : Type

Vertex type for CSS initialization: physical qubits plus one dummy per X-check

• qubit {C : CSSCode} : Fin C.numQubits → CSSInitVertex C
• dummy {C : CSSCode} : Fin C.numXChecks → CSSInitVertex C

def QEC1.CSSCodeInitializationAsGauging.instDecidableEqCSSInitVertex.decEq {C✝ : CSSCode} (x✝ x✝¹ : CSSInitVertex C✝) : Decidable (x✝ = x✝¹)

Equations

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

instance QEC1.CSSCodeInitializationAsGauging.instDecidableEqCSSInitVertex {C✝ : CSSCode} : DecidableEq (CSSInitVertex C✝)

Equations

• QEC1.CSSCodeInitializationAsGauging.instDecidableEqCSSInitVertex = QEC1.CSSCodeInitializationAsGauging.instDecidableEqCSSInitVertex.decEq

theorem QEC1.CSSCodeInitializationAsGauging.CSSInitVertex.qubit_injective {C : CSSCode} : Function.Injective qubit

theorem QEC1.CSSCodeInitializationAsGauging.CSSInitVertex.dummy_injective {C : CSSCode} : Function.Injective dummy

theorem QEC1.CSSCodeInitializationAsGauging.CSSInitVertex.qubit_ne_dummy {C : CSSCode} (i : Fin C.numQubits) (j : Fin C.numXChecks) : qubit i ≠ dummy j

instance QEC1.CSSCodeInitializationAsGauging.instFintypeCSSInitVertex (C : CSSCode) : Fintype (CSSInitVertex C)

Fintype instance for CSSInitVertex

Equations

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

theorem QEC1.CSSCodeInitializationAsGauging.cssInitVertex_card (C : CSSCode) : Fintype.card (CSSInitVertex C) = C.numQubits + C.numXChecks

Total initialization vertices = physical qubits + dummies (one per X-check)

def QEC1.CSSCodeInitializationAsGauging.CSSInitVertex.isDummy {C : CSSCode} : CSSInitVertex C → Bool

A predicate distinguishing dummy vertices

Equations

• (QEC1.CSSCodeInitializationAsGauging.CSSInitVertex.dummy a).isDummy = true
• (QEC1.CSSCodeInitializationAsGauging.CSSInitVertex.qubit a).isDummy = false

theorem QEC1.CSSCodeInitializationAsGauging.cssInitVertex_dummy_count (C : CSSCode) : {v : CSSInitVertex C | v.isDummy = true}.card = C.numXChecks

There are exactly numXChecks dummy vertices

Section 5: Gauging Procedure for Initialization

The three-step gauging procedure for CSS initialization:

Step 1: Start with a trivial code. The dummy vertices represent the X-check generators. The initialization state is |0⟩^⊗n on qubits and |+⟩ on dummies.

Step 2: Perform generalized gauging with Z-check hypergraph. This measures the generalized Gauss's law operators A_v = X_v ∏_{e ∋ v} X_e. Since X-checks are in ker(H_Z), they are preserved by the gauging.

Step 3: Ungauging readout: measure Z on all qubits.

The key algebraic property connecting these steps is that X-checks being in ker(H_Z) means they are measurable via the gauging procedure.

theorem QEC1.CSSCodeInitializationAsGauging.init_gauging_new_qubits (C : CSSCode) : C.initHypergraph.newQubitCount = C.numZChecks

The gauging procedure for CSS initialization introduces numZChecks new qubits (one per hyperedge = one per Z-check).

theorem QEC1.CSSCodeInitializationAsGauging.init_gauging_new_checks (C : CSSCode) : C.initHypergraph.newCheckCount = C.numQubits

The gauging procedure introduces numQubits new checks (one Gauss law operator A_v per qubit vertex).

theorem QEC1.CSSCodeInitializationAsGauging.init_gaussLaw_product (C : CSSCode) : ∑ v : Fin C.numQubits, C.initHypergraph.gaussLawVertexSupport v = fun (x : Fin C.numQubits) => 1

The sum of all Gauss law vertex supports equals the all-ones vector, representing L = ∏_v X_v (the product of all X operators).

Section 6: Steane-Style Measurement via Gauging

Steane's method for fault-tolerant measurement of a stabilizer group:

1. Initialize ancilla code block via CSS gauging (as above)
2. Perform gauging measurement of XX on matching qubit pairs between data and ancilla blocks
3. Ungauge to read out Z on all ancilla qubits

We formalize the data/ancilla block structure and the pairwise XX operators.

inductive QEC1.CSSCodeInitializationAsGauging.SteaneVertex (n : ℕ) : Type

Vertex type for Steane measurement: data block + ancilla block, both with n qubits

• data {n : ℕ} : Fin n → SteaneVertex n
• ancilla {n : ℕ} : Fin n → SteaneVertex n

def QEC1.CSSCodeInitializationAsGauging.instDecidableEqSteaneVertex.decEq {n✝ : ℕ} (x✝ x✝¹ : SteaneVertex n✝) : Decidable (x✝ = x✝¹)

Equations

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

instance QEC1.CSSCodeInitializationAsGauging.instDecidableEqSteaneVertex {n✝ : ℕ} : DecidableEq (SteaneVertex n✝)

Equations

• QEC1.CSSCodeInitializationAsGauging.instDecidableEqSteaneVertex = QEC1.CSSCodeInitializationAsGauging.instDecidableEqSteaneVertex.decEq

theorem QEC1.CSSCodeInitializationAsGauging.SteaneVertex.data_injective {n : ℕ} : Function.Injective data

theorem QEC1.CSSCodeInitializationAsGauging.SteaneVertex.ancilla_injective {n : ℕ} : Function.Injective ancilla

theorem QEC1.CSSCodeInitializationAsGauging.SteaneVertex.data_ne_ancilla {n : ℕ} (i j : Fin n) : data i ≠ ancilla j

instance QEC1.CSSCodeInitializationAsGauging.instFintypeSteaneVertex (n : ℕ) : Fintype (SteaneVertex n)

Fintype instance for SteaneVertex

Equations

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

instance QEC1.CSSCodeInitializationAsGauging.instDecidableEqSteaneVertex_1 (n : ℕ) : DecidableEq (SteaneVertex n)

DecidableEq for SteaneVertex needed downstream

Equations

• QEC1.CSSCodeInitializationAsGauging.instDecidableEqSteaneVertex_1 n = inferInstance

theorem QEC1.CSSCodeInitializationAsGauging.steaneVertex_card (n : ℕ) : Fintype.card (SteaneVertex n) = 2 * n

Total Steane vertices = 2n (data block + ancilla block)

def QEC1.CSSCodeInitializationAsGauging.pairwiseXXSupport {n : ℕ} (i : Fin n) : SteaneVertex n → ZMod 2

Pairwise XX operator support: 1 on data[i] and ancilla[i], 0 elsewhere. Represents the XX operator on matching qubit pairs for Steane measurement.

Equations

• QEC1.CSSCodeInitializationAsGauging.pairwiseXXSupport i (QEC1.CSSCodeInitializationAsGauging.SteaneVertex.data i_1) = if i_1 = i then 1 else 0
• QEC1.CSSCodeInitializationAsGauging.pairwiseXXSupport i (QEC1.CSSCodeInitializationAsGauging.SteaneVertex.ancilla i_1) = if i_1 = i then 1 else 0

@[simp]

theorem QEC1.CSSCodeInitializationAsGauging.pairwiseXXSupport_data_same {n : ℕ} (i : Fin n) : pairwiseXXSupport i (SteaneVertex.data i) = 1

@[simp]

theorem QEC1.CSSCodeInitializationAsGauging.pairwiseXXSupport_ancilla_same {n : ℕ} (i : Fin n) : pairwiseXXSupport i (SteaneVertex.ancilla i) = 1

@[simp]

theorem QEC1.CSSCodeInitializationAsGauging.pairwiseXXSupport_data_ne {n : ℕ} (i j : Fin n) (h : j ≠ i) : pairwiseXXSupport i (SteaneVertex.data j) = 0

@[simp]

theorem QEC1.CSSCodeInitializationAsGauging.pairwiseXXSupport_ancilla_ne {n : ℕ} (i j : Fin n) (h : j ≠ i) : pairwiseXXSupport i (SteaneVertex.ancilla j) = 0

theorem QEC1.CSSCodeInitializationAsGauging.pairwiseXX_weight {n : ℕ} (_hn : 0 < n) (i : Fin n) : {v : SteaneVertex n | pairwiseXXSupport i v = 1}.card = 2

Weight of pairwise XX operator is 2: each XX acts on exactly 2 qubits.

theorem QEC1.CSSCodeInitializationAsGauging.pairwiseXX_commute {n : ℕ} (i j : Fin n) : HypergraphGeneralization.Hypergraph.symplecticInnerProductV (pairwiseXXSupport i) 0 (pairwiseXXSupport j) 0 = 0

All pairwise XX operators commute with each other (they are X-type operators).

Section 7: Steane Gauging Hypergraph

The Steane measurement can be formulated as a gauging measurement using a hypergraph on the combined data + ancilla vertex set. The hyperedges are the pairwise XX connections between matching qubits.

def QEC1.CSSCodeInitializationAsGauging.steaneHypergraph (n : ℕ) : HypergraphGeneralization.Hypergraph (SteaneVertex n) (Fin n)

The Steane gauging hypergraph: vertices are data + ancilla qubits, hyperedges correspond to pairwise XX connections.

Equations

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

theorem QEC1.CSSCodeInitializationAsGauging.steaneHypergraph_edge_card (n : ℕ) (i : Fin n) : ((steaneHypergraph n).incidence i).card = 2

Each hyperedge of the Steane hypergraph has exactly 2 vertices.

theorem QEC1.CSSCodeInitializationAsGauging.steaneHypergraph_graphLike (n : ℕ) : (steaneHypergraph n).isGraphLike

The Steane hypergraph is graph-like (all edges have size 2).

theorem QEC1.CSSCodeInitializationAsGauging.steaneHypergraph_allOnes_in_kernel (n : ℕ) : HypergraphGeneralization.Hypergraph.allOnesV ∈ (steaneHypergraph n).operatorKernel

The all-ones vector on all Steane vertices is in the kernel (each edge has even cardinality).

Section 8: Three-Step Steane Procedure as Gauging

The complete Steane-style measurement decomposes into three gauging steps:

1. State preparation: Initialize ancilla code block via CSS gauging (prepare |0⟩^⊗n, gauge with Z-check hypergraph to measure X-checks)

2. Entangling step: Gauge with pairwise XX between data and ancilla (this is equivalent to transversal CNOT in Steane's original)

3. Readout: Ungauge by measuring Z on all ancilla qubits

We formalize the key algebraic property: the composition of these steps preserves the measurability of the stabilizer group.

inductive QEC1.CSSCodeInitializationAsGauging.SteaneGaugingStep : Type

The three steps of Steane measurement via gauging.

• statePreparation : SteaneGaugingStep
• entanglingMeasurement : SteaneGaugingStep
• readout : SteaneGaugingStep

instance QEC1.CSSCodeInitializationAsGauging.instDecidableEqSteaneGaugingStep : DecidableEq SteaneGaugingStep

Equations

• QEC1.CSSCodeInitializationAsGauging.instDecidableEqSteaneGaugingStep x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance QEC1.CSSCodeInitializationAsGauging.instFintypeSteaneGaugingStep : Fintype SteaneGaugingStep

Equations

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

theorem QEC1.CSSCodeInitializationAsGauging.steane_step_count : Fintype.card SteaneGaugingStep = 3

There are exactly 3 steps in the Steane gauging procedure.

def QEC1.CSSCodeInitializationAsGauging.readoutSupport (n : ℕ) : SteaneVertex n → ZMod 2

The readout step measures Z on ancilla qubits only (not data qubits).

Equations

• QEC1.CSSCodeInitializationAsGauging.readoutSupport n (QEC1.CSSCodeInitializationAsGauging.SteaneVertex.data i) = 0
• QEC1.CSSCodeInitializationAsGauging.readoutSupport n (QEC1.CSSCodeInitializationAsGauging.SteaneVertex.ancilla i) = 1

@[simp]

theorem QEC1.CSSCodeInitializationAsGauging.readoutSupport_data (n : ℕ) (i : Fin n) : readoutSupport n (SteaneVertex.data i) = 0

Readout support is nonzero only on ancilla qubits

@[simp]

theorem QEC1.CSSCodeInitializationAsGauging.readoutSupport_ancilla (n : ℕ) (i : Fin n) : readoutSupport n (SteaneVertex.ancilla i) = 1

theorem QEC1.CSSCodeInitializationAsGauging.readout_weight (n : ℕ) (_hn : 0 < n) : {v : SteaneVertex n | readoutSupport n v = 1}.card = n

The number of qubits measured in readout is n (all ancilla qubits).

Section 9: Unification Under Gauging Framework

The key insight: standard fault-tolerant gadgets (CSS initialization, Steane measurement) are special cases of the hypergraph gauging framework from Rem_15.

theorem QEC1.CSSCodeInitializationAsGauging.css_init_is_gauging (C : CSSCode) (i : Fin C.numXChecks) : C.xCheckVector i ∈ C.initHypergraph.operatorKernel

CSS initialization is a special case of hypergraph gauging: the Z-check hypergraph has the property that all X-checks are in its kernel (measurable group).

theorem QEC1.CSSCodeInitializationAsGauging.css_init_measurable_group_contains_xChecks (C : CSSCode) (i j : Fin C.numXChecks) : C.xCheckVector i + C.xCheckVector j ∈ C.initHypergraph.operatorKernel

The measurable group for CSS initialization contains all X-check combinations.

theorem QEC1.CSSCodeInitializationAsGauging.steane_is_2local (n : ℕ) : (steaneHypergraph n).isKLocalHypergraph 2

The Steane gauging hypergraph is 2-local (graph-like).

theorem QEC1.CSSCodeInitializationAsGauging.pairwiseXX_in_steane_kernel {n : ℕ} (i : Fin n) : pairwiseXXSupport i ∈ (steaneHypergraph n).operatorKernel

Combining CSS initialization and Steane measurement: the pairwise XX operators have even overlap with the Steane hypergraph (since each XX acts on exactly one vertex per edge).

theorem QEC1.CSSCodeInitializationAsGauging.sum_pairwiseXX_is_allOnes {n : ℕ} : ∑ i : Fin n, pairwiseXXSupport i = fun (x : SteaneVertex n) => 1

Sum of all pairwise XX operators is the all-ones vector (product of all XX).

Summary

This formalization captures Remark 21 about CSS code initialization as gauging:

Definitions:

• CSSCode: CSS code structure with X-type and Z-type checks + orthogonality
• CSSCode.initHypergraph: The Z-check initialization hypergraph
• CSSCode.xCheckVector: X-check support as binary vector
• CSSInitVertex: Qubit + dummy vertex type for initialization
• SteaneVertex: Data + ancilla vertex type for Steane measurement
• steaneHypergraph: The pairwise XX gauging hypergraph
• SteaneGaugingStep: The three steps of Steane measurement

Key Results:

• xCheck_in_kernel: CSS orthogonality ⟹ X-checks ∈ ker(H_Z)
• xCheck_sum_in_kernel: Kernel closed under addition (XOR of X-checks)
• cssInitVertex_card: Total initialization vertices = n + numXChecks
• steaneVertex_card: Total Steane vertices = 2n
• pairwiseXX_weight: Each XX operator has weight 2
• pairwiseXX_in_steane_kernel: XX operators are in the Steane hypergraph kernel
• sum_pairwiseXX_is_allOnes: Product of all XX gives the logical operator
• steane_is_2local: Steane hypergraph is 2-local (graph-like)