12 Def 2: Gauss’s Law Operators
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
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:
Each \(A_v\) is Hermitian with eigenvalues \(\pm 1\).
All \(A_v\) mutually commute: \([A_v, A_{v'}] = 0\) for all \(v, v' \in V_G\).
\(\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\).
The vertex support of Gauss law operator \(A_v\) is a binary vector with \(1\) at position \(v\) and \(0\) elsewhere. Formally,
the basis vector at \(v\). This represents \(X_v\) in the product \(A_v = X_v \prod _{e \ni v} X_e\).
The edge support of Gauss law operator \(A_v\) is \(1\) at edges incident to \(v\) and \(0\) elsewhere. Formally,
the coboundary of vertex \(v\). This represents \(\prod _{e \ni v} X_e\) in the product \(A_v = X_v \prod _{e \ni v} X_e\).
For any \(x \in \mathbb {Z}/2\mathbb {Z}\), we have \(x + x = 0\).
We case-split on \(x\). Since \(\mathbb {Z}/2\mathbb {Z} = \{ 0,1\} \), we check: \(0 + 0 = 0\) and \(1 + 1 = 0\). Both hold by computation.
For any vertex \(v\), the vertex support of \(A_v\) added to itself is zero:
By extensionality, it suffices to show equality at each coordinate \(w\). At each \(w\), the sum becomes \(\operatorname {vertexSupport}(A_v)(w) + \operatorname {vertexSupport}(A_v)(w)\), which by simplification of pointwise addition equals \(x + x\) for some \(x \in \mathbb {Z}/2\mathbb {Z}\). This is \(0\) by the lemma that \(x + x = 0\) in \(\mathbb {Z}/2\mathbb {Z}\).
For any vertex \(v\), the edge support of \(A_v\) added to itself is zero:
By extensionality at each edge \(e\), the sum becomes \(x + x = 0\) in \(\mathbb {Z}/2\mathbb {Z}\) by the self-addition lemma.
For any vertex \(v\) and coordinate \(w\),
This represents \(A_v^2 = I\). If \(A_v|\psi \rangle = \lambda |\psi \rangle \) and \(A_v^2 = I\), then \(\lambda ^2 = 1\), so \(\lambda \in \{ -1, +1\} \).
Let \(w\) be arbitrary. Rewriting \(2 \cdot x\) as \(\mathrm{Nat.cast}(2) \cdot x\), we establish that \((2 : \mathbb {Z}/2\mathbb {Z}) = 0\) by computation. Then \(0 \cdot x = 0\) by simplification.
The \(Z\)-support of a Gauss law operator on vertex qubits is the empty set, since Gauss law operators are purely \(X\)-type:
The \(Z\)-support of a Gauss law operator on edge qubits is also empty:
The symplectic form between two Gauss law operators \(A_v\) and \(A_w\) is defined as
For \(X\)-type operators, this equals \(|\emptyset | + |\emptyset | = 0\).
For any vertices \(v, w\),
Unfolding the definition of \(\omega \), both \(Z\)-support sets are empty by definition, so \(|\emptyset | + |\emptyset | = 0\).
For any vertices \(v, w\), \([A_v, A_w] = 0\). Equivalently,
Since \(\omega (A_v, A_w) = 0\) by the previous theorem, \(0 \mod 2 = 0\).
The sum of all vertex supports of Gauss law operators:
The sum of all edge supports of Gauss law operators:
For each vertex \(w\),
Unfolding the definitions, the sum at coordinate \(w\) becomes \(\sum _{v \in V} \operatorname {vertexSupport}(A_v)(w)\). Since \(\operatorname {vertexSupport}(A_v)\) is the basis vector \(e_v\), this equals \(\sum _{v \in V} (\text{if } v = w \text{ then } 1 \text{ else } 0)\). By the standard identity for sums with indicator functions (summing \(1\) when \(v = w\) over the universe), this equals \(1\).
The sum of all vertex supports equals the all-ones vector:
This is the support of \(L = \prod _{v \in V} X_v\).
By extensionality at each coordinate \(w\), the result follows from the previous theorem.
For each edge \(e\),
Unfolding definitions, the sum at coordinate \(e\) becomes \(\sum _{v \in V} \operatorname {edgeSupport}(A_v)(e)\). Rewriting each term using the edge support definition, this equals \(\sum _{v \in V} (\text{if } G.\mathrm{isIncident}(e, v) \text{ then } 1 \text{ else } 0)\) in \(\mathbb {Z}/2\mathbb {Z}\).
We split the sum into incident and non-incident vertices. The sum over non-incident vertices is \(0\) (each term is \(0\)). For the incident vertices, let \(v_1, v_2\) be the two endpoints of \(e\), which satisfy \(v_1 \neq v_2\) by the edge endpoints lemma. We establish that the filter of vertices incident to \(e\) is exactly \(\{ v_1, v_2\} \): a vertex \(v\) is incident to \(e\) iff \(v\) equals \(v_1\) or \(v_2\) (unfolding the incidence definition). Therefore the sum over incident vertices is \(1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\) (since each edge is incident to exactly its two distinct endpoints, and \(1 + 1 = 0 \pmod{2}\)).
The sum of all edge supports is the zero vector:
This represents \(X_e^2 = I\) for each edge (edges cancel pairwise).
By extensionality at each coordinate \(e\), the zero vector has value \(0\) at \(e\), which equals the product edge support at \(e\) by the previous theorem.
The product of all Gauss law operators equals \(L\):
Specifically:
Vertex support: \(\sum _v \operatorname {vertexSupport}(A_v) = \mathbf{1}\) (the support of \(L = \prod _v X_v\)).
Edge support: \(\sum _v \operatorname {edgeSupport}(A_v) = \mathbf{0}\) (since \(X_e^2 = I\), edge terms cancel).
This follows directly by pairing the two results: the vertex support is all-ones and the edge support is zero.
The edge support of \(A_v\) equals the coboundary of the basis vector at \(v\):
where \(\delta \) is the coboundary map from Definition 1.
Unfolding the edge support definition, \(\operatorname {edgeSupport}(A_v) = \delta _0(v)\) (the coboundary of vertex \(v\)). Rewriting using the lemma that \(\delta (e_v) = \delta _0(v)\) (the coboundary map applied to the basis vector at \(v\) equals the coboundary of vertex \(v\)), the result follows.
The sum of all edge supports equals the coboundary of the all-ones vector:
Rewriting each edge support as \(\delta (e_v)\), the sum becomes \(\sum _v \delta (e_v)\). By linearity of the coboundary map \(\delta \), this equals \(\delta \! \left(\sum _v e_v\right)\). It remains to show \(\sum _v e_v = \mathbf{1}\). By extensionality at each coordinate \(w\), \(\sum _v e_v(w) = \sum _v (\text{if } v = w \text{ then } 1 \text{ else } 0) = 1\).
The number of Gauss law operators equals the number of vertices:
The number of constraints among Gauss law operators is \(1\) (the single product constraint \(\prod _v A_v = L\)).
The number of independent Gauss law generators is
If \(|V| \geq 1\), then the independent count equals \(|V| - 1\).
Unfolding the definitions: the independent count is the generator count minus the constraint count, which is \(|V| - 1\). This follows by simplification.
The abelian group generated by \(\{ A_v\} \) has order
For any vertex \(w\),
This follows directly from the theorem that the product vertex support at each vertex is \(1\), after unfolding the product vertex support as a pointwise sum.
There exists a generator that is a linear combination of the others. Specifically, there exists \(v_0 \in V\) such that for all \(w \in V\),
Since \(V\) is nonempty, we obtain some \(v_0 \in V\). Let \(w \in V\) be arbitrary. From the constraint equation, we have \(\sum _{v \in V} \operatorname {vertexSupport}(A_v)(w) = 1\). Rewriting this sum by separating out \(v_0\):
By ring arithmetic, \(\operatorname {vertexSupport}(A_{v_0})(w) = \operatorname {vertexSupport}(A_{v_0})(w) + 0\). Adding and subtracting \(\sum _{v \neq v_0}\) and rearranging by ring identities, we obtain \(\operatorname {vertexSupport}(A_{v_0})(w) = 1 - \sum _{v \in V \setminus \{ v_0\} } \operatorname {vertexSupport}(A_v)(w)\).
The degree of vertex \(v\) in the graph \(G\) is the number of edges incident to \(v\):
The number of edges where \(A_v\) has support \(1\) equals the degree of \(v\):
It suffices to show the two finsets are equal. By extensionality at each edge \(e\): \(\operatorname {edgeSupport}(A_v)(e) = 1\) iff \(G.\mathrm{isIncident}(e, v)\), by the edge support characterization. Splitting on cases, if \(e\) is incident to \(v\) then \(\operatorname {edgeSupport}(A_v)(e) = 1\), and if not then \(\operatorname {edgeSupport}(A_v)(e) = 0 \neq 1\). Thus the filter set equals the set of incident edges, which has cardinality \(\deg (v)\).
The total support size of \(A_v\) is \(1\) (for the vertex qubit) plus \(\deg (v)\) (for the edge qubits):
The Gauss law operator \(A_v\) corresponds to the coboundary of its vertex support:
This shows \(A_v = X_v \cdot \prod _{e \ni v} X_e\) in the binary vector representation.
Unfolding the vertex support definition, \(\operatorname {vertexSupport}(A_v) = e_v\) (the basis vector). Unfolding the edge support definition, \(\operatorname {edgeSupport}(A_v) = \delta _0(v)\) (the coboundary of vertex \(v\)). Rewriting using the lemma that \(\delta (e_v) = \delta _0(v)\), the equality holds.
Convert a measurement outcome to \(\mathbb {Z}/2\mathbb {Z}\):
The product of measurement outcomes as a \(\mathbb {Z}/2\mathbb {Z}\) sum:
The XOR of all measurement outcomes determines the \(L\) eigenvalue:
That is, the product is \(0\) (meaning \(L\) eigenvalue \(+1\)) if and only if the number of \(-1\) outcomes is even.
Unfolding the measurement product, we rewrite the \(\mathbb {Z}/2\mathbb {Z}\) sum as the cardinality of the set of vertices with outcome \(-1\) (i.e., where \(\mathrm{measurementToZMod2} = 1\)), using the identity that a sum of \(\mathbb {Z}/2\mathbb {Z}\) values equals the count of \(1\)s cast to \(\mathbb {Z}/2\mathbb {Z}\).
For the forward direction: if \(\mathrm{measurementProduct} = 0\), we extract the \(\mathbb {Z}/2\mathbb {Z}\) value via \(\mathrm{ZMod.val}\) and conclude that the cardinality modulo \(2\) is \(0\).
For the reverse direction: if the cardinality is \(0 \pmod{2}\), we rewrite the natural number cast to \(\mathbb {Z}/2\mathbb {Z}\) using \(\mathrm{ZMod.natCast\_ mod}\) to replace the cardinality with its remainder modulo \(2\), which is \(0\), and then simplify.
If all outcomes are \(+1\), the measurement product is \(0\) (i.e., \(L\) eigenvalue is \(+1\)):
Unfolding the definitions of \(\mathrm{measurementProduct}\) and \(\mathrm{measurementToZMod2}\), it suffices to show the sum is zero. We show each term is zero: for any \(v\), rewriting using the hypothesis \(\mathrm{outcomes}(v) = +1\), the term becomes \(\mathrm{measurementToZMod2}(+1) = 0\). A sum of zeros is \(0\).