Remark 23: Generalizations Beyond Pauli

Statement

The gauging measurement procedure (Def_5) generalizes beyond Pauli logical operators on qubits:

1. Non-Pauli operators: The procedure applies to any representation of a finite group by operators with tensor product factorization (including magic state production and Clifford operators in topological codes).

2. Qudit systems: Replace Z₂ with Z_p (or more general finite groups), using p-state qudits. The boundary/coboundary maps become Z_p-linear maps.

3. Nonabelian groups: The procedure generalizes to nonabelian symmetry groups, but measuring local charges no longer determines a definite global charge (the total charge can remain in superposition).

Main Results

• quditBoundaryMap : boundary map ∂ over Z_p generalizing Def_1
• quditCoboundaryMap : coboundary map δ over Z_p
• quditCoboundaryMap_eq_transpose : δ is the transpose of ∂ over Z_p
• quditBoundary_comp_secondBoundary_eq_zero : ∂ ∘ ∂₂ = 0 over Z_p
• abelian_charge_sum_well_defined : sum of local charges is order-independent
• nonabelian_product_order_dependent : product of noncommuting elements is order-dependent

Corollaries

• quditBoundaryMap_specializes_to_qubit : Z_p maps reduce to Z₂ maps when p = 2
• qudit_range_secondBoundary_le_ker_boundary : im(∂₂) ≤ ker(∂) over Z_p
• abelian_local_determines_global : local abelian charges determine global charge
• nonabelian_local_underdetermines_global : local nonabelian measurements leave ambiguity

1. Qudit Generalization: Boundary Maps over Z_p

def GeneralizationsBeyondPauli.quditBoundaryMap {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] (p : ℕ) : (↑G.edgeSet → ZMod p) →ₗ[ZMod p] V → ZMod p

The qudit boundary map ∂ : Z_p^E → Z_p^V, generalizing Def_1 from Z₂ to Z_p. For γ ∈ Z_p^E, (∂γ)v = Σ{e ∋ v} γ_e (mod p).

Equations

• GeneralizationsBeyondPauli.quditBoundaryMap G p = { toFun := fun (γ : ↑G.edgeSet → ZMod p) (v : V) => ∑ e : ↑G.edgeSet, if v ∈ ↑e then γ e else 0, map_add' := ⋯, map_smul' := ⋯ }

def GeneralizationsBeyondPauli.quditCoboundaryMap {V : Type u_1} (G : SimpleGraph V) (p : ℕ) : (V → ZMod p) →ₗ[ZMod p] ↑G.edgeSet → ZMod p

The qudit coboundary map δ : Z_p^V → Z_p^E, generalizing Def_1 from Z₂ to Z_p. For f ∈ Z_p^V and edge e = {a,b}, (δ f)_e = f(a) + f(b) (mod p).

Equations

• GeneralizationsBeyondPauli.quditCoboundaryMap G p = { toFun := fun (f : V → ZMod p) (e : ↑G.edgeSet) => Sym2.lift ⟨fun (a b : V) => f a + f b, ⋯⟩ ↑e, map_add' := ⋯, map_smul' := ⋯ }

