By simplification using the definition of \(\operatorname {incidentEdges}\), which is a filter on the universe by the predicate \(v \in e\), this equivalence holds directly.

This holds by reflexivity, since the \(\operatorname {zVec}\) component of \(\operatorname {gaussLawOp}\) is defined to be \(0\).

This holds by reflexivity, since the \(\operatorname {xVec}\) component of \(\operatorname {fluxOp}\) is defined to be \(0\).

By extensionality, for any qubit \(q\), we simplify using the definitions of \(\operatorname {supportZ}\) and \(\operatorname {gaussLawOp}\). Since \(A_v.\operatorname {zVec} = 0\), no qubit \(q\) can belong to \(\operatorname {supportZ}(A_v)\), so \(\operatorname {supportZ}(A_v) = \emptyset \).

By extensionality, for any qubit \(q\), we simplify using the definitions of \(\operatorname {supportX}\) and \(\operatorname {fluxOp}\). Since \(B_p.\operatorname {xVec} = 0\), no qubit \(q\) can belong to \(\operatorname {supportX}(B_p)\), so \(\operatorname {supportX}(B_p) = \emptyset \).

We unfold the definitions of \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\). The symplectic inner product is a sum over all qubits \(q\):

We show each summand is zero. For each \(q\), since both \(A_v\) and \(A_w\) have \(\operatorname {zVec} = 0\), both terms in the sum vanish by simplification using the definition of \(\operatorname {gaussLawOp}\).

We unfold the definitions of \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\). The symplectic inner product is a sum over all qubits \(r\). We show each summand is zero. For each \(r\), since both \(B_p\) and \(B_q\) have \(\operatorname {xVec} = 0\), both terms in the sum vanish by simplification using the definition of \(\operatorname {fluxOp}\).

We unfold the definitions of \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\). The symplectic inner product is

Since \(A_v\) is pure \(X\)-type (\(\operatorname {zVec} = 0\)) and \(B_p\) is pure \(Z\)-type (\(\operatorname {xVec} = 0\)), the second term in each summand vanishes. We establish that

by congruence: for each \(q\), the extra terms simplify to zero using the definitions of \(\operatorname {gaussLawOp}\) and \(\operatorname {fluxOp}\). Rewriting with this identity, we split the sum over \(V \oplus E\) into vertex and edge parts using \(\operatorname {Fintype.sum\_ sum\_ type}\).

For the vertex part: \(\sum _{w \in V} (A_v)_x(\operatorname {inl}(w)) \cdot (B_p)_z(\operatorname {inl}(w)) = 0\), because \(B_p\) has \(\operatorname {zVec} = 0\) on vertices. We show each summand is zero by simplification, then rewrite with this identity and \(0 + (\cdot ) = (\cdot )\).

For the edge part: we establish that

This is shown by congruence and case analysis: for each edge \(e\), we consider the cases \(v \in e\) and \(e \in \operatorname {cycles}(p)\) and simplify. Rewriting with this identity, we apply \(\operatorname {Finset.sum\_ boole}\) to convert the sum of indicators to a cardinality:

By \(\operatorname {ZMod.natCast\_ eq\_ zero\_ iff\_ even}\), this is \(0 \in \mathbb {Z}/2\mathbb {Z}\) if and only if the count is even. The result then follows directly from the hypothesis \(\operatorname {hcyc}(p, v)\).

Let \(w\) be an arbitrary vertex. We simplify using the definitions of \(\operatorname {supportX}\) and \(\operatorname {gaussLawOp}\). The \(X\)-vector of \(A_v\) at \(\operatorname {inl}(w)\) is \(1\) if \(w = v\) and \(0\) otherwise, so the result follows directly.

Let \(e\) be an arbitrary edge. We simplify using the definitionsof \(\operatorname {supportX}\) and \(\operatorname {gaussLawOp}\). The \(X\)-vector of \(A_v\) at \(\operatorname {inr}(e)\) is \(1\) if \(v \in e\) and \(0\) otherwise, so the result follows directly.

Let \(e\) be an arbitrary edge. We simplify using the definitions of \(\operatorname {supportZ}\) and \(\operatorname {fluxOp}\). The \(Z\)-vector of \(B_p\) at \(\operatorname {inr}(e)\) is \(1\) if \(e \in \operatorname {cycles}(p)\) and \(0\) otherwise, so the result follows directly.

Let \(w\) be an arbitrary vertex. We simplify using the definitions of \(\operatorname {supportZ}\) and \(\operatorname {fluxOp}\). Since \(B_p.\operatorname {zVec}(\operatorname {inl}(w)) = 0\), the vertex qubit \(\operatorname {inl}(w)\) does not belong to \(\operatorname {supportZ}(B_p)\).

By simplification using the definition of \(\operatorname {gaussLawOp}\). The \(X\)-vector of \(A_w\) at \(\operatorname {inl}(v)\) is \(1\) if \(w = v\) and \(0\) otherwise, so the sum picks out exactly the single term \(w = v\), giving \(1\).

