Rem_15: Hypergraph Generalization of Gauging Measurement

Statement

The gauging measurement procedure can be generalized by replacing the graph G with a hypergraph to measure multiple operators simultaneously.

Setup: Consider an abelian group of operators describable as the X-type operators that commute with an auxiliary set of k-local Z-type checks. Using the stabilizer formalism, this group can be equivalently formulated as the kernel of a sparse linear map over F_2.

Procedure: For qubits, this is equivalent to replacing the graph G with a hypergraph. The generalized gauging procedure performs a code deformation by:

1. Introducing a qubit for each hyperedge
2. Measuring into new Gauss's law checks A_v given by the product of X on a vertex and the adjacent hyperedges: A_v = X_v ∏_{e ∋ v, e ∈ hyperedges} X_e

Application: This allows measuring any abelian group of commuting logical operators that can be characterized as the kernel of a sparse parity-check matrix.

Main Definitions

• Hypergraph : A hypergraph with vertices V and hyperedges H
• Hypergraph.incidenceMatrix : The incidence matrix over ZMod 2
• Hypergraph.parityCheckMap : The parity-check map H_Z : Z₂^V → Z₂^H
• Hypergraph.gaussLawSupport : The support of a generalized Gauss law operator A_v
• Hypergraph.toGraphWithCycles : A graph is a special case of a hypergraph (with edge size 2)

Key Properties

• gaussLaw_commute_hypergraph : All generalized A_v commute (symplectic inner product = 0)
• gaussLaw_vertex_support_sum_allOnes : ∑_v A_v support = all-ones on V (represents L)
• kernel_is_abelian_group : The abelian group of operators equals ker(H_Z)
• ofGraphWithCycles_isGraphLike : Ordinary graphs embed into hypergraphs
• kLocal_means_sparse_row : k-local Z-checks ↔ sparse parity-check matrix

Hypergraph Definition

A hypergraph generalizes a graph: each hyperedge connects a set of vertices (not necessarily just two).

structure QEC1.HypergraphGeneralization.Hypergraph (V : Type u_1) (H : Type u_2) [DecidableEq V] [Fintype V] [Fintype H] : Type (max u_1 u_2)

A hypergraph on vertices V with hyperedges indexed by H. Each hyperedge is a subset of vertices (represented as a Finset V).

• incidence : H → Finset V

  Each hyperedge maps to its set of incident vertices

Binary Vector Types

@[reducible, inline]

abbrev QEC1.HypergraphGeneralization.Hypergraph.VectorV (V : Type u_3) : Type u_3

Binary vectors over vertices: Z₂^V

Equations

• QEC1.HypergraphGeneralization.Hypergraph.VectorV V = (V → ZMod 2)

@[reducible, inline]

abbrev QEC1.HypergraphGeneralization.Hypergraph.VectorH (H : Type u_3) : Type u_3

Binary vectors over hyperedges: Z₂^H

Equations

• QEC1.HypergraphGeneralization.Hypergraph.VectorH H = (H → ZMod 2)

instance QEC1.HypergraphGeneralization.Hypergraph.instModuleZModOfNatNatVectorV {V : Type u_1} : Module (ZMod 2) (VectorV V)

Equations

• QEC1.HypergraphGeneralization.Hypergraph.instModuleZModOfNatNatVectorV = Pi.module V (fun (x : V) => ZMod 2) (ZMod 2)

instance QEC1.HypergraphGeneralization.Hypergraph.instModuleZModOfNatNatVectorH {H : Type u_2} : Module (ZMod 2) (VectorH H)

Equations

• QEC1.HypergraphGeneralization.Hypergraph.instModuleZModOfNatNatVectorH = Pi.module H (fun (x : H) => ZMod 2) (ZMod 2)

Incidence Matrix and Parity-Check Map

The incidence matrix M over F_2 has M_{h,v} = 1 iff vertex v ∈ hyperedge h. The parity-check map is the corresponding linear map Z₂^V → Z₂^H.

