Remark 17: Hypergraph Generalization

Statement

The gauging measurement procedure can be generalized by replacing the graph G with a hypergraph H = (V, E) where each hyperedge e ∈ E is a nonempty subset of vertices.

Setup:

• Introduce one auxiliary qubit per hyperedge.
• Gauss's law operators: A_v = X_v ∏_{e ∋ v} X_e.
• Boundary map ∂: Z₂^E → Z₂^V with (∂γ)v = Σ{e ∋ v} γ_e.

Key result: γ ∈ ker(∂) corresponds to the X-type operator ∏v X_v^{(Σ{e ∋ v} γ_e mod 2)} which commutes with all A_v. The hypergraph gauging measures any such operator.

Main Results

• hyperBoundaryMap : the boundary map ∂ for hypergraphs
• hyperGaussLawOp : hypergraph Gauss's law operator A_v
• hyperGaussLawOp_pure_X : A_v is pure X-type
• hyperGaussLaw_commute : all A_v mutually commute
• symplecticInner_pureZ_gaussLaw : ⟨Z(γ), A_v⟩ = (∂γ)_v
• ker_boundary_iff_commutes_all_gaussLaw : γ ∈ ker(∂) ↔ Z(γ) commutes with all A_v
• cssInit_boundary_eq : CSS initialization is a special case
• graphLike_boundary_single_sum : graph case recovered when hyperedges have 2 vertices

Hyperedge incidence

