Documentation

QEC1.Definitions.Def_2_GaussLawOperators

Def_2: Gauss's Law Operators #

Statement #

Given a connected graph $G = (V_G, E_G)$ whose vertices are identified with the qubits in the support of a logical operator $L = \prod_{v \in V_G} X_v$, the Gauss's law operators are the set $\mathcal{A} = \{A_v\}_{v \in V_G}$ where: $$A_v = X_v \prod_{e \ni v} X_e$$ Here $X_v$ is the Pauli-$X$ operator on the vertex qubit $v$, and $X_e$ is the Pauli-$X$ operator on the edge qubit $e$. The product $\prod_{e \ni v}$ is over all edges incident to vertex $v$.

The Gauss's law operators satisfy:

  1. Each $A_v$ is Hermitian with eigenvalues $\pm 1$.
  2. All $A_v$ mutually commute: $[A_v, A_{v'}] = 0$ for all $v, v' \in V_G$.
  3. $\prod_{v \in V_G} A_v = L \cdot \prod_{e \in E_G} X_e^{2} = L$ (since $X_e^2 = I$).

This last property is the key to the gauging measurement: measuring all $A_v$ and multiplying the outcomes yields the eigenvalue of $L$.

Main Definitions #

Key Properties #

Corollaries #

Gauss Law Operator Support #

A Gauss law operator A_v is an X-type Pauli operator. We represent it by its support:

In the binary vector representation (Rem_3), the support encodes where X operators act.

def GraphWithCycles.gaussLawOperator_vertexSupport {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (_G : GraphWithCycles V E C) (v : V) :

The vertex support of Gauss law operator A_v: a binary vector with 1 at v, 0 elsewhere. This represents X_v in the product A_v = X_v ∏_{e∋v} X_e.

Equations
Instances For
    def GraphWithCycles.gaussLawOperator_edgeSupport {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v : V) :

    The edge support of Gauss law operator A_v: 1 at edges incident to v, 0 elsewhere. This represents ∏{e∋v} X_e in the product A_v = X_v ∏{e∋v} X_e.

    Equations
    Instances For

      Basic Properties of Gauss Law Operator Support #

      @[simp]
      theorem GraphWithCycles.gaussLawOperator_vertexSupport_ne {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v w : V) (h : v w) :
      @[simp]
      theorem GraphWithCycles.gaussLawOperator_edgeSupport_incident {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v : V) (e : E) (h : G.isIncident e v) :
      @[simp]
      theorem GraphWithCycles.gaussLawOperator_edgeSupport_not_incident {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v : V) (e : E) (h : ¬G.isIncident e v) :
      theorem GraphWithCycles.gaussLawOperator_edgeSupport_apply {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v : V) (e : E) :

      The edge support at an edge e

      Property 1: A_v² = I (Hermitian with eigenvalues ±1) #

      In the binary vector representation over ZMod 2:

      This implies A_v is Hermitian (since X† = X, products of X are Hermitian) and has eigenvalues ±1 (from A² = I, any eigenvalue λ satisfies λ² = 1).

      theorem GraphWithCycles.ZMod2_add_self (x : ZMod 2) :
      x + x = 0

      In ZMod 2, any element added to itself is 0

      A_v² = I on vertex support: support + support = 0 (in ZMod 2)

      A_v² = I on edge support: support + support = 0 (in ZMod 2)

      theorem GraphWithCycles.gaussLaw_hermitian {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v w : V) :

      Property 1: A_v is Hermitian with eigenvalues ±1. Represented by A_v² = I, which in ZMod 2 is: 2 • support = 0. If A|ψ⟩ = λ|ψ⟩ and A² = I, then λ² = 1, so λ ∈ {-1, +1}.

      Property 2: All A_v mutually commute #

      For Pauli operators, [A, B] = 0 iff the symplectic form ω(A, B) ≡ 0 (mod 2), where: ω(A, B) = |supp_X(A) ∩ supp_Z(B)| + |supp_Z(A) ∩ supp_X(B)|

      Since Gauss law operators are X-type (only X, no Z), they have:

      Therefore ω(A_v, A_w) = |supp_X(A_v) ∩ ∅| + |∅ ∩ supp_X(A_w)| = 0.

      def GraphWithCycles.gaussLaw_ZSupport_vertex {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (_G : GraphWithCycles V E C) (_v : V) :

      The Z-support of a Gauss law operator is empty (X-type operators have no Z component)

      Equations
      Instances For
        def GraphWithCycles.gaussLaw_ZSupport_edge {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (_G : GraphWithCycles V E C) (_v : V) :

        The Z-support on edges is also empty

        Equations
        Instances For
          def GraphWithCycles.gaussLaw_symplectic {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v w : V) :

          The symplectic form between two Gauss law operators. For X-type operators: ω(A_v, A_w) = |X_v ∩ Z_w| + |Z_v ∩ X_w| = 0 + 0 = 0

          Equations
          Instances For
            @[simp]
            @[simp]
            theorem GraphWithCycles.gaussLaw_symplectic_zero {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v w : V) :

            The symplectic form is zero for X-type operators

            theorem GraphWithCycles.gaussLaw_commute {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v w : V) :

            Property 2: Two Gauss law operators commute. [A_v, A_w] = 0 since ω(A_v, A_w) = 0 (X-type operators always commute).

            Property 3: ∏_{v ∈ V} A_v = L #

            The product of all Gauss law operators:

            Therefore ∏_v A_v = L (the logical operator with support on all vertices).

            Sum of all vertex supports: ∑_v (A_v vertex support)

            Equations
            Instances For

              Sum of all edge supports: ∑_v (A_v edge support)

              Equations
              Instances For

                Each vertex w appears in exactly one A_v (namely when v = w), so the sum at w is 1

                The product of all A_v has vertex support equal to the all-ones vector. This is the support of L = ∏_{v ∈ V} X_v.

                Each edge e is incident to exactly 2 vertices (its endpoints). In ZMod 2, 1 + 1 = 0, so edge contributions cancel.

                The product of all A_v has edge support equal to zero (edges cancel pairwise). This represents X_e² = I for each edge.

                Property 3: The product of all Gauss law operators equals L.

                • Vertex support: all 1s (= L = ∏_v X_v)
                • Edge support: all 0s (since X_e² = I, edge terms cancel)

                This is the key property: measuring all A_v and multiplying outcomes gives the eigenvalue of L.

                Relationship to Coboundary Map #

                The edge support of A_v equals δ(v) where δ is the coboundary map from Def_1. This connects Gauss law operators to the chain complex structure.

                The edge support of A_v equals the coboundary of the basis vector at v

                The sum of all edge supports equals the coboundary of the all-ones vector

                Group Structure: |V| - 1 Independent Generators #

                The Gauss law operators satisfy one constraint: ∏_v A_v = L. This means of the |V| generators, only |V| - 1 are independent. The abelian group generated by {A_v} has order 2^{|V|-1}.

                def GraphWithCycles.gaussLaw_generator_count {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (_G : GraphWithCycles V E C) :

                Number of Gauss law operators equals number of vertices

                Equations
                Instances For

                  Number of constraints among Gauss law operators (the single product constraint)

                  Equations
                  Instances For

                    Number of independent Gauss law generators = |V| - 1

                    Equations
                    Instances For

                      The independent count is |V| - 1

                      def GraphWithCycles.gaussLaw_group_order {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) :

                      The abelian group generated by {A_v} has order 2^{|V|-1}

                      Equations
                      Instances For
                        theorem GraphWithCycles.gaussLaw_constraint_equation {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (w : V) :

                        The constraint: sum of all generators (in ZMod 2) equals the all-ones vector

                        theorem GraphWithCycles.gaussLaw_linear_dependency {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) [Nonempty V] :
                        ∃ (v₀ : V), ∀ (w : V), G.gaussLawOperator_vertexSupport v₀ w = 1 - vFinset.univ.erase v₀, G.gaussLawOperator_vertexSupport v w

                        There exists a generator that is a linear combination of the others (linear dependency)

                        Support Size and Degree #

                        The support size of A_v is 1 + degree(v):

                        noncomputable def GraphWithCycles.vertexDegree {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v : V) :

                        The degree of vertex v in the graph

                        Equations
                        Instances For
                          theorem GraphWithCycles.gaussLawOperator_edgeSupport_size {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v : V) :

                          The support size of A_v on edge qubits equals the degree of v

                          noncomputable def GraphWithCycles.gaussLawOperator_totalSupport {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (G : GraphWithCycles V E C) (v : V) :

                          Total support size of A_v is 1 (vertex) + degree(v) (edges)

                          Equations
                          Instances For

                            Equivalence with Coboundary in Chain Complex #

                            The Gauss law operators are closely related to the coboundary map δ. Specifically, A_v has edge support δ(e_v) where e_v is the basis vector at v.

                            The Gauss law operator A_v corresponds to:

                            • Vertex support: e_v (basis vector at v)
                            • Edge support: δ(e_v) (coboundary of basis vector at v) This shows A_v = X_v · ∏_{e∋v} X_e in the binary vector representation.

                            Measurement Property #

                            The key property for the gauging measurement: Measuring all A_v and multiplying the outcomes (±1) gives the eigenvalue of L.

                            In our ZMod 2 representation:

                            Product of measurement outcomes as ZMod 2 sum

                            Equations
                            Instances For
                              theorem GraphWithCycles.gaussLaw_measurement_determines_L {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (_G : GraphWithCycles V E C) (outcomes : VGraphMeasurementOutcome) :
                              measurementProduct outcomes = 0 {v : V | measurementToZMod2 (outcomes v) = 1}.card % 2 = 0

                              The measurement of all A_v determines the eigenvalue of L. The XOR of all measurement outcomes (in ZMod 2) equals the L eigenvalue: 0 means L eigenvalue +1, 1 means L eigenvalue -1. Sum = 0 iff even number of -1 outcomes.

                              theorem GraphWithCycles.gaussLaw_all_plus_implies_L_plus {V : Type u_1} {E : Type u_2} {C : Type u_3} [DecidableEq V] [DecidableEq E] [DecidableEq C] [Fintype V] [Fintype E] [Fintype C] (_G : GraphWithCycles V E C) (outcomes : VGraphMeasurementOutcome) (h : ∀ (v : V), outcomes v = GraphMeasurementOutcome.plus) :

                              If all outcomes are +1, the product is 0 (L eigenvalue +1)

                              Summary #

                              The Gauss law operators formalize the key concept from the gauging measurement protocol:

                              1. Definition: A_v = X_v ∏_{e∋v} X_e represented as binary vectors over ZMod 2

                                • Vertex support: basis vector e_v (1 at v, 0 elsewhere)
                                • Edge support: coboundary δ(e_v) (1 at incident edges, 0 elsewhere)
                              2. Property 1 (Hermitian): A_v² = I

                                • In ZMod 2: support + support = 0
                                • Implies eigenvalues are ±1
                              3. Property 2 (Commutativity): [A_v, A_w] = 0 for all v, w

                                • X-type operators have zero symplectic form
                                • All Gauss law operators mutually commute
                              4. Property 3 (Product Constraint): ∏_v A_v = L

                                • Vertex support: all 1s (= support of L = ∏_v X_v)
                                • Edge support: 0 (edges cancel since each appears twice, and X² = I)
                              5. Group Structure: |V| generators with 1 constraint give |V|-1 independent generators

                                • The generated abelian group has order 2^{|V|-1}
                              6. Measurement: Multiplying all A_v outcomes gives the L eigenvalue

                                • Key to the gauging measurement protocol