def QEC1.HypergraphGeneralization.Hypergraph.incidenceEntry {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (HG : Hypergraph V H) (h : H) (v : V) : ZMod 2

The incidence matrix entry: 1 if vertex v is in hyperedge h, 0 otherwise

Equations

• HG.incidenceEntry h v = if v ∈ HG.incidence h then 1 else 0

def QEC1.HypergraphGeneralization.Hypergraph.parityCheckMap {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (HG : Hypergraph V H) : VectorV V →ₗ[ZMod 2] VectorH H

The parity-check map H_Z : Z₂^V → Z₂^H. For each hyperedge h, (H_Z(x))h = ∑{v ∈ h} x_v (mod 2). This is the linear map whose kernel characterizes the abelian group.

Equations

• HG.parityCheckMap = { toFun := fun (x : QEC1.HypergraphGeneralization.Hypergraph.VectorV V) (h : H) => ∑ v ∈ HG.incidence h, x v, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem QEC1.HypergraphGeneralization.Hypergraph.parityCheckMap_apply {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (x : VectorV V) (h : H) : HG.parityCheckMap x h = ∑ v ∈ HG.incidence h, x v

Kernel Characterization

The abelian group of X-type operators that commute with all k-local Z-type checks is exactly the kernel of the parity-check map.

def QEC1.HypergraphGeneralization.Hypergraph.operatorKernel {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (HG : Hypergraph V H) : Submodule (ZMod 2) (VectorV V)

The kernel of the parity-check map: vectors x ∈ Z₂^V such that H_Z(x) = 0. This characterizes the abelian group of commuting X-type operators.

Equations

• HG.operatorKernel = HG.parityCheckMap.ker

@[simp]

theorem QEC1.HypergraphGeneralization.Hypergraph.mem_operatorKernel_iff {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (x : VectorV V) : x ∈ HG.operatorKernel ↔ ∀ (h : H), ∑ v ∈ HG.incidence h, x v = 0

Membership in the kernel: x ∈ ker(H_Z) iff ∑_{v ∈ h} x_v = 0 for all hyperedges h

k-Locality

A Z-type check is k-local if the corresponding hyperedge has at most k vertices.

def QEC1.HypergraphGeneralization.Hypergraph.isKLocal {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (HG : Hypergraph V H) (k : ℕ) (h : H) : Prop

A hyperedge h is k-local if it contains at most k vertices

Equations

• HG.isKLocal k h = ((HG.incidence h).card ≤ k)

def QEC1.HypergraphGeneralization.Hypergraph.isKLocalHypergraph {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (HG : Hypergraph V H) (k : ℕ) : Prop

The hypergraph is k-local if all hyperedges are k-local

Equations

• HG.isKLocalHypergraph k = ∀ (h : H), HG.isKLocal k h

theorem QEC1.HypergraphGeneralization.Hypergraph.kLocal_means_sparse_row {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (k : ℕ) (h : H) (hk : HG.isKLocal k h) : {v : V | HG.incidenceEntry h v ≠ 0}.card ≤ k

k-locality means the parity-check map is sparse: each row has at most k nonzero entries

Generalized Gauss Law Operators

In the hypergraph setting, the Gauss law operator A_v is: A_v = X_v ∏_{e ∋ v, e ∈ hyperedges} X_e

The support on vertex qubits: 1 at v, 0 elsewhere The support on hyperedge qubits: 1 at each hyperedge containing v

def QEC1.HypergraphGeneralization.Hypergraph.incidentHyperedges {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (HG : Hypergraph V H) (v : V) : Finset H

The set of hyperedges incident to vertex v

Equations

• HG.incidentHyperedges v = {h : H | v ∈ HG.incidence h}

def QEC1.HypergraphGeneralization.Hypergraph.gaussLawVertexSupport {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (_HG : Hypergraph V H) (v : V) : VectorV V

The vertex support of the generalized Gauss law operator A_v: a binary vector on V with 1 at v, 0 elsewhere (represents X_v)

Equations

• _HG.gaussLawVertexSupport v = Pi.single v 1

def QEC1.HypergraphGeneralization.Hypergraph.gaussLawHyperedgeSupport {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (HG : Hypergraph V H) (v : V) : VectorH H

The hyperedge support of A_v: 1 at each hyperedge containing v, 0 elsewhere

Equations

• HG.gaussLawHyperedgeSupport v h = if v ∈ HG.incidence h then 1 else 0

@[simp]

theorem QEC1.HypergraphGeneralization.Hypergraph.gaussLawVertexSupport_same {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (v : V) : HG.gaussLawVertexSupport v v = 1

@[simp]

theorem QEC1.HypergraphGeneralization.Hypergraph.gaussLawVertexSupport_ne {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (v w : V) (h : v ≠ w) : HG.gaussLawVertexSupport v w = 0

@[simp]

theorem QEC1.HypergraphGeneralization.Hypergraph.gaussLawHyperedgeSupport_mem {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (v : V) (h : H) (hv : v ∈ HG.incidence h) : HG.gaussLawHyperedgeSupport v h = 1

@[simp]

theorem QEC1.HypergraphGeneralization.Hypergraph.gaussLawHyperedgeSupport_not_mem {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (v : V) (h : H) (hv : v ∉ HG.incidence h) : HG.gaussLawHyperedgeSupport v h = 0

Properties of Generalized Gauss Law Operators

def QEC1.HypergraphGeneralization.Hypergraph.gaussLawZTypeSupport {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (_HG : Hypergraph V H) (_v : V) : VectorV V

All generalized Gauss law operators commute. Two Pauli operators P₁, P₂ commute iff the symplectic inner product of their supports is 0 (mod 2). Since A_v are purely X-type operators (no Z component), the Z-type support of each A_v is empty. Therefore the symplectic overlap is always 0.

We model this as: the Z-type support of each A_v is the zero vector (trivial), so the symplectic inner product ∑_i (X-support₁(i) * Z-support₂(i) + Z-support₁(i) * X-support₂(i)) is 0 for any pair of A_v operators.

Equations

• _HG.gaussLawZTypeSupport _v = 0

def QEC1.HypergraphGeneralization.Hypergraph.gaussLawZTypeHyperedgeSupport {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (_HG : Hypergraph V H) (_v : V) : VectorH H

Equations

• _HG.gaussLawZTypeHyperedgeSupport _v = 0

def QEC1.HypergraphGeneralization.Hypergraph.symplecticInnerProductV {V : Type u_1} [Fintype V] (xS₁ zS₁ xS₂ zS₂ : VectorV V) : ZMod 2

The symplectic inner product of two Pauli operators on the vertex qubits. For X-type support vectors xS₁, xS₂ and Z-type support vectors zS₁, zS₂, the symplectic product is ∑_i (xS₁(i) * zS₂(i) + zS₁(i) * xS₂(i)).

Equations

• QEC1.HypergraphGeneralization.Hypergraph.symplecticInnerProductV xS₁ zS₁ xS₂ zS₂ = ∑ i : V, (xS₁ i * zS₂ i + zS₁ i * xS₂ i)

def QEC1.HypergraphGeneralization.Hypergraph.symplecticInnerProductH {H : Type u_2} [Fintype H] (xS₁ zS₁ xS₂ zS₂ : VectorH H) : ZMod 2

The symplectic inner product on hyperedge qubits.

Equations

• QEC1.HypergraphGeneralization.Hypergraph.symplecticInnerProductH xS₁ zS₁ xS₂ zS₂ = ∑ i : H, (xS₁ i * zS₂ i + zS₁ i * xS₂ i)

theorem QEC1.HypergraphGeneralization.Hypergraph.gaussLaw_commute_hypergraph {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (v₁ v₂ : V) : symplecticInnerProductV (HG.gaussLawVertexSupport v₁) (HG.gaussLawZTypeSupport v₁) (HG.gaussLawVertexSupport v₂) (HG.gaussLawZTypeSupport v₂) = 0 ∧ symplecticInnerProductH (HG.gaussLawHyperedgeSupport v₁) (HG.gaussLawZTypeHyperedgeSupport v₁) (HG.gaussLawHyperedgeSupport v₂) (HG.gaussLawZTypeHyperedgeSupport v₂) = 0

All generalized Gauss law operators A_v commute: the symplectic inner product of A_v₁ and A_v₂ is 0 on both vertex and hyperedge qubits. This is because A_v has trivial (zero) Z-type support.

theorem QEC1.HypergraphGeneralization.Hypergraph.gaussLaw_vertex_support_sum_allOnes {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) : ∑ v : V, HG.gaussLawVertexSupport v = fun (x : V) => 1

The sum of all vertex supports is the all-ones vector on V. This corresponds to ∏_v A_v having L = ∏_v X_v as its vertex component.

theorem QEC1.HypergraphGeneralization.Hypergraph.gaussLaw_hyperedge_support_sum {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (h : H) : ∑ v : V, HG.gaussLawHyperedgeSupport v h = ↑(HG.incidence h).card

The sum of all hyperedge supports gives the cardinality (mod 2) at each hyperedge, because each hyperedge h has |incidence h| vertices contributing. In the graph case (each hyperedge has exactly 2 vertices), this is 0 mod 2.

theorem QEC1.HypergraphGeneralization.Hypergraph.gaussLaw_product_edge_zero {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (h_graphlike : ∀ (h : H), (HG.incidence h).card = 2) (h : H) : ∑ v : V, HG.gaussLawHyperedgeSupport v h = 0

For the graph case: when every hyperedge has exactly 2 vertices, the sum of all hyperedge supports is 0 (mod 2).

Graphs as Special Case of Hypergraphs

An ordinary graph (where every edge connects exactly 2 vertices) is a hypergraph where every hyperedge has exactly 2 vertices.

def QEC1.HypergraphGeneralization.Hypergraph.isGraphLike {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (HG : Hypergraph V H) : Prop

A hypergraph is graph-like if every hyperedge has exactly 2 vertices

Equations

• HG.isGraphLike = ∀ (h : H), (HG.incidence h).card = 2

def QEC1.HypergraphGeneralization.Hypergraph.ofGraphWithCycles {V : Type u_1} [DecidableEq V] [Fintype V] {E : Type u_3} {C : Type u_4} [DecidableEq E] [DecidableEq C] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) : Hypergraph V E

Construct a hypergraph from a GraphWithCycles

Equations

• QEC1.HypergraphGeneralization.Hypergraph.ofGraphWithCycles G = { incidence := fun (e : E) => G.edgeVertices e }

theorem QEC1.HypergraphGeneralization.Hypergraph.ofGraphWithCycles_isGraphLike {V : Type u_1} [DecidableEq V] [Fintype V] {E : Type u_3} {C : Type u_4} [DecidableEq E] [DecidableEq C] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) : (ofGraphWithCycles G).isGraphLike

A hypergraph derived from a graph is graph-like

Parity Check Matrix Sparsity

The parity-check matrix is sparse when the hypergraph is k-local.

theorem QEC1.HypergraphGeneralization.Hypergraph.parityCheck_sparse_rows {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (k : ℕ) (hk : HG.isKLocalHypergraph k) (h : H) : (HG.incidence h).card ≤ k

For a k-local hypergraph, the parity-check matrix has at most k entries per row

theorem QEC1.HypergraphGeneralization.Hypergraph.parityCheck_total_entries_bound {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (k : ℕ) (hk : HG.isKLocalHypergraph k) : ∑ h : H, (HG.incidence h).card ≤ k * Fintype.card H

The total number of nonzero entries in the incidence matrix is bounded by k * |H|

Application: Measuring Abelian Groups via Kernel

Any abelian group of commuting X-type logical operators that can be characterized as the kernel of a sparse parity-check matrix can be measured via hypergraph gauging.

theorem QEC1.HypergraphGeneralization.Hypergraph.kernel_is_abelian_group {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) : ∃ (S : Submodule (ZMod 2) (VectorV V)), ∀ (x : VectorV V), x ∈ S ↔ HG.parityCheckMap x = 0

The kernel of the parity-check map is a submodule (abelian group over F_2)

@[simp]

theorem QEC1.HypergraphGeneralization.Hypergraph.zero_mem_kernel {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) : 0 ∈ HG.operatorKernel

Zero vector is always in the kernel

theorem QEC1.HypergraphGeneralization.Hypergraph.kernel_add_closed {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (x y : VectorV V) (hx : x ∈ HG.operatorKernel) (hy : y ∈ HG.operatorKernel) : x + y ∈ HG.operatorKernel

The kernel is closed under addition (symmetric difference of supports)

Generalized Gauging Procedure

The generalized gauging procedure introduces one qubit per hyperedge and measures generalized Gauss law operators A_v = X_v ∏_{e ∋ v} X_e.

def QEC1.HypergraphGeneralization.Hypergraph.newQubitCount {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (_HG : Hypergraph V H) : ℕ

The number of new qubits introduced = number of hyperedges

Equations

• _HG.newQubitCount = Fintype.card H

def QEC1.HypergraphGeneralization.Hypergraph.newCheckCount {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (_HG : Hypergraph V H) : ℕ

The number of new checks = number of vertices (one A_v per vertex)

Equations

• _HG.newCheckCount = Fintype.card V

def QEC1.HypergraphGeneralization.Hypergraph.hypergraphCoboundary {V : Type u_1} {H : Type u_2} [DecidableEq V] [Fintype V] [Fintype H] (HG : Hypergraph V H) : VectorV V →ₗ[ZMod 2] VectorH H

The generalized coboundary map δ : Z₂^V → Z₂^H for the hypergraph. For vertex v, δ(v) = indicator vector of hyperedges containing v. This is the transpose of the incidence matrix.

Equations

• HG.hypergraphCoboundary = { toFun := fun (x : QEC1.HypergraphGeneralization.Hypergraph.VectorV V) (h : H) => ∑ v ∈ HG.incidence h, x v, map_add' := ⋯, map_smul' := ⋯ }

theorem QEC1.HypergraphGeneralization.Hypergraph.hypergraphCoboundary_eq_parityCheck {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) : HG.hypergraphCoboundary = HG.parityCheckMap

The hypergraph coboundary equals the parity-check map

def QEC1.HypergraphGeneralization.Hypergraph.allOnesV {V : Type u_1} : VectorV V

The all-ones vector on V represents the logical operator L = ∏_v X_v

Equations

• QEC1.HypergraphGeneralization.Hypergraph.allOnesV x✝ = 1

theorem QEC1.HypergraphGeneralization.Hypergraph.logical_in_kernel_iff {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) : allOnesV ∈ HG.operatorKernel ↔ ∀ (h : H), (HG.incidence h).card % 2 = 0

The logical operator L is in the kernel iff every hyperedge has even cardinality

theorem QEC1.HypergraphGeneralization.Hypergraph.graphLike_logical_in_kernel {V : Type u_1} {H : Type u_2} [DecidableEq V] [DecidableEq H] [Fintype V] [Fintype H] (HG : Hypergraph V H) (h_gl : HG.isGraphLike) : allOnesV ∈ HG.operatorKernel

In the graph case, the logical is always in the kernel (each edge has 2 vertices)

Summary

This formalization captures Remark 15 about the hypergraph generalization of gauging:

Definitions:

• Hypergraph: A hypergraph with vertices V and hyperedges H, each hyperedge is a set of vertices
• parityCheckMap: The sparse linear map H_Z : Z₂^V → Z₂^H whose kernel characterizes the abelian group of operators
• operatorKernel: The kernel of H_Z, representing the abelian group of commuting operators
• gaussLawVertexSupport/gaussLawHyperedgeSupport: X-type support vectors for A_v operators
• gaussLawZTypeSupport/gaussLawZTypeHyperedgeSupport: Z-type support (trivially zero for A_v)
• symplecticInnerProductV/symplecticInnerProductH: Symplectic inner product for commutativity

Key Results:

• gaussLaw_commute_hypergraph: A_v operators commute (symplectic inner product = 0)
• mem_operatorKernel_iff: x ∈ ker(H_Z) iff ∑_{v ∈ h} x_v = 0 for all hyperedges h
• kernel_is_abelian_group: The kernel characterizes commuting operators (x ∈ S ↔ H_Z(x) = 0)
• gaussLaw_vertex_support_sum_allOnes: Product of all A_v vertex parts gives L
• ofGraphWithCycles_isGraphLike: Ordinary graphs embed as graph-like hypergraphs
• kLocal_means_sparse_row: k-local checks correspond to sparse parity-check matrix
• logical_in_kernel_iff: L ∈ ker(H_Z) iff all hyperedges have even cardinality