By extensionality, it suffices to check each component. For each qubit \(q \in V \oplus E\), we case-split on whether \(q\) is a vertex or an edge qubit and simplify using the definition of \(\operatorname {deformedOpExt}\).

By extensionality, it suffices to check each component. For each qubit \(q\), we case-split on whether \(q\) is a vertex or edge qubit and simplify using the definition of \(\operatorname {deformedOpExt}\).

By extensionality, it suffices to verify equality on each qubit \(q \in V \oplus E\).

For the \(\operatorname {xVec}\) component: if \(q = v \in V\), then \((\widetilde{P} \cdot \widetilde{P}).\operatorname {xVec}(v) = P.\operatorname {xVec}(v) + P.\operatorname {xVec}(v) = 0\) by the characteristic-two identity \(a + a = 0\) in \(\mathbb {Z}/2\mathbb {Z}\). If \(q = e \in E\), then \((\widetilde{P} \cdot \widetilde{P}).\operatorname {xVec}(e) = 0 + 0 = 0\), which equals \(\mathbf{1}.\operatorname {xVec}(e)\).

For the \(\operatorname {zVec}\) component: if \(q = v \in V\), then \((\widetilde{P} \cdot \widetilde{P}).\operatorname {zVec}(v) = P.\operatorname {zVec}(v) + P.\operatorname {zVec}(v) = 0\) by the same characteristic-two identity. If \(q = e \in E\), then \((\widetilde{P} \cdot \widetilde{P}).\operatorname {zVec}(e) = \gamma (e) + \gamma (e) = 0\).

Expanding the definition of \(\operatorname {zSupportOnVertices}\), the left-hand side is \(\sum _{v \in V} \mathbf{1}_{P.\operatorname {zVec}(v) \neq 0}\), which by rewriting in terms of the boolean indicator function equals the cardinality of \(\{ v \in V \mid P.\operatorname {zVec}(v) \neq 0\} \) cast to \(\mathbb {Z}/2\mathbb {Z}\).

Unfolding the definition of \(\operatorname {CommutesWithLogical}\), the condition becomes \(\sum _v \operatorname {zSupportOnVertices}(P)(v) = 0\) in \(\mathbb {Z}/2\mathbb {Z}\). By the lemma \(\operatorname {sum\_ zSupportOnVertices\_ eq\_ card}\), this sum equals the cardinality cast to \(\mathbb {Z}/2\mathbb {Z}\). The result then follows from the fact that \(n = 0\) in \(\mathbb {Z}/2\mathbb {Z}\) if and only if \(n\) is even.

Expanding the definition of the boundary map, we have

Swapping the order of summation, it suffices to show that each inner sum \(\sum _{v \in V} \mathbf{1}_{v \in e} \cdot \gamma (e)\) vanishes. We factor out \(\gamma (e)\) to obtain \(\bigl(\sum _{v \in V} \mathbf{1}_{v \in e}\bigr) \cdot \gamma (e)\).

For each edge \(e = \{ a, b\} \) with \(a \neq b\) (since the graph has no loops), we have \(\sum _{v \in V} \mathbf{1}_{v \in \{ a,b\} } = \mathbf{1}_{v=a} + \mathbf{1}_{v=b}\). After evaluating the sum over all vertices, we get the contribution \(1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\), so each edge’s contribution is \(0 \cdot \gamma (e) = 0\). The total sum is therefore \(0\).

Unfolding the definition of \(\operatorname {CommutesWithLogical}\), we need to show \(\sum _v \operatorname {zSupportOnVertices}(P)(v) = 0\). Unfolding the boundary condition \(\partial \gamma = \operatorname {zSupportOnVertices}(P)\), we rewrite the goal as \(\sum _v (\partial \gamma )(v) = 0\). This follows directly from the theorem \(\operatorname {boundary\_ sum\_ eq\_ zero}\).

Expanding the definition of \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\), we need to show

We split the sum over the type \(V \oplus E\).

Vertex contribution: We first establish that

Expanding the definitions of \(\widetilde{P}\) and \(A_v\), the \(A_v.\operatorname {zVec}\) component on vertices is \(0\), so the first term vanishes. The \(A_v.\operatorname {xVec}\) component on vertex \(w\) is \(\mathbf{1}_{w=v}\), so the sum reduces to \(\sum _w P.\operatorname {zVec}(w) \cdot \mathbf{1}_{w=v} = P.\operatorname {zVec}(v)\).