def HypergraphGeneralization.hyperIncidentEdges {V : Type u_1} {E : Type u_2} [Fintype E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (v : V) : Finset E

The finset of hyperedges incident to vertex v.

Equations

• HypergraphGeneralization.hyperIncidentEdges incident v = {e : E | incident v e}

@[simp]

theorem HypergraphGeneralization.mem_hyperIncidentEdges {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (v : V) (e : E) : e ∈ hyperIncidentEdges incident v ↔ incident v e

def HypergraphGeneralization.hyperedgeVertices {V : Type u_1} [Fintype V] {E : Type u_2} (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (e : E) : Finset V

The finset of vertices in hyperedge e.

Equations

• HypergraphGeneralization.hyperedgeVertices incident e = {v : V | incident v e}

@[simp]

theorem HypergraphGeneralization.mem_hyperedgeVertices {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (e : E) (v : V) : v ∈ hyperedgeVertices incident e ↔ incident v e

theorem HypergraphGeneralization.hyperedgeVertices_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (e : E) (hne : ∃ (v : V), incident v e) : (hyperedgeVertices incident e).Nonempty

Hypergraph Boundary Map

def HypergraphGeneralization.hyperBoundaryMap {V : Type u_1} {E : Type u_2} [Fintype E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] : (E → ZMod 2) →ₗ[ZMod 2] V → ZMod 2

The hypergraph boundary map ∂ : Z₂^E → Z₂^V. For γ ∈ Z₂^E, (∂γ)v = Σ{e ∋ v} γ_e (mod 2). This generalizes the graph boundary map: for graphs, each edge is incident to exactly 2 vertices; for hypergraphs, a hyperedge can be incident to any nonempty set of vertices.

Equations

• HypergraphGeneralization.hyperBoundaryMap incident = { toFun := fun (γ : E → ZMod 2) (v : V) => ∑ e : E, if incident v e then γ e else 0, map_add' := ⋯, map_smul' := ⋯ }

theorem HypergraphGeneralization.hyperBoundaryMap_apply {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (γ : E → ZMod 2) (v : V) : (hyperBoundaryMap incident) γ v = ∑ e : E, if incident v e then γ e else 0

theorem HypergraphGeneralization.hyperBoundaryMap_single {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (e₀ : E) (v : V) : (hyperBoundaryMap incident) (fun (e : E) => if e = e₀ then 1 else 0) v = if incident v e₀ then 1 else 0

The boundary of a single hyperedge indicator: (∂ 1_e)(v) = 1 iff v ∈ e.

Hypergraph Coboundary Map

def HypergraphGeneralization.hyperCoboundaryMap {V : Type u_1} [Fintype V] {E : Type u_2} (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] : (V → ZMod 2) →ₗ[ZMod 2] E → ZMod 2

The hypergraph coboundary map δ : Z₂^V → Z₂^E, the transpose of ∂. For f ∈ Z₂^V, (δf)e = Σ{v ∈ e} f_v (mod 2).

Equations

• HypergraphGeneralization.hyperCoboundaryMap incident = { toFun := fun (f : V → ZMod 2) (e : E) => ∑ v : V, if incident v e then f v else 0, map_add' := ⋯, map_smul' := ⋯ }

theorem HypergraphGeneralization.hyperCoboundaryMap_apply {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (f : V → ZMod 2) (e : E) : (hyperCoboundaryMap incident) f e = ∑ v : V, if incident v e then f v else 0

theorem HypergraphGeneralization.hyperCoboundaryMap_eq_transpose {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (f : V → ZMod 2) (γ : E → ZMod 2) : ∑ e : E, (hyperCoboundaryMap incident) f e * γ e = ∑ v : V, f v * (hyperBoundaryMap incident) γ v

δ is the transpose of ∂: ⟨δ f, γ⟩_E = ⟨f, ∂ γ⟩_V.

Extended Qubit Type

@[reducible, inline]

abbrev HypergraphGeneralization.HyperExtQubit {V : Type u_1} {E : Type u_2} : Type (max u_1 u_2)

The extended qubit type for hypergraph gauging: vertex qubits (Sum.inl v) and hyperedge qubits (Sum.inr e).

Equations

• HypergraphGeneralization.HyperExtQubit = (V ⊕ E)

Hypergraph Gauss's Law Operator

def HypergraphGeneralization.hyperGaussLawOp {V : Type u_1} [DecidableEq V] {E : Type u_2} (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (v : V) : PauliOp (V ⊕ E)

The hypergraph Gauss's law operator A_v on the extended system V ⊕ E. A_v = X_v ∏_{e ∋ v} X_e: acts with X on vertex qubit v and all incident hyperedge qubits.

Equations

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

@[simp]

theorem HypergraphGeneralization.hyperGaussLawOp_zVec {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (v : V) : (hyperGaussLawOp incident v).zVec = 0

A_v is pure X-type: its Z-vector is identically zero.

theorem HypergraphGeneralization.hyperGaussLawOp_pure_X {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (v : V) (q : V ⊕ E) : (hyperGaussLawOp incident v).zVec q = 0

A_v has no Z support.

@[simp]

theorem HypergraphGeneralization.hyperGaussLawOp_xVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (v w : V) : (hyperGaussLawOp incident v).xVec (Sum.inl w) = if w = v then 1 else 0

@[simp]

theorem HypergraphGeneralization.hyperGaussLawOp_xVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (v : V) (e : E) : (hyperGaussLawOp incident v).xVec (Sum.inr e) = if incident v e then 1 else 0

Commutation of Gauss's Law Operators

theorem HypergraphGeneralization.hyperGaussLaw_commute {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (v w : V) : (hyperGaussLawOp incident v).PauliCommute (hyperGaussLawOp incident w)

All hypergraph Gauss's law operators mutually commute. This holds because they are all pure X-type (zVec = 0).

The X-Type Operator from an Edge Vector

def HypergraphGeneralization.xOpFromBoundary {V : Type u_1} {E : Type u_2} [Fintype E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (γ : E → ZMod 2) : PauliOp V

Given an edge vector γ : E → ZMod 2, the corresponding X-type operator on vertex qubits: ∏_{v ∈ V} X_v^{(∂γ)_v}. Acts as X on vertex v iff (∂γ)_v = 1.

Equations

• HypergraphGeneralization.xOpFromBoundary incident γ = { xVec := (HypergraphGeneralization.hyperBoundaryMap incident) γ, zVec := 0 }

@[simp]

theorem HypergraphGeneralization.xOpFromBoundary_xVec {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (γ : E → ZMod 2) : (xOpFromBoundary incident γ).xVec = (hyperBoundaryMap incident) γ

@[simp]

theorem HypergraphGeneralization.xOpFromBoundary_zVec {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (γ : E → ZMod 2) : (xOpFromBoundary incident γ).zVec = 0

Product of Gauss's Law Operators

theorem HypergraphGeneralization.hyperGaussLaw_product_xVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (w : V) : ∑ v : V, (hyperGaussLawOp incident v).xVec (Sum.inl w) = 1

On vertex qubits: each vertex w gets contribution 1 from A_w only.

theorem HypergraphGeneralization.hyperGaussLaw_product_xVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (e : E) : ∑ v : V, (hyperGaussLawOp incident v).xVec (Sum.inr e) = ↑(hyperedgeVertices incident e).card

On edge qubits: each hyperedge e gets |vertices(e)| mod 2.

Kernel of Boundary Map and Commutation

theorem HypergraphGeneralization.mem_ker_hyperBoundary_iff {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (γ : E → ZMod 2) : γ ∈ (hyperBoundaryMap incident).ker ↔ ∀ (v : V), (hyperBoundaryMap incident) γ v = 0

γ ∈ ker(∂) iff the boundary is zero: (∂γ)_v = 0 for all v.

theorem HypergraphGeneralization.ker_boundary_gives_identity_on_V {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (γ : E → ZMod 2) (hγ : γ ∈ (hyperBoundaryMap incident).ker) : xOpFromBoundary incident γ = 1

The X-type operator on V from γ ∈ ker(∂) is the identity (since ∂γ = 0).

Gauss Subset Product

def HypergraphGeneralization.hyperGaussSubsetProduct {V : Type u_1} [Fintype V] {E : Type u_2} (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (c : V → ZMod 2) : PauliOp (V ⊕ E)

The Gauss subset product for hypergraphs: the product of A_v over vertices where c_v = 1. On vertex qubits, the X-vector is c; on edge qubits, it is δc.

Equations

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

@[simp]

theorem HypergraphGeneralization.hyperGaussSubsetProduct_xVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (c : V → ZMod 2) (w : V) : (hyperGaussSubsetProduct incident c).xVec (Sum.inl w) = c w

@[simp]

theorem HypergraphGeneralization.hyperGaussSubsetProduct_xVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (c : V → ZMod 2) (e : E) : (hyperGaussSubsetProduct incident c).xVec (Sum.inr e) = ∑ v : V, if incident v e then c v else 0

@[simp]

theorem HypergraphGeneralization.hyperGaussSubsetProduct_zVec {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (c : V → ZMod 2) : (hyperGaussSubsetProduct incident c).zVec = 0

theorem HypergraphGeneralization.hyperGaussSubsetProduct_allOnes_vertex {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (w : V) : (hyperGaussSubsetProduct incident fun (x : V) => 1).xVec (Sum.inl w) = 1

The Gauss subset product for the all-ones vector gives L = ∏_v X_v on vertices.

theorem HypergraphGeneralization.hyperGaussSubsetProduct_allOnes_edge {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (e : E) : (hyperGaussSubsetProduct incident fun (x : V) => 1).xVec (Sum.inr e) = ↑(hyperedgeVertices incident e).card

On edge qubits, the all-ones Gauss product gives |vertices(e)| mod 2.

@[simp]

theorem HypergraphGeneralization.hyperGaussSubsetProduct_zero {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] : hyperGaussSubsetProduct incident 0 = 1

The Gauss subset product for the zero vector gives the identity.

theorem HypergraphGeneralization.hyperGaussSubsetProduct_add {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (c₁ c₂ : V → ZMod 2) : hyperGaussSubsetProduct incident (c₁ + c₂) = hyperGaussSubsetProduct incident c₁ * hyperGaussSubsetProduct incident c₂

The Gauss subset product is additive.

theorem HypergraphGeneralization.hyperGaussSubsetProduct_edge_eq_coboundary {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (c : V → ZMod 2) (e : E) : (hyperGaussSubsetProduct incident c).xVec (Sum.inr e) = (hyperCoboundaryMap incident) c e

The edge X-vector of the Gauss subset product equals the coboundary.

Pure-Z Hyperedge Operator and Kernel Characterization

def HypergraphGeneralization.pureZHyperedgeOp {V : Type u_1} {E : Type u_2} (γ : E → ZMod 2) : PauliOp (V ⊕ E)

A pure-Z hyperedge operator: acts as Z on hyperedge qubit e iff γ(e) = 1.

Equations

• HypergraphGeneralization.pureZHyperedgeOp γ = { xVec := 0, zVec := fun (q : V ⊕ E) => match q with | Sum.inl val => 0 | Sum.inr e => γ e }

@[simp]

theorem HypergraphGeneralization.pureZHyperedgeOp_xVec {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (γ : E → ZMod 2) : (pureZHyperedgeOp γ).xVec = 0

@[simp]

theorem HypergraphGeneralization.pureZHyperedgeOp_zVec_vertex {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (γ : E → ZMod 2) (v : V) : (pureZHyperedgeOp γ).zVec (Sum.inl v) = 0

@[simp]

theorem HypergraphGeneralization.pureZHyperedgeOp_zVec_edge {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (γ : E → ZMod 2) (e : E) : (pureZHyperedgeOp γ).zVec (Sum.inr e) = γ e

theorem HypergraphGeneralization.symplecticInner_pureZ_gaussLaw {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (γ : E → ZMod 2) (v : V) : (pureZHyperedgeOp γ).symplecticInner (hyperGaussLawOp incident v) = (hyperBoundaryMap incident) γ v

The symplectic inner product of the pure-Z hyperedge operator for γ with A_v equals (∂γ)_v. This is the key computation connecting the boundary map to commutation with Gauss operators.

theorem HypergraphGeneralization.pureZHyperedgeOp_commutes_gaussLaw_iff {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (γ : E → ZMod 2) (v : V) : (pureZHyperedgeOp γ).PauliCommute (hyperGaussLawOp incident v) ↔ (hyperBoundaryMap incident) γ v = 0

Key theorem: The pure-Z hyperedge operator for γ commutes with A_v iff (∂γ)_v = 0.

theorem HypergraphGeneralization.ker_boundary_iff_commutes_all_gaussLaw {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (γ : E → ZMod 2) : γ ∈ (hyperBoundaryMap incident).ker ↔ ∀ (v : V), (pureZHyperedgeOp γ).PauliCommute (hyperGaussLawOp incident v)

γ ∈ ker(∂) iff the pure-Z hyperedge operator commutes with ALL Gauss operators.

theorem HypergraphGeneralization.commuting_pureZ_operators_eq_ker_image {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (P : PauliOp (V ⊕ E)) (hxVec : P.xVec = 0) (hzVertex : ∀ (v : V), P.zVec (Sum.inl v) = 0) (hcomm : ∀ (v : V), P.PauliCommute (hyperGaussLawOp incident v)) : (fun (e : E) => P.zVec (Sum.inr e)) ∈ (hyperBoundaryMap incident).ker

The set of pure-Z hyperedge operators commuting with all A_v is exactly the image of ker(∂): if P is pure-Z on edges, zero on vertices, and commutes with all A_v, then its edge Z-vector is in ker(∂).

Recovering the Graph Case

def HypergraphGeneralization.IsGraphLike {V : Type u_1} [Fintype V] {E : Type u_2} (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] : Prop

A hypergraph comes from a simple graph when each hyperedge has exactly 2 vertices.

Equations

• HypergraphGeneralization.IsGraphLike incident = ∀ (e : E), (HypergraphGeneralization.hyperedgeVertices incident e).card = 2

theorem HypergraphGeneralization.graphLike_boundary_single_sum {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (hgl : IsGraphLike incident) (e₀ : E) : ∑ v : V, (hyperBoundaryMap incident) (fun (e : E) => if e = e₀ then 1 else 0) v = 0

For a graph-like hypergraph, the boundary of a single edge sums to 0 over all vertices, because each edge has exactly 2 endpoints and 2 = 0 in ZMod 2.

CSS Code Initialization as a Special Case

theorem HypergraphGeneralization.cssInit_boundary_eq {Q : Type u_3} [Fintype Q] [DecidableEq Q] {I : Type u_4} [Fintype I] [DecidableEq I] (xCheckSupport : I → Finset Q) (γ : I → ZMod 2) (q : Q) : (hyperBoundaryMap fun (v : Q) (i : I) => v ∈ xCheckSupport i) γ q = ∑ i : I, if q ∈ xCheckSupport i then γ i else 0

For CSS code initialization, the incidence relation is membership in check supports.

• V = set of physical qubits (Q)
• E = set of X-type checks (I)
• incident q i iff qubit q participates in X-check i The boundary map then encodes the X-check parity matrix.

Summary Theorems

theorem HypergraphGeneralization.hypergraph_generalization_summary {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_2} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] : (∀ (v w : V), (hyperGaussLawOp incident v).PauliCommute (hyperGaussLawOp incident w)) ∧ (∀ (γ : E → ZMod 2), γ ∈ (hyperBoundaryMap incident).ker ↔ ∀ (v : V), (pureZHyperedgeOp γ).PauliCommute (hyperGaussLawOp incident v)) ∧ (∀ (f : V → ZMod 2) (γ : E → ZMod 2), ∑ e : E, (hyperCoboundaryMap incident) f e * γ e = ∑ v : V, f v * (hyperBoundaryMap incident) γ v) ∧ hyperGaussSubsetProduct incident 0 = 1

Summary: The hypergraph generalization extends the graph gauging framework.

1. All Gauss operators mutually commute (pure X-type)
2. Pure-Z edge operators commute with A_v iff γ ∈ ker(∂)
3. The coboundary δ is the transpose of ∂
4. The Gauss subset product is additive and encodes the vertex-edge duality