Suppose for contradiction that there exists \(\gamma \) with \(\operatorname {BoundaryCondition}(G, P, \gamma )\). Then by boundaryCondition_implies_commutes, we conclude \(\operatorname {CommutesWithLogical}(P)\), contradicting the hypothesis \(\neg \operatorname {CommutesWithLogical}(P)\).

Rewriting via the distributivity of finite sums, \(\sum _v f(v) + \sum _v g(v) = \sum _v (f(v) + g(v))\), it suffices to show equality pointwise. By extensionality, for each \(v\), this follows directly from zSupportOnVertices_mul, which gives \(\operatorname {zSupportOnVertices}(P \cdot Q)(v) = \operatorname {zSupportOnVertices}(P)(v) + \operatorname {zSupportOnVertices}(Q)(v)\).

Unfolding \(\operatorname {CommutesWithLogical}\) in all hypotheses and the goal, we have \(\sum _v \operatorname {zSupportOnVertices}(P)(v) = 0\) and \(\sum _v \operatorname {zSupportOnVertices}(Q)(v) = 0\). By the Z-support sum additivity, \(\sum _v \operatorname {zSupportOnVertices}(P \cdot Q)(v) = 0 + 0 = 0\).

Assume for contradiction that \(\operatorname {CommutesWithLogical}(P)\) holds. Then by mul_commuting_preserves_commutesWithLogical applied to \(P\) and \(Q\), we obtain \(\operatorname {CommutesWithLogical}(P \cdot Q)\), contradicting the hypothesis.

Unfolding \(\operatorname {zSupportOnVertices}\), the goal becomes \(\sum _w (\text{if } (\operatorname {pauliZ}(v)).\mathit{zVec}(w) \neq 0 \text{ then } 1 \text{ else } 0) = 1\). We first establish that for each \(w\), the indicator equals \(\text{if } w = v \text{ then } 1 \text{ else } 0\). For the case \(w = v\): substituting, by Pi.single_eq_same the \(z\)-vector value at \(v\) is nonzero, giving \(1\). For \(w \neq v\): by Pi.single_eq_of_ne, the \(z\)-vector at \(w\) is \(0\), giving \(0\). Rewriting the sum with these equalities and simplifying using the characteristic sum \(\sum _w [\! [w = v]\! ] = 1\), we obtain \(1\).

Unfolding \(\operatorname {CommutesWithLogical}\), the goal becomes \(\sum _w \operatorname {zSupportOnVertices}(\operatorname {pauliZ}(v))(w) \neq 0\). By the lemma zSupportOnVertices_singleZ_sum, this sum equals \(1\). Since \(1 \neq 0\) in \(\mathbb {Z}/2\mathbb {Z}\), the result follows.

Unfolding \(\operatorname {CommutesWithLogical}\) and rewriting via the Z-support sum additivity and the fact that \(\sum _w \operatorname {zSupportOnVertices}(\operatorname {pauliZ}(v))(w) = 1\), the goal reduces to showing \(\sum _v \operatorname {zSupportOnVertices}(P)(v) + 1 = 0 \iff \sum _v \operatorname {zSupportOnVertices}(P)(v) \neq 0\) in \(\mathbb {Z}/2\mathbb {Z}\).

For the forward direction: assume \(\sum _v \operatorname {zSupportOnVertices}(P)(v) + 1 = 0\) and suppose for contradiction that \(\sum _v \operatorname {zSupportOnVertices}(P)(v) = 0\). Substituting gives \(0 + 1 = 0\), i.e. \(1 = 0\), a contradiction.

For the reverse direction: assume \(\sum _v \operatorname {zSupportOnVertices}(P)(v) \neq 0\). In \(\mathbb {Z}/2\mathbb {Z}\), every element is \(0\) or \(1\). Since the sum is not \(0\), it must be \(1\). Then \(1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\) (by the characteristic-two identity), as required.