We unfold the definition of \(\operatorname {gaussLawOp}\). The sum counts, modulo \(2\), the number of vertices \(v\) with \(v \in e\). We decompose the edge: let \(e = \{ a, b\} \) with \(a \neq b\) (since \(G\) has no loops). The sum \(\sum _{v \in V} [\! [v \in \{ a,b\} ]\! ]\) equals \(([\! [v = a]\! ] + [\! [v = b]\! ])\) summed over \(v\).

We establish for each \(v\) that the indicator \([\! [v \in \{ a,b\} ]\! ] = [\! [v = a]\! ] + [\! [v = b]\! ]\) by case analysis: if \(v = a\), we use \(a \neq b\) and simplify via \(\operatorname {Sym2.mem\_ iff}\); if \(v = b\), similarly; if \(v \neq a\) and \(v \neq b\), then \(v \notin \{ a,b\} \) by \(\operatorname {Sym2.mem\_ iff}\) and pushing negation.

Rewriting with this identity, we distribute the sum: \(\sum _v ([\! [v = a]\! ] + [\! [v = b]\! ]) = \sum _v [\! [v = a]\! ] + \sum _v [\! [v = b]\! ]\). Each sum evaluates to \(1\) by \(\operatorname {Finset.sum\_ ite\_ eq’}\) over the universe. The result is \(1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\) by \(\operatorname {CharTwo.add\_ self\_ eq\_ zero}\).

By extensionality, we must show that the \(\operatorname {xVec}\) and \(\operatorname {zVec}\) components agree.

For xVec: We rewrite the \(\operatorname {xVec}\) of the product as a sum over the universe, then apply the private helper lemma prod_pauliOp_xVec to express \((\prod _v A_v)_x(q) = \sum _v (A_v)_x(q)\). We case-split on \(q\):

• If \(q = \operatorname {inl}(w)\) for a vertex \(w\): by simplification using \(\operatorname {gaussLawOp}\) and \(\operatorname {logicalOp}\), we rewrite the sum \(\sum _v [\! [v = w]\! ]\) using \(\operatorname {Finset.sum\_ ite\_ eq’}\) over the universe to obtain \(1\), which matches \(L_x(\operatorname {inl}(w)) = 1\).

• If \(q = \operatorname {inr}(e)\) for an edge \(e\): by simplification using \(\operatorname {gaussLawOp}\) and \(\operatorname {logicalOp}\), the result follows from \(\operatorname {gaussLaw\_ product\_ xVec\_ inr}\), which gives \(0 = L_x(\operatorname {inr}(e))\).

For zVec: We similarly rewrite using prod_pauliOp_zVec. Since every \(A_v\) has \(\operatorname {zVec} = 0\), the sum is \(0\) for all \(q\), matching \(L.\operatorname {zVec} = 0\). This is verified by simplification using the definitions of \(\operatorname {gaussLawOp}\) and \(\operatorname {logicalOp}\).

By extensionality, for any qubit \(q\), we simplify using the definitions of \(\operatorname {supportZ}\) and \(\operatorname {logicalOp}\). Since \(L.\operatorname {zVec} = 0\), no qubit belongs to \(\operatorname {supportZ}(L)\).

We unfold the definitions of \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\). The symplectic inner product is a sum over all qubits \(q\). We show each summand is zero by case-splitting on \(q\):

• If \(q = \operatorname {inl}(w)\): by simplification using the definitions of \(\operatorname {logicalOp}\) and \(\operatorname {fluxOp}\), the term vanishes since \(B_p.\operatorname {zVec}(\operatorname {inl}(w)) = 0\) and \(B_p.\operatorname {xVec} = 0\).

• If \(q = \operatorname {inr}(e)\): by simplification using the definitions of \(\operatorname {logicalOp}\) and \(\operatorname {fluxOp}\), the term vanishes since \(L.\operatorname {zVec} = 0\) and \(L.\operatorname {xVec}(\operatorname {inr}(e)) = 0\).

This follows directly by combining the three individual commutation theorems: part (i) from \(\operatorname {gaussLaw\_ commute}\), part (ii) from \(\operatorname {flux\_ commute}\), and part (iii) from \(\operatorname {gauss\_ flux\_ commute}\).

We unfold the definition of \(\operatorname {gaussLawOp}\) and then rewrite using \(\operatorname {GraphMaps.coboundaryMap\_ single}\), which expresses the coboundary of a basis vector \(\mathbf{1}_v\) in exactly the same indicator form as \((A_v)_x\) on edges.

We unfold the definition of \(\operatorname {fluxOp}\) and then rewrite using \(\operatorname {GraphMaps.secondBoundaryMap\_ single}\), which expresses the second boundary of a basis vector \(\mathbf{1}_p\) in exactly the same indicator form as \((B_p)_z\) on edges.