13 Def 3: Flux Operators
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:
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 \(\lvert 0\rangle ^{\otimes E_G}\) of the edge qubits:
Initially, \(Z_e \lvert 0\rangle _e = \lvert 0\rangle _e\) for each edge, so each \(Z_e\) is a stabilizer.
After measuring the Gauss’s law operators \(A_v\) (which involve \(X_e\) terms), individual \(Z_e\) operators are no longer stabilizers.
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.
The number of independent cycles in a connected graph according to Euler’s formula. For a connected graph with vertex set \(V\) and edge set \(E\):
We represent this as an integer to handle the subtraction correctly:
The vertex support of flux operator \(B_p\): zero everywhere. Since \(B_p\) is a \(Z\)-type operator, it has no \(X\) component on vertices. For any graph \(G\) and cycle \(p\):
The edge support of flux operator \(B_p\): \(1\) at edges in cycle \(p\), \(0\) elsewhere. This represents \(B_p = \prod _{e \in p} Z_e\). For a graph \(G\) and cycle \(p\):
i.e., the image of cycle \(p\) under the second boundary map.
For a graph \(G\), cycle \(p\), and edge \(e\) with \(e \in \operatorname {cycles}(G, p)\):
By simplification using the definitions of fluxOperator_edgeSupport and boundary2OfCycle_apply, together with the hypothesis \(e \in \operatorname {cycles}(G, p)\), the result follows.
For a graph \(G\), cycle \(p\), and edge \(e\) with \(e \notin \operatorname {cycles}(G, p)\):
By simplification using the definitions of fluxOperator_edgeSupport and boundary2OfCycle_apply, together with the hypothesis \(e \notin \operatorname {cycles}(G, p)\), the result follows.
For a graph \(G\), cycle \(p\), and edge \(e\):
By simplification using the definitions of fluxOperator_edgeSupport and boundary2OfCycle_apply, the result follows directly.
\(B_p^2 = I\) on edge support: in \(\mathbb {Z}/2\mathbb {Z}\), the edge support added to itself equals zero:
By extensionality, it suffices to show equality for an arbitrary edge \(e\). Using the pointwise addition of \(\Pi \)-types and the zero function, the goal reduces to showing \(f(e) + f(e) = 0\) for each component. This follows directly from the lemma that \(x + x = 0\) in \(\mathbb {Z}/2\mathbb {Z}\) for any \(x\).
\(B_p\) is Hermitian with eigenvalues \(\pm 1\). This is represented by \(B_p^2 = I\), which in \(\mathbb {Z}/2\mathbb {Z}\) is: \(2 \cdot \operatorname {support} = 0\). Formally, for all edges \(e\):
Let \(e\) be an arbitrary edge. Rewriting \(2 \cdot x\) as \(\operatorname {Nat.cast}(2) \cdot x\), we establish that \((2 : \mathbb {Z}/2\mathbb {Z}) = 0\) by computation (decide). Then by simplification with this fact, the result follows.
The \(X\)-support of a flux operator on vertices is empty (\(Z\)-type operators have no \(X\) component):
The \(X\)-support of a flux operator on edges is also empty:
The symplectic form between two flux operators. For \(Z\)-type operators:
Formally:
The symplectic form is zero for \(Z\)-type operators:
By simplification using the definition of flux_symplectic and the fact that both \(X\)-supports are empty, the cardinalities are both \(0\), so the sum is \(0\).
Two flux operators commute: \([B_p, B_q] = 0\) since \(\omega (B_p, B_q) = 0\) (\(Z\)-type operators always commute). Formally:
By simplification using the fact that flux_symplectic_zero gives \(\operatorname {flux\_ symplectic}(G, p, q) = 0\), the result \(0 \bmod 2 = 0\) follows immediately.
The set of edges that are both in cycle \(p\) and incident to vertex \(v\):
The symplectic form between a flux operator \(B_p\) and a Gauss law operator \(A_v\):
i.e., the number of edges in cycle \(p\) that are incident to vertex \(v\).
The number of edges in a cycle incident to any vertex is even (0 or 2). For a cycle \(p\) and vertex \(v\), if
then
We consider two cases from the hypothesis. Case 1: if the cardinality is \(0\), then \(0 \bmod 2 = 0\) follows by simplification. Case 2: if the cardinality is \(2\), then \(2 \bmod 2 = 0\) follows by simplification.
Flux operators commute with Gauss law operators. Given the cycle validity hypothesis that each vertex has an even number of incident edges from the cycle:
By simplification using the definition of flux_gaussLaw_symplectic, the goal reduces to the hypothesis \(|\operatorname {cycleEdgesIncidentTo}(G, p, v)| \bmod 2 = 0\), which is exactly the given assumption.
In the computational basis, \(\lvert 0\rangle \) is a \(+1\) eigenstate of \(Z\). The eigenvalue of \(B_p\) on \(\lvert 0\rangle ^{\otimes E}\) is \((+1)^{|p|} = +1\). In \(\mathbb {Z}/2\mathbb {Z}\), the phase contribution from \(Z\) operators on \(\lvert 0\rangle \) states is \(0\):
By simplification, a sum of zeros over any index set equals zero.
The initial stabilizer condition: each edge qubit in state \(\lvert 0\rangle \) is stabilized by \(Z_e\). Represented as \(Z\lvert 0\rangle = +\lvert 0\rangle \), so the measurement outcome is \(0\) (for \(+1\)) in \(\mathbb {Z}/2\mathbb {Z}\):
Product of initial stabilizer outcomes for \(B_p\) is \(+1\) (represented as \(0\) in \(\mathbb {Z}/2\mathbb {Z}\)):
By simplification using the definition of initialEdgeStabilizerOutcome (which is identically \(0\)), the sum reduces to \(0\).
The edge support of \(B_p\) equals the second boundary of the basis vector at \(p\):
By simplification using the definition of fluxOperator_edgeSupport, the left-hand side unfolds to \(\operatorname {boundary2OfCycle}(G, p)\). Rewriting using boundary2Map_basisC, which states that \(\partial _2(\mathbf{e}_p) = \operatorname {boundary2OfCycle}(G, p)\), the result follows.
The flux operator support is exactly the characteristic vector of the cycle. For all edges \(e\):
Let \(e\) be an arbitrary edge. The result follows directly from fluxOperator_edgeSupport_apply.
The support size of \(B_p\) on edge qubits equals the size of cycle \(p\):
We show the two finsets are equal by applying congr 1 and then extensionality. For an arbitrary edge \(e\), using membership in the universal finset and filter, together with fluxOperator_edgeSupport_apply, we split on whether \(e \in \operatorname {cycles}(G, p)\). In the positive case, the support value is \(1\), so membership holds by simplification. In the negative case, the support value is \(0 \neq 1\), so non-membership holds by simplification.
The weight of flux operator \(B_p\), defined as the number of edges in cycle \(p\):
The weight equals the support size:
Rewriting using fluxOperator_edgeSupport_size, the right-hand side becomes \(|\operatorname {cycles}(G,p)|\), which equals the left-hand side by definition (rfl).
The sum (product) of edge supports of two flux operators corresponds to the symmetric difference. For any edge \(e\):
By simplification using pointwise addition and fluxOperator_edgeSupport_apply, we case-split on whether \(e \in \operatorname {cycles}(G,p)\) and \(e \in \operatorname {cycles}(G,q)\). In each of the four cases:
\(e \in p\), \(e \in q\): the XOR condition is false, and \(1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\), by reflexivity.
\(e \in p\), \(e \notin q\): the XOR condition is true, and \(1 + 0 = 1\), verified by computation.
\(e \notin p\), \(e \in q\): the XOR condition is true, and \(0 + 1 = 1\), verified by computation.
\(e \notin p\), \(e \notin q\): the XOR condition is false, and \(0 + 0 = 0\), by simplification.
The \(Z\)-support of \(B_p\) on edges (edges in cycle \(p\)):
The \(X\)-support of \(A_v\) on edges (edges incident to \(v\)):
The intersection of the \(Z\)-support of \(B_p\) and the \(X\)-support of \(A_v\):
The intersection equals the cycle edges incident to \(v\):
By extensionality on an arbitrary edge \(e\). Unfolding the definitions of flux_gaussLaw_intersection, flux_ZSupport, gaussLaw_XSupport, cycleEdgesIncidentTo, and incidentEdges, membership in the intersection of two finsets and membership in a filtered finset both reduce to the conjunction of \(e \in \operatorname {cycles}(G,p)\) and \(\operatorname {isIncident}(e, v)\), by simplification.
The symplectic form equals the cardinality of the intersection:
By simplification using flux_gaussLaw_symplectic and flux_gaussLaw_intersection_eq, the result follows directly.
\(B_p\) is purely \(Z\)-type: no \(X\) support on vertices. For all \(v \in V\):
Let \(v\) be an arbitrary vertex. This holds by reflexivity, since the vertex support is defined to be identically zero.
\(B_p\) is purely \(Z\)-type: no \(X\) support on edges:
This holds by reflexivity, since the \(X\)-support on edges is defined to be the empty set.
\(A_v\) is \(X\)-type (\(Z\)-support empty):
Both components hold by reflexivity, since both \(Z\)-supports are defined to be empty sets. We verify both conditions by the constructor and rfl for each.
\(B_p\) is \(Z\)-type (\(X\)-support empty):
Both components hold by reflexivity, since both \(X\)-supports are defined to be empty sets. We verify both conditions by the constructor and rfl for each.
The symplectic form \(\omega (B_p, A_v)\) counts edges in cycle \(p\) incident to \(v\):
This holds by reflexivity (definitional equality).
A cycle \(p\) is valid if every vertex has \(0\) or \(2\) incident edges from the cycle:
For valid cycles, flux operators commute with all Gauss law operators. If \(p\) is a valid cycle, then for all \(v \in V\):
Let \(v\) be an arbitrary vertex. We apply flux_commutes_with_gaussLaw to \(G\), \(p\), \(v\), supplying the hypothesis that \(|\operatorname {cycleEdgesIncidentTo}(G, p, v)| \bmod 2 = 0\). This hypothesis is obtained from cycleEdgesIncidentTo_card_even applied to \(G\), \(p\), \(v\), and the validity condition \(h\_ {\text{valid}}(v)\) which gives \(|\operatorname {cycleEdgesIncidentTo}(G, p, v)| \in \{ 0, 2\} \).
Euler’s formula for connected graphs: the cycle rank (first Betti number) is \(|E| - |V| + 1\). If \(|V| \le |E|\) and \(|C| = |E| - |V| + 1\) (as natural numbers), then:
By simplification using the definition of independentCycleCount. Rewriting with the hypothesis \(|C| = |E| - |V| + 1\), and using that natural number casts distribute over addition and that \(1\) maps to \(1\), it suffices to show the cast of the natural number subtraction equals the integer subtraction. Using congr 1, this reduces to \(\operatorname {Int.ofNat}(|E| - |V|) = (|E| : \mathbb {Z}) - (|V| : \mathbb {Z})\), which follows from Int.ofNat_sub applied to the hypothesis \(|V| \le |E|\).