Documentation

QEC1.Definitions.Def_3_FluxOperators

Def_3: Flux Operators #

Statement #

Given a connected graph $G = (V_G, E_G)$ with a generating set of cycles $\{p\}_C$ (where $C = |E_G| - |V_G| + 1$ is the number of independent cycles by Euler's formula for connected graphs), the flux operators are the set $\mathcal{B} = \{B_p\}_{p \in C}$ where: $$B_p = \prod_{e \in p} Z_e$$ Here $Z_e$ is the Pauli-$Z$ operator on the edge qubit $e$, and the product is over all edges $e$ that belong to cycle $p$.

The flux operators arise from the initial state $|0\rangle^{\otimes E_G}$ of the edge qubits:

  1. Initially, $Z_e |0\rangle_e = |0\rangle_e$ for each edge, so each $Z_e$ is a stabilizer.
  2. After measuring the Gauss's law operators $A_v$ (which involve $X_e$ terms), individual $Z_e$ operators are no longer stabilizers.
  3. However, products $B_p = \prod_{e \in p} Z_e$ over cycles remain stabilizers because they commute with all $A_v$: $[B_p, A_v] = 0$ for all $p, v$.

To verify: $B_p$ and $A_v$ commute because the number of edges in cycle $p$ incident to vertex $v$ is always even (either 0 or 2), so the number of anticommuting $X_e$-$Z_e$ pairs is even.

Main Definitions #

Key Properties #

Corollaries #

Flux Operator Support #

A flux operator B_p is a Z-type Pauli operator. We represent it by its support:

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

Euler's Formula for Connected Graphs #

For a connected graph with |V| vertices and |E| edges, the number of independent cycles (first Betti number / cyclomatic number) is C = |E| - |V| + 1.

This is a consequence of Euler's formula: V - E + F = 2 for planar graphs, where F includes the outer face. For general connected graphs, it follows from spanning tree arguments: a spanning tree has |V| - 1 edges, so there are |E| - (|V| - 1) = |E| - |V| + 1 edges outside the spanning tree, each creating one independent cycle.

The number of independent cycles in a connected graph according to Euler's formula. For a connected graph: C = |E| - |V| + 1. We represent this as an integer to handle the subtraction correctly.

Equations
Instances For
    def GraphWithCycles.fluxOperator_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) (_p : C) :

    The vertex support of flux operator B_p: zero everywhere. B_p is a Z-type operator and has no X component on vertices.

    Equations
    Instances For
      def GraphWithCycles.fluxOperator_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) (p : C) :

      The edge support of flux operator B_p: 1 at edges in cycle p, 0 elsewhere. This represents B_p = ∏_{e ∈ p} Z_e.

      Equations
      Instances For

        Basic Properties of Flux Operator Support #

        @[simp]
        theorem GraphWithCycles.fluxOperator_vertexSupport_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) (p : C) (v : V) :
        @[simp]
        theorem GraphWithCycles.fluxOperator_edgeSupport_in_cycle {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) (p : C) (e : E) (h : e G.cycles p) :
        @[simp]
        theorem GraphWithCycles.fluxOperator_edgeSupport_not_in_cycle {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) (p : C) (e : E) (h : eG.cycles p) :
        theorem GraphWithCycles.fluxOperator_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) (p : C) (e : E) :

        The edge support at an edge e

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

        In the binary vector representation over ZMod 2:

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

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

        theorem GraphWithCycles.flux_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) (p : C) (e : E) :

        Property 1: B_p is Hermitian with eigenvalues ±1. Represented by B_p² = I, which in ZMod 2 is: 2 • support = 0.

        Property 2: All B_p 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 flux operators are Z-type (only Z, no X), they have:

        Therefore ω(B_p, B_q) = |∅ ∩ supp_Z(B_q)| + |supp_Z(B_p) ∩ ∅| = 0.

        def GraphWithCycles.flux_XSupport_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) (_p : C) :

        The X-support of a flux operator on vertices is empty (Z-type operators have no X component)

        Equations
        Instances For
          def GraphWithCycles.flux_XSupport_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) (_p : C) :

          The X-support on edges is also empty

          Equations
          Instances For
            def GraphWithCycles.flux_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) (p q : C) :

            The symplectic form between two flux operators. For Z-type operators: ω(B_p, B_q) = |X_p ∩ Z_q| + |Z_p ∩ X_q| = 0 + 0 = 0

            Equations
            Instances For
              @[simp]
              theorem GraphWithCycles.flux_XSupport_vertex_empty {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) (p : C) :
              @[simp]
              theorem GraphWithCycles.flux_XSupport_edge_empty {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) (p : C) :
              theorem GraphWithCycles.flux_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) (p q : C) :

              The symplectic form is zero for Z-type operators

              theorem GraphWithCycles.flux_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) (p q : C) :
              G.flux_symplectic p q % 2 = 0

              Property 2: Two flux operators commute. [B_p, B_q] = 0 since ω(B_p, B_q) = 0 (Z-type operators always commute).

              Key Property: Flux Operators Commute with Gauss Law Operators #

              For B_p and A_v to commute, we need the symplectic form ω(B_p, A_v) ≡ 0 (mod 2).

              ω(B_p, A_v) = |supp_X(B_p) ∩ supp_Z(A_v)| + |supp_Z(B_p) ∩ supp_X(A_v)|

              Since B_p is Z-type (supp_X(B_p) = ∅) and A_v is X-type (supp_Z(A_v) = ∅):

              The key insight: the number of edges in cycle p incident to vertex v is always even:

              Therefore ω(B_p, A_v) ≡ 0 (mod 2), so [B_p, A_v] = 0.

              def GraphWithCycles.cycleEdgesIncidentTo {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) (p : C) (v : V) :

              The set of edges that are both in cycle p and incident to vertex v

              Equations
              Instances For
                def GraphWithCycles.flux_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) (p : C) (v : V) :

                The symplectic form between a flux operator B_p and a Gauss law operator A_v. ω(B_p, A_v) = |Z-support of B_p ∩ X-support of A_v on edges| = |edges in cycle p incident to v|

                Equations
                Instances For
                  theorem GraphWithCycles.cycleEdgesIncidentTo_card_even {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) (p : C) (v : V) (h_valid_cycle : (G.cycleEdgesIncidentTo p v).card = 0 (G.cycleEdgesIncidentTo p v).card = 2) :

                  The number of edges in a cycle incident to any vertex is even (0 or 2).

                  For a cycle p and vertex v:

                  • If v is not on the cycle: 0 edges are incident (even)
                  • If v is on the cycle: exactly 2 edges are incident (the two edges of the cycle at v)

                  This is because a cycle visits each of its vertices exactly once, entering and leaving via two distinct edges.

                  Note: This property requires that cycles are "proper" in the sense that they form a simple path returning to the start. We state it as a hypothesis since the structure GraphWithCycles allows arbitrary finsets of edges as "cycles". In practice, cycles arising from Euler's formula satisfy this property.

                  theorem GraphWithCycles.flux_commutes_with_gaussLaw {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) (p : C) (v : V) (h_valid : (G.cycleEdgesIncidentTo p v).card % 2 = 0) :

                  Flux operators commute with Gauss law operators. This requires the cycle validity hypothesis that each vertex has 0 or 2 incident edges from the cycle.

                  Initial State Stabilization #

                  The flux operators B_p arise from the initial state |0⟩^⊗E of the edge qubits.

                  Property: Z|0⟩ = |0⟩ (the |0⟩ state is a +1 eigenstate of Z).

                  Initially:

                  After measuring A_v:

                  This is because B_p commutes with all A_v (shown above), so measuring A_v doesn't disturb the eigenvalue of B_p.

                  theorem GraphWithCycles.flux_eigenvalue_on_zero_state {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) (p : C) :
                  _eG.cycles p, 0 = 0

                  In the computational basis, |0⟩ is a +1 eigenstate of Z. We represent this as: the eigenvalue of B_p on |0⟩^⊗E is (+1)^|p| = +1. The eigenvalue (+1)^|p| = +1 because any power of +1 is +1. In ZMod 2: the phase contribution from Z operators on |0⟩ states is 0.

                  The initial stabilizer condition: each edge qubit in state |0⟩ is stabilized by Z_e. Represented as: Z|0⟩ = +|0⟩, so measurement outcome is 0 (for +1) in ZMod 2.

                  Equations
                  Instances For
                    theorem GraphWithCycles.flux_stabilizes_initial_state {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) (p : C) :

                    Product of initial stabilizer outcomes for B_p is +1 (represented as 0 in ZMod 2)

                    Relationship to Second Boundary Map #

                    The edge support of B_p equals ∂₂(p) where ∂₂ is the second boundary map from Def_1. This connects flux operators to the chain complex structure.

                    The edge support of B_p equals the second boundary of the basis vector at p

                    theorem GraphWithCycles.fluxOperator_edgeSupport_characteristic {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) (p : C) (e : E) :

                    The flux operator support is exactly the characteristic vector of the cycle

                    Support Size #

                    The weight (support size) of B_p equals the number of edges in cycle p.

                    theorem GraphWithCycles.fluxOperator_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) (p : C) :
                    {e : E | G.fluxOperator_edgeSupport p e = 1}.card = (G.cycles p).card

                    The support size of B_p on edge qubits equals the size of cycle p

                    noncomputable def GraphWithCycles.fluxOperator_weight {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) (p : C) :

                    The weight of flux operator B_p

                    Equations
                    Instances For
                      theorem GraphWithCycles.fluxOperator_weight_eq_support {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) (p : C) :

                      The weight equals the support size

                      Product of Flux Operators #

                      When cycles share edges, the product of their flux operators corresponds to the symmetric difference of their edge sets.

                      theorem GraphWithCycles.flux_product_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) (p q : C) (e : E) :

                      Sum (product) of edge supports of two flux operators

                      Commutativity Verification Details #

                      We provide a more detailed verification of why B_p commutes with A_v.

                      def GraphWithCycles.flux_ZSupport {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) (p : C) :

                      The Z-support of B_p on edges (edges in cycle p)

                      Equations
                      Instances For
                        def GraphWithCycles.gaussLaw_XSupport {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 X-support of A_v on edges (edges incident to v)

                        Equations
                        Instances For
                          def GraphWithCycles.flux_gaussLaw_intersection {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) (p : C) (v : V) :

                          The intersection of Z-support of B_p and X-support of A_v

                          Equations
                          Instances For
                            theorem GraphWithCycles.flux_gaussLaw_intersection_eq {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) (p : C) (v : V) :

                            The intersection equals the cycle edges incident to v

                            The symplectic form equals the cardinality of this intersection

                            Type Characterization #

                            Flux operators are purely Z-type: they act only via Pauli-Z operators on edges, with no X or Y components.

                            theorem GraphWithCycles.flux_is_Z_type_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) (p : C) (v : V) :

                            B_p is purely Z-type: no X support on vertices

                            theorem GraphWithCycles.flux_is_Z_type_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) (p : C) :

                            B_p is purely Z-type: no X support on edges

                            Comparison with Gauss Law Operators #

                            Gauss law operators A_v are X-type, flux operators B_p are Z-type:

                            This complementary structure ensures they commute.

                            Summary: A_v is X-type (Z-support empty)

                            theorem GraphWithCycles.flux_is_Z_type {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) (p : C) :

                            Summary: B_p is Z-type (X-support empty)

                            Combined: The symplectic form ω(B_p, A_v) counts edges in cycle p incident to v

                            Valid Cycle Condition #

                            For the commutativity proof to work, we need that cycles are "valid" in the sense that each vertex has 0 or 2 incident edges from the cycle.

                            This is automatically satisfied for cycles arising from Euler's formula in a connected graph, but we state it explicitly since our GraphWithCycles structure allows arbitrary finsets of edges.

                            def GraphWithCycles.IsValidCycle {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) (p : C) :

                            A cycle is valid if every vertex has 0 or 2 incident edges from the cycle

                            Equations
                            Instances For
                              theorem GraphWithCycles.flux_commutes_with_all_gaussLaw {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) (p : C) (h_valid : G.IsValidCycle p) (v : V) :

                              For valid cycles, flux operators commute with all Gauss law operators

                              Euler's Formula Statement #

                              The number of independent cycles in a connected graph is |E| - |V| + 1.

                              theorem GraphWithCycles.euler_formula_cycles {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) (h_edges : Fintype.card V Fintype.card E) (h_cycle_count : Fintype.card C = Fintype.card E - Fintype.card V + 1) :

                              Euler's formula for connected graphs: the cycle rank (first Betti number) is |E| - |V| + 1. This theorem states that if the cycle type C has the correct cardinality, then |C| = |E| - |V| + 1.

                              Note: For connected graphs with at least one cycle, we have |E| ≥ |V| (spanning tree has |V| - 1 edges, so any additional edge creates a cycle). This hypothesis ensures natural number subtraction matches integer subtraction.

                              Summary #

                              The flux operators formalize the second key concept from the gauging measurement protocol:

                              1. Definition: B_p = ∏_{e ∈ p} Z_e represented as binary vectors over ZMod 2

                                • Vertex support: zero everywhere (Z-type has no X component)
                                • Edge support: boundary₂(e_p) (1 at edges in cycle p, 0 elsewhere)
                              2. Property 1 (Hermitian): B_p² = I

                                • In ZMod 2: support + support = 0
                                • Implies eigenvalues are ±1
                              3. Property 2 (Commutativity among flux ops): [B_p, B_q] = 0 for all p, q

                                • Z-type operators have zero symplectic form with each other
                                • All flux operators mutually commute
                              4. Property 3 (Commutativity with Gauss law): [B_p, A_v] = 0

                                • The symplectic form ω(B_p, A_v) = |edges in cycle p incident to v|
                                • This is always even (0 or 2 for valid cycles)
                                • Therefore flux and Gauss law operators commute
                              5. Initial State: B_p stabilizes |0⟩^⊗E

                                • Z|0⟩ = |0⟩, so products of Z also stabilize |0⟩
                                • This stabilizer structure is preserved after measuring A_v
                              6. Euler's Formula: C = |E| - |V| + 1 independent cycles

                                • The cycle type C has this many elements for a connected graph
                                • Each independent cycle gives one flux operator
                              7. Relationship to Chain Complex:

                                • Edge support of B_p = ∂₂(e_p) (second boundary map from Def_1)
                                • Connects to the algebraic structure of the graph