Edge contribution: We establish that

Since \(\widetilde{P}.\operatorname {xVec}(e) = 0\) on edges, the first term vanishes. The second term is \(\gamma (e) \cdot \mathbf{1}_{v \in e}\), which gives the claimed expression after case-splitting on whether \(v \in e\).

Combining: The total symplectic inner product is \(P.\operatorname {zVec}(v) + \sum _e \mathbf{1}_{v \in e} \cdot \gamma (e)\). From the boundary condition, \((\partial \gamma )(v) = \operatorname {zSupportOnVertices}(P)(v)\). Expanding the boundary map, \((\partial \gamma )(v) = \sum _e \mathbf{1}_{v \in e} \cdot \gamma (e)\). Rewriting using the boundary condition, the total becomes \(P.\operatorname {zVec}(v) + \operatorname {zSupportOnVertices}(P)(v)\). If \(P.\operatorname {zVec}(v) = 0\), then \(\operatorname {zSupportOnVertices}(P)(v) = 0\) and the sum is \(0\). If \(P.\operatorname {zVec}(v) \neq 0\), then \(P.\operatorname {zVec}(v) = 1\) and \(\operatorname {zSupportOnVertices}(P)(v) = 1\) in \(\mathbb {Z}/2\mathbb {Z}\), so the sum is \(1 + 1 = 0\) by the characteristic-two identity.

By extensionality, we verify equality on each qubit \(q \in V \oplus E\).

For the \(\operatorname {xVec}\) component: if \(q = v \in V\), then both sides equal \(P.\operatorname {xVec}(v) + Q.\operatorname {xVec}(v)\) by simplification using the definition of \(\operatorname {deformedOpExt}\). If \(q = e \in E\), then both sides equal \(0 + 0 = 0\).

For the \(\operatorname {zVec}\) component: if \(q = v \in V\), then both sides equal \(P.\operatorname {zVec}(v) + Q.\operatorname {zVec}(v)\). If \(q = e \in E\), then both sides equal \(\gamma _1(e) + \gamma _2(e)\) by the pointwise addition of functions.

Expanding the definition, \(\operatorname {zSupportOnVertices}\) is defined using the indicator \(\mathbf{1}_{P.\operatorname {zVec}(v) \neq 0}\), and \(P \cdot Q\) has \(\operatorname {zVec}(v) = P.\operatorname {zVec}(v) + Q.\operatorname {zVec}(v)\). We use the fact that in \(\mathbb {Z}/2\mathbb {Z}\), \(a \neq 0 \iff a = 1\). We then case-split on whether \(P.\operatorname {zVec}(v) = 0\) and \(Q.\operatorname {zVec}(v) = 0\):

• If both are \(0\): both sides are \(0\).

• If \(P.\operatorname {zVec}(v) = 0\) and \(Q.\operatorname {zVec}(v) \neq 0\): left side is \(1\), right side is \(0 + 1 = 1\).

• If \(P.\operatorname {zVec}(v) \neq 0\) and \(Q.\operatorname {zVec}(v) = 0\): left side is \(1\), right side is \(1 + 0 = 1\).

• If both are nonzero: \(P.\operatorname {zVec}(v) + Q.\operatorname {zVec}(v) = 1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\) by the characteristic-two identity, so the left side is \(0\), and the right side is \(1 + 1 = 0\).

Unfolding the boundary condition at both hypotheses, we use the linearity of the boundary map: \(\partial (\gamma _1 + \gamma _2) = \partial \gamma _1 + \partial \gamma _2\). By extensionality, for each vertex \(v\) we compute

using the hypotheses. By the additivity lemma \(\operatorname {zSupportOnVertices\_ mul}\), the right-hand side equals \(\operatorname {zSupportOnVertices}(P \cdot Q)(v)\).

Unfolding the boundary condition, we need \(\partial 0 = \operatorname {zSupportOnVertices}(P)\). Since the boundary map is linear, \(\partial 0 = 0\). The hypothesis gives \(\operatorname {zSupportOnVertices}(P) = 0\), so the two sides are equal by symmetry.