Definition 2: Gauss's Law and Flux Operators

Statement

Given a graph G = (V, E) and a collection of cycles C, we define Pauli operators on the extended qubit system V ⊕ E (vertex qubits + edge qubits):

1. Gauss's law operator A_v = X_v ∏_{e ∋ v} X_e for each vertex v ∈ V
2. Flux operator B_p = ∏_{e ∈ p} Z_e for each cycle p ∈ C

Main Results

• gaussLawOp : the Gauss's law operator A_v
• fluxOp : the flux operator B_p
• gaussLawOp_is_pure_X : A_v is pure X-type (zVec = 0)
• fluxOp_is_pure_Z : B_p is pure Z-type (xVec = 0)
• gaussLaw_commute : [A_v, A_v'] = 0
• flux_commute : [B_p, B_p'] = 0
• gauss_flux_commute : [A_v, B_p] = 0
• gaussLaw_product : ∏v A_v = L = ∏{v ∈ V} X_v (the logical operator)

Corollaries

• Support characterization lemmas
• X-support and Z-support computations

Extended qubit type: V ⊕ G.edgeSet

@[reducible, inline]

abbrev GaussFlux.ExtQubit {V : Type u_1} (G : SimpleGraph V) : Type u_1

The extended qubit type: vertex qubits (Sum.inl v) and edge qubits (Sum.inr e).

Equations

• GaussFlux.ExtQubit G = (V ⊕ ↑G.edgeSet)

instance GaussFlux.instFintypeExtQubit {V : Type u_1} [Fintype V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] : Fintype (ExtQubit G)

Equations

• GaussFlux.instFintypeExtQubit G = inferInstanceAs (Fintype (V ⊕ ↑G.edgeSet))

instance GaussFlux.instDecidableEqExtQubit {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) : DecidableEq (ExtQubit G)

Equations

• GaussFlux.instDecidableEqExtQubit G = inferInstanceAs (DecidableEq (V ⊕ ↑G.edgeSet))

Incident edges

noncomputable def GaussFlux.incidentEdges {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [Fintype ↑G.edgeSet] (v : V) : Finset ↑G.edgeSet

The finset of edges incident to vertex v.

Equations

• GaussFlux.incidentEdges G v = {e : ↑G.edgeSet | v ∈ ↑e}

@[simp]

theorem GaussFlux.mem_incidentEdges {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) (e : ↑G.edgeSet) : e ∈ incidentEdges G v ↔ v ∈ ↑e

Gauss's Law Operator

def GaussFlux.gaussLawOp {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) (v : V) : PauliOp (ExtQubit G)

The 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 edge qubits.

Equations

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

@[simp]

theorem GaussFlux.gaussLawOp_zVec {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : (gaussLawOp G v).zVec = 0

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

Flux Operator

def GaussFlux.fluxOp {V : Type u_1} (G : SimpleGraph V) {C : Type u_2} (cycles : C → Set ↑G.edgeSet) [(c : C) → DecidablePred fun (x : ↑G.edgeSet) => x ∈ cycles c] (p : C) : PauliOp (ExtQubit G)

The flux operator B_p on the extended system V ⊕ E. B_p = ∏_{e ∈ p} Z_e: acts with Z on all edge qubits in cycle p.

Equations

• GaussFlux.fluxOp G cycles p = { xVec := 0, zVec := fun (q : GaussFlux.ExtQubit G) => match q with | Sum.inl val => 0 | Sum.inr e => if e ∈ cycles p then 1 else 0 }

@[simp]

theorem GaussFlux.fluxOp_xVec {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 : C) : (fluxOp G cycles p).xVec = 0

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

Pure X-type / Z-type Properties

theorem GaussFlux.gaussLawOp_is_pure_X {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : (gaussLawOp G v).supportZ = ∅

A_v is pure X-type: it has no Z support.

theorem GaussFlux.fluxOp_is_pure_Z {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 : C) : (fluxOp G cycles p).supportX = ∅

B_p is pure Z-type: it has no X support.

Commutation: Gauss operators mutually commute

theorem GaussFlux.gaussLaw_commute {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v w : V) : (gaussLawOp G v).PauliCommute (gaussLawOp G w)

All Gauss's law operators mutually commute: [A_v, A_w] = 0. This holds because they are all pure X-type.

Commutation: Flux operators mutually commute

theorem GaussFlux.flux_commute {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 q : C) : (fluxOp G cycles p).PauliCommute (fluxOp G cycles q)

All flux operators mutually commute: [B_p, B_q] = 0. This holds because they are all pure Z-type.

Commutation: Gauss and flux operators commute

noncomputable def GaussFlux.cycleIncidentCount {V : Type u_1} [DecidableEq V] (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] (v : V) (p : C) : ℕ

The number of edges in cycle p that are incident to vertex v. For a cycle, this is always even (0 or 2).

Equations

• GaussFlux.cycleIncidentCount G cycles v p = {e : ↑G.edgeSet | e ∈ cycles p ∧ v ∈ ↑e}.card

theorem GaussFlux.gauss_flux_commute {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] (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) (v : V) (p : C) : (gaussLawOp G v).PauliCommute (fluxOp G cycles p)

Gauss's law operators commute with flux operators: [A_v, B_p] = 0. This holds because the symplectic inner product counts the overlap of X-support(A_v) with Z-support(B_p), which equals the number of edges in p incident to v. For a valid cycle, this is always even.

X-support characterization

theorem GaussFlux.gaussLawOp_supportX_vertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v w : V) : Sum.inl w ∈ (gaussLawOp G v).supportX ↔ w = v

The X-support of A_v on vertex qubits is {v}.

theorem GaussFlux.gaussLawOp_supportX_edge {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) (e : ↑G.edgeSet) : Sum.inr e ∈ (gaussLawOp G v).supportX ↔ v ∈ ↑e

The X-support of A_v on edge qubits is the set of incident edges.

theorem GaussFlux.fluxOp_supportZ_edge {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 : C) (e : ↑G.edgeSet) : Sum.inr e ∈ (fluxOp G cycles p).supportZ ↔ e ∈ cycles p

The Z-support of B_p on edge qubits is the set of edges in the cycle.

theorem GaussFlux.fluxOp_supportZ_vertex {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 : C) (w : V) : Sum.inl w ∉ (fluxOp G cycles p).supportZ

The Z-support of B_p on vertex qubits is empty.

Gauss Product Property

def GaussFlux.logicalOp {V : Type u_1} (G : SimpleGraph V) : PauliOp (ExtQubit G)

The logical operator L = ∏_{v ∈ V} X_v on the extended system: acts X on all vertex qubits and I on all edge qubits.

Equations

• GaussFlux.logicalOp G = { xVec := fun (q : GaussFlux.ExtQubit G) => match q with | Sum.inl val => 1 | Sum.inr val => 0, zVec := 0 }

theorem GaussFlux.gaussLaw_product_xVec_inl {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) : ∑ w : V, (gaussLawOp G w).xVec (Sum.inl v) = 1

Helper: The product of Gauss's law operators is computed pointwise as the sum of their x-vectors in ZMod 2. On vertex qubits, each vertex v contributes 1 exactly once (from A_v). On edge qubits, each edge e = {a,b} contributes 1 from A_a and 1 from A_b, so the sum is 0 (mod 2).

theorem GaussFlux.gaussLaw_product_xVec_inr {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (e : ↑G.edgeSet) : ∑ v : V, (gaussLawOp G v).xVec (Sum.inr e) = 0

theorem GaussFlux.gaussLaw_product {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : ∏ v : V, gaussLawOp G v = logicalOp G

Gauss product property (clean version): ∏_{v ∈ V} A_v = L, the logical X operator on all vertices. Each vertex gets X exactly once; each edge gets X² = I.

Logical operator is pure X-type

@[simp]

theorem GaussFlux.logicalOp_is_pure_X {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] : (logicalOp G).supportZ = ∅

The logical operator L is pure X-type.

Commutation of logical with flux

theorem GaussFlux.logical_flux_commute {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 : C) : (logicalOp G).PauliCommute (fluxOp G cycles p)

The logical operator commutes with all flux operators.

Summary: All Commutation Relations

theorem GaussFlux.all_commutation_relations {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] (hcyc : ∀ (c : C) (v : V), Even {e : ↑G.edgeSet | e ∈ cycles c ∧ v ∈ ↑e}.card) : (∀ (v w : V), (gaussLawOp G v).PauliCommute (gaussLawOp G w)) ∧ (∀ (p q : C), (fluxOp G cycles p).PauliCommute (fluxOp G cycles q)) ∧ ∀ (v : V) (p : C), (gaussLawOp G v).PauliCommute (fluxOp G cycles p)

All three commutation relations hold simultaneously: (i) [A_v, A_w] = 0 for all v, w ∈ V (ii) [B_p, B_q] = 0 for all p, q ∈ C (iii) [A_v, B_p] = 0 for all v ∈ V, p ∈ C

Relationship to Boundary Maps

theorem GaussFlux.gaussLawOp_xVec_edge_eq_coboundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [Fintype ↑G.edgeSet] (v : V) (e : ↑G.edgeSet) : (gaussLawOp G v).xVec (Sum.inr e) = (GraphMaps.coboundaryMap G) (Pi.single v 1) e

The Gauss's law operator A_v has X-support related to the coboundary map: the X-support on edges is exactly the set of edges incident to v, which is described by δ(1_v) in the boundary map formalism.

theorem GaussFlux.fluxOp_zVec_edge_eq_secondBoundary {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 : C) (e : ↑G.edgeSet) : (fluxOp G cycles p).zVec (Sum.inr e) = (GraphMaps.secondBoundaryMap G cycles) (Pi.single p 1) e

The flux operator B_p has Z-support related to the second boundary map: the Z-support on edges is exactly the set of edges in cycle p, which is described by ∂₂(1_p) in the boundary map formalism.