def GeneralizationsBeyondPauli.quditSecondBoundaryMap {V : Type u_1} (G : SimpleGraph V) {C : Type u_2} [Fintype C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (p : ℕ) : (C → ZMod p) →ₗ[ZMod p] ↑G.edgeSet → ZMod p

The qudit second boundary map ∂₂ : Z_p^C → Z_p^E, generalizing Def_1 from Z₂ to Z_p.

Equations

• GeneralizationsBeyondPauli.quditSecondBoundaryMap G cycles p = { toFun := fun (σ : C → ZMod p) (e : ↑G.edgeSet) => ∑ c : C, if e ∈ cycles c then σ c else 0, map_add' := ⋯, map_smul' := ⋯ }

def GeneralizationsBeyondPauli.quditSecondCoboundaryMap {V : Type u_1} (G : SimpleGraph V) [Fintype ↑G.edgeSet] {C : Type u_2} (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (p : ℕ) : (↑G.edgeSet → ZMod p) →ₗ[ZMod p] C → ZMod p

The qudit second coboundary map δ₂ : Z_p^E → Z_p^C, generalizing Def_1 from Z₂ to Z_p.

Equations

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

Transpose properties

theorem GeneralizationsBeyondPauli.quditCoboundaryMap_eq_transpose {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (p : ℕ) [NeZero p] (f : V → ZMod p) (γ : ↑G.edgeSet → ZMod p) : ∑ e : ↑G.edgeSet, (quditCoboundaryMap G p) f e * γ e = ∑ v : V, f v * (quditBoundaryMap G p) γ v

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

theorem GeneralizationsBeyondPauli.quditSecondCoboundaryMap_eq_transpose {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (p : ℕ) [NeZero p] (γ : ↑G.edgeSet → ZMod p) (σ : C → ZMod p) : ∑ c : C, (quditSecondCoboundaryMap G cycles p) γ c * σ c = ∑ e : ↑G.edgeSet, γ e * (quditSecondBoundaryMap G cycles p) σ e

δ₂ is the transpose of ∂₂ over Z_p: ⟨δ₂γ, σ⟩_C = ⟨γ, ∂₂σ⟩_E.

Chain complex property: ∂ ∘ ∂₂ = 0 over Z_p

theorem GeneralizationsBeyondPauli.quditBoundary_comp_secondBoundary_eq_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (p : ℕ) [NeZero p] (hcyc : ∀ (c : C) (v : V), p ∣ {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) : quditBoundaryMap G p ∘ₗ quditSecondBoundaryMap G cycles p = 0

The chain complex property ∂ ∘ ∂₂ = 0 holds over Z_p, provided each cycle has the property that the number of edges incident to each vertex is divisible by p. Over Z₂, this is the standard cycle condition (even incidence). Over Z_p for odd p, this requires p | (incidence count), which holds for oriented cycles where ∂e = head(e) - tail(e) (each vertex sees +1 and -1, canceling).

theorem GeneralizationsBeyondPauli.qudit_range_secondBoundary_le_ker_boundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (p : ℕ) [NeZero p] (hcyc : ∀ (c : C) (v : V), p ∣ {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) : (quditSecondBoundaryMap G cycles p).range ≤ (quditBoundaryMap G p).ker

im(∂₂) ≤ ker(∂) over Z_p (consequence of ∂ ∘ ∂₂ = 0).

Specialization: Z_p maps reduce to Z₂ maps when p = 2

theorem GeneralizationsBeyondPauli.quditBoundaryMap_specializes_to_qubit {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (γ : ↑G.edgeSet → ZMod 2) (v : V) : (quditBoundaryMap G 2) γ v = (GraphMaps.boundaryMap G) γ v

The qudit boundary map at p = 2 agrees with the standard Z₂ boundary map from Def_1.

theorem GeneralizationsBeyondPauli.quditCoboundaryMap_specializes_to_qubit {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (f : V → ZMod 2) (e : ↑G.edgeSet) : (quditCoboundaryMap G 2) f e = (GraphMaps.coboundaryMap G) f e

The qudit coboundary map at p = 2 agrees with the standard Z₂ coboundary map from Def_1.

theorem GeneralizationsBeyondPauli.quditSecondBoundaryMap_specializes_to_qubit {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (σ : C → ZMod 2) (e : ↑G.edgeSet) : (quditSecondBoundaryMap G cycles 2) σ e = (GraphMaps.secondBoundaryMap G cycles) σ e

The qudit second boundary map at p = 2 agrees with the standard Z₂ second boundary map.

theorem GeneralizationsBeyondPauli.quditSecondCoboundaryMap_specializes_to_qubit {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (γ : ↑G.edgeSet → ZMod 2) (c : C) : (quditSecondCoboundaryMap G cycles 2) γ c = (GraphMaps.secondCoboundaryMap G cycles) γ c

The qudit second coboundary map at p = 2 agrees with the standard Z₂ second coboundary map.

Qudit boundary map basic properties

@[simp]

theorem GeneralizationsBeyondPauli.quditBoundaryMap_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (p : ℕ) [NeZero p] (v : V) : (quditBoundaryMap G p) 0 v = 0

@[simp]

theorem GeneralizationsBeyondPauli.quditCoboundaryMap_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (p : ℕ) [NeZero p] (e : ↑G.edgeSet) : (quditCoboundaryMap G p) 0 e = 0

@[simp]

theorem GeneralizationsBeyondPauli.quditSecondBoundaryMap_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (p : ℕ) [NeZero p] (e : ↑G.edgeSet) : (quditSecondBoundaryMap G cycles p) 0 e = 0

@[simp]

theorem GeneralizationsBeyondPauli.quditSecondCoboundaryMap_zero {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] {C : Type u_2} [Fintype C] [DecidableEq C] (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (p : ℕ) [NeZero p] (c : C) : (quditSecondCoboundaryMap G cycles p) 0 c = 0

theorem GeneralizationsBeyondPauli.quditBoundaryMap_add {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (p : ℕ) [NeZero p] (γ₁ γ₂ : ↑G.edgeSet → ZMod p) : (quditBoundaryMap G p) (γ₁ + γ₂) = (quditBoundaryMap G p) γ₁ + (quditBoundaryMap G p) γ₂

The qudit boundary map is Z_p-linear: it maps sums to sums.

theorem GeneralizationsBeyondPauli.quditCoboundaryMap_add {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (p : ℕ) [NeZero p] (f₁ f₂ : V → ZMod p) : (quditCoboundaryMap G p) (f₁ + f₂) = (quditCoboundaryMap G p) f₁ + (quditCoboundaryMap G p) f₂

The qudit coboundary map is Z_p-linear: it maps sums to sums.

2. Abelian Group Charge Determination

theorem GeneralizationsBeyondPauli.abelian_charge_sum_well_defined {α : Type u_3} [AddCommMonoid α] {n : ℕ} (charges : Fin n → α) (perm : Equiv.Perm (Fin n)) : ∑ i : Fin n, charges (perm i) = ∑ i : Fin n, charges i

For an abelian group, the sum of local charges is independent of the ordering. This is the core mathematical fact that makes abelian gauging work: measuring individual A_v operators in any order gives the same total charge σ = Σ_v ε_v, because addition is commutative.

theorem GeneralizationsBeyondPauli.abelian_sum_perm_invariant {α : Type u_3} [AddCommMonoid α] {ι : Type u_4} [Fintype ι] (charges : ι → α) (perm : Equiv.Perm ι) : ∑ i : ι, charges (perm i) = ∑ i : ι, charges i

For abelian groups, the sum over any fintype is permutation-invariant. This generalizes to arbitrary index types.

theorem GeneralizationsBeyondPauli.abelian_local_determines_global {α : Type u_3} [AddCommMonoid α] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (charges : ι → α) (σ₁ σ₂ : Equiv.Perm ι) : ∑ i : ι, charges (σ₁ i) = ∑ i : ι, charges (σ₂ i)

For abelian groups, the sum over a fintype is independent of the enumeration. This is why measuring Gauss's law operators A_v in any order gives the same total sign σ = Σ_v ε_v ∈ Z_p.

3. Nonabelian Groups: Product Order Dependence

For nonabelian groups, Finset.prod (= ∏) requires CommMonoid, which nonabelian groups do not satisfy. We instead use List.prod (which only requires Monoid) to express ordered products, making the order-dependence manifest.

theorem GeneralizationsBeyondPauli.nonabelian_product_order_dependent {G : Type u_3} [Group G] (g₁ g₂ : G) (hne : g₁ * g₂ ≠ g₂ * g₁) : [g₁, g₂].prod ≠ [g₂, g₁].prod

For nonabelian groups, the product of elements depends on the order of multiplication. If g₁ * g₂ ≠ g₂ * g₁, then the two orderings [g₁, g₂] and [g₂, g₁] give different products. This is the fundamental obstruction to measuring nonabelian charges locally.

theorem GeneralizationsBeyondPauli.abelian_product_perm_invariant {G : Type u_3} [CommMonoid G] (l₁ l₂ : List G) (hp : l₁.Perm l₂) : l₁.prod = l₂.prod

For a commutative (abelian) monoid, the product of any list is invariant under permutation. This is the positive direction: abelian gauging works because local measurements determine the global charge.

theorem GeneralizationsBeyondPauli.abelian_fintype_prod_perm_invariant {G : Type u_3} [CommMonoid G] {ι : Type u_4} [Fintype ι] (elements : ι → G) (σ : Equiv.Perm ι) : ∏ i : ι, elements (σ i) = ∏ i : ι, elements i

For a commutative monoid, all permutations of a finite sequence give the same product.

theorem GeneralizationsBeyondPauli.abelian_all_perms_same_product {G : Type u_3} [CommMonoid G] {ι : Type u_4} [Fintype ι] (elements : ι → G) (σ₁ σ₂ : Equiv.Perm ι) : ∏ i : ι, elements (σ₁ i) = ∏ i : ι, elements (σ₂ i)

For a commutative monoid, ALL permutations give the same product.

4. Qudit Gauss's Law Operators (Generalized)

def GeneralizationsBeyondPauli.quditHyperBoundaryMap {V : Type u_1} {E : Type u_3} [Fintype E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (p : ℕ) [NeZero p] : (E → ZMod p) →ₗ[ZMod p] V → ZMod p

The qudit boundary map for a hypergraph over Z_p, generalizing both the graph case (Def_1) and the hypergraph case (Rem_17) from Z₂ to Z_p.

Equations

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

def GeneralizationsBeyondPauli.quditHyperCoboundaryMap {V : Type u_1} [Fintype V] {E : Type u_3} (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (p : ℕ) [NeZero p] : (V → ZMod p) →ₗ[ZMod p] E → ZMod p

The qudit coboundary map for a hypergraph over Z_p.

Equations

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

theorem GeneralizationsBeyondPauli.quditHyperCoboundaryMap_eq_transpose {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_3} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (p : ℕ) [NeZero p] (f : V → ZMod p) (γ : E → ZMod p) : ∑ e : E, (quditHyperCoboundaryMap incident p) f e * γ e = ∑ v : V, f v * (quditHyperBoundaryMap incident p) γ v

The qudit hypergraph coboundary is the transpose of the boundary over Z_p.

theorem GeneralizationsBeyondPauli.quditHyperBoundaryMap_specializes_to_Z2 {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_3} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (γ : E → ZMod 2) (v : V) : (quditHyperBoundaryMap incident 2) γ v = (HypergraphGeneralization.hyperBoundaryMap incident) γ v

The qudit hypergraph boundary map at p = 2 agrees with the Z₂ version from Rem_17.

theorem GeneralizationsBeyondPauli.quditHyperCoboundaryMap_specializes_to_Z2 {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_3} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (f : V → ZMod 2) (e : E) : (quditHyperCoboundaryMap incident 2) f e = (HypergraphGeneralization.hyperCoboundaryMap incident) f e

The qudit hypergraph coboundary map at p = 2 agrees with the Z₂ version from Rem_17.

@[simp]

theorem GeneralizationsBeyondPauli.quditHyperBoundaryMap_zero {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_3} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (p : ℕ) [NeZero p] (v : V) : (quditHyperBoundaryMap incident p) 0 v = 0

@[simp]

theorem GeneralizationsBeyondPauli.quditHyperCoboundaryMap_zero {V : Type u_1} [Fintype V] [DecidableEq V] {E : Type u_3} [Fintype E] [DecidableEq E] (incident : V → E → Prop) [(v : V) → (e : E) → Decidable (incident v e)] (p : ℕ) [NeZero p] (e : E) : (quditHyperCoboundaryMap incident p) 0 e = 0

5. Nonabelian Local vs Global Charge

theorem GeneralizationsBeyondPauli.nonabelian_local_underdetermines_global {G : Type u_3} [Group G] (g₁ g₂ : G) (hne : g₁ * g₂ ≠ g₂ * g₁) : ¬∀ (l₁ l₂ : List G), l₁.Perm l₂ → l₁.prod = l₂.prod

Nonabelian local underdetermines global: In a nonabelian group, knowing the individual elements g_v does NOT determine their product uniquely, because the product depends on the order of multiplication. For any two noncommuting elements, the two orderings produce different products. This is the formal content of the paper's caveat about nonabelian gauging.

theorem GeneralizationsBeyondPauli.abelian_local_determines_global' {G : Type u_3} [CommMonoid G] (l₁ l₂ : List G) (hp : l₁.Perm l₂) : l₁.prod = l₂.prod

Abelian local determines global: In a commutative group, the product of elements is uniquely determined regardless of ordering. This is why abelian gauging works.

theorem GeneralizationsBeyondPauli.charge_dichotomy_iff_comm {G : Type u_3} [Group G] : (∀ (g₁ g₂ : G), [g₁, g₂].prod = [g₂, g₁].prod) ↔ ∀ (g₁ g₂ : G), g₁ * g₂ = g₂ * g₁

The abelian-nonabelian dichotomy: a group has the property that all 2-element ordered products are the same iff it is commutative.

6. Summary

theorem GeneralizationsBeyondPauli.generalizations_beyond_pauli_summary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : (∀ (p : ℕ) [NeZero p] (f : V → ZMod p) (γ : ↑G.edgeSet → ZMod p), ∑ e : ↑G.edgeSet, (quditCoboundaryMap G p) f e * γ e = ∑ v : V, f v * (quditBoundaryMap G p) γ v) ∧ (∀ (γ : ↑G.edgeSet → ZMod 2) (v : V), (quditBoundaryMap G 2) γ v = (GraphMaps.boundaryMap G) γ v) ∧ (∀ {α : Type u_3} [inst : AddCommMonoid α] {n : ℕ} (charges : Fin n → α) (perm : Equiv.Perm (Fin n)), ∑ i : Fin n, charges (perm i) = ∑ i : Fin n, charges i) ∧ ∀ {G : Type u_4} [inst : Group G] (g₁ g₂ : G), g₁ * g₂ ≠ g₂ * g₁ → [g₁, g₂].prod ≠ [g₂, g₁].prod

Summary theorem: The three generalizations beyond Pauli operators on qubits.

1. Qudit: Boundary/coboundary maps generalize from Z₂ to Z_p, preserving linearity and the transpose property. The chain complex property ∂ ∘ ∂₂ = 0 still holds.

2. Abelian: For abelian groups, the sum/product of local charges is order-independent, so measuring local charges determines the global charge.

3. Nonabelian: For nonabelian groups, the product of local charges depends on the order, so local measurements do NOT determine a definite global charge.