Unfolding \(\operatorname {CommutesWithLogical’}\) and \(\operatorname {zSupportRestricted}\), it suffices to show that for each vertex \(v\), the indicator \([\! [(P \cdot \operatorname {pauliZ}(\operatorname {inr}(e))).\mathit{zVec}(\operatorname {inl}(v)) \neq 0]\! ]\) equals \([\! [P.\mathit{zVec}(\operatorname {inl}(v)) \neq 0]\! ]\). We establish that \((\operatorname {pauliZ}(\operatorname {inr}(e))).\mathit{zVec}(\operatorname {inl}(v)) = 0\) by simplifying: since \(\operatorname {inl}(v) \neq \operatorname {inr}(e)\), the single function evaluates to \(0\) by Pi.single_eq_of_ne. Then the multiplication formula for \(\mathit{zVec}\) gives \((P \cdot \operatorname {pauliZ}(\operatorname {inr}(e))).\mathit{zVec}(\operatorname {inl}(v)) = P.\mathit{zVec}(\operatorname {inl}(v)) + 0 = P.\mathit{zVec}(\operatorname {inl}(v))\), and the result follows by simplification.

Assume for contradiction that \(\operatorname {CommutesWithLogical}(P \cdot s)\) holds. We show \(\operatorname {CommutesWithLogical}(P)\), contradicting \(\neg \operatorname {CommutesWithLogical}(P)\). First note that \(P \cdot s \cdot s = P\)by associativity, \(s \cdot s = \operatorname {id}\) (Pauli self-inverse), and \(P \cdot \operatorname {id} = P\). Rewriting the goal using \(P = P \cdot s \cdot s\), the result follows from mul_commuting_preserves_commutesWithLogical applied to \(P \cdot s\) and \(s\).

Suppose \(\operatorname {BoundaryCondition}(G, P, \gamma )\) holds. By boundaryCondition_implies_commutes, \(\operatorname {CommutesWithLogical}(P)\), contradicting the hypothesis.

For the forward direction: assume \(\operatorname {CommutesWithLogical}(P \cdot Q)\). Note that \(P \cdot Q \cdot Q = P\) by associativity, self-inverse (\(Q \cdot Q = \operatorname {id}\)), and the identity law. Rewriting, \(\operatorname {CommutesWithLogical}(P)\) follows from mul_commuting_preserves_commutesWithLogical applied to \(P \cdot Q\) and \(Q\).

For the reverse direction: assume \(\operatorname {CommutesWithLogical}(P)\). Then \(\operatorname {CommutesWithLogical}(P \cdot Q)\) follows directly from mul_commuting_preserves_commutesWithLogical applied to \(P\) and \(Q\).

By the equivalence \(\operatorname {CommutesWithLogical}(P \cdot Q) \iff \operatorname {CommutesWithLogical}(P)\) (from commutesWithLogical_mul_iff using \(\operatorname {CommutesWithLogical}(Q)\)), and rewriting with the hypothesis \(\neg \operatorname {CommutesWithLogical}(P)\), we obtain \(\neg \operatorname {CommutesWithLogical}(P \cdot Q)\).

Suppose \(\operatorname {BoundaryCondition}(G, P \cdot Q, \gamma )\) holds. By boundaryCondition_implies_commutes, \(\operatorname {CommutesWithLogical}(P \cdot Q)\). But by no_modification_helps, \(\neg \operatorname {CommutesWithLogical}(P \cdot Q)\), a contradiction.

Unfolding \(\operatorname {BoundaryCondition}\), both directions follow directly. For the forward direction: given \(\gamma \) and \(h_\gamma \) witnessing the boundary condition, we have \(\operatorname {zSupportOnVertices}(P) \in \operatorname {range}(\partial )\) by the membership criterion \(\langle \gamma , h_\gamma \rangle \). For the reverse direction: given \(\gamma \) and \(h_\gamma \) from the range membership, we obtain the boundary condition \(\langle \gamma , h_\gamma \rangle \).

Rewriting via the equivalence boundaryCondition_exists_iff_in_image, the goal becomes \(\neg \exists \gamma ,\; \operatorname {BoundaryCondition}(G, P, \gamma )\). This follows directly from noncommuting_cannot_be_deformed.