Both equalities hold by reflexivity of definitional computation.

We proceed by case analysis on \(p \in \{ I, X, Y, Z\} \). In each case, the equivalence is verified by simplification using the definitions of \(\mathrm{isNontrivial}\), \(\mathrm{isXType}\), and \(\mathrm{isZType}\).

We proceed by case analysis on both \(p\) and \(q\), each ranging over \(\{ I, X, Y, Z\} \). In each of the 16 cases, the equivalence is verified by simplification using the definition of \(\mathrm{commutes}\).

We proceed by case analysis on \(q \in \{ I, X, Y, Z\} \) and verify each case by simplification using the definitions of \(\mathrm{commutes}\) and \(\mathrm{isZType}\).

We proceed by case analysis on \(q \in \{ I, X, Y, Z\} \) and verify each case by simplification using the definitions of \(\mathrm{commutes}\) and \(\mathrm{isXType}\).

By extensionality, it suffices to show equality for an arbitrary element \(i\). We unfold the definitions of \(\mathrm{anticommutingPositionsWithPureX}\) and \(\mathrm{zSupport}\), expressing both sides using filter and membership in finsets. The equivalence then follows by the tautology that the filter condition on \(S\) combined with the Z-type check is equivalent to membership in \(\mathcal{S}_Z(P) \cap S\).

We unfold the definition of \(\mathrm{commutes}\). The anticommuting positions are exactly those \(i\) where \(P_i\) does not commute with \((\mathrm{pureX}(S))_i\). We establish that

by extensionality. For the forward direction: if \(i \in S\), then \(\mathrm{pureX}(S)_i = X\), and by case analysis on \(P_i \in \{ I, X, Y, Z\} \), the position anticommutes precisely when \(P_i\) is Z-type. If \(i \notin S\), then \(\mathrm{pureX}(S)_i = I\), which commutes with everything, so we get a contradiction. For the reverse direction: given \(P_i\) is Z-type and \(i \in S\), we again case-split on \(P_i\) (the cases \(I\) and \(X\) are excluded by the Z-type assumption) and verify that \(Y\) anticommutes with \(X\) and \(Z\) anticommutes with \(X\). Having established this equality, the result follows by rewriting.

This follows directly from the forward direction of Theorem 112, i.e., \((\mathrm{commutes\_ with\_ pureX\_ iff}\; P\; S).\mathrm{mp}\; h\).

This follows directly from the backward direction of Theorem 112, i.e., \((\mathrm{commutes\_ with\_ pureX\_ iff}\; P\; S).\mathrm{mpr}\; h\).

We use the product representation of \(L\): by \(L.\mathrm{product\_ representation}\), the Pauli components of \(L\) are the same as those of \(\mathrm{pureX}(\mathrm{supp}(L))\). Since the commutation check depends only on the Pauli components (not the phase), we have

Rewriting the hypothesis \(h\) with this equivalence, the result follows directly from Theorem 113 applied to \(P\) and \(\mathrm{supp}(L)\).

From Theorem 116, we obtain \(|\mathcal{S}_Z(P) \cap \mathrm{supp}(L)| \equiv 0 \pmod{2}\). Since \(\mathrm{supp}(L) = \mathrm{Fin}(n)\) by the hypothesis \(\mathrm{hfull}\), we simplify \(\mathcal{S}_Z(P) \cap \mathrm{Fin}(n) = \mathcal{S}_Z(P)\) (using \(\mathrm{Finset.inter\_ univ}\)), yielding \(|\mathcal{S}_Z(P)| \equiv 0 \pmod{2}\).

By case analysis on \(p \in \{ I, X, Y, Z\} \), verified by simplification using the definitions of \(\mathrm{xzExponents}\) and \(\mathrm{isXType}\).

By case analysis on \(p \in \{ I, X, Y, Z\} \), verified by simplification using the definitions of \(\mathrm{xzExponents}\) and \(\mathrm{isZType}\).

We construct the decomposition by verifying both fields. For the X-support correctness: by extensionality on an arbitrary qubit \(i\), we simplify the definitions of \(\mathrm{xSupport}\) and the filter, and the equivalence follows from the symmetric form of Lemma 119 applied to \(P_i\). For the Z-support correctness: similarly, by extensionality and simplification, the equivalence follows from the symmetric form of Lemma 120 applied to \(P_i\).

By extensionality on an arbitrary qubit \(i\). We unfold \(\mathrm{zSupport}\) and \(\mathrm{pureX}\), then split on whether \(i \in S\): if \(i \in S\), then \(\mathrm{pureX}(S)_i = X\), which has \(\mathrm{isZType}(X) = \mathrm{false}\); if \(i \notin S\), then \(\mathrm{pureX}(S)_i = I\), which has \(\mathrm{isZType}(I) = \mathrm{false}\). In either case, \(i\) is not in the Z-type support.

By Theorem 112, it suffices to show \(|\mathcal{S}_Z(\mathrm{pureX}(S)) \cap T| \equiv 0 \pmod{2}\). By Lemma 123, \(\mathcal{S}_Z(\mathrm{pureX}(S)) = \emptyset \), so \(\emptyset \cap T = \emptyset \) which has cardinality \(0\), and \(0 \bmod 2 = 0\).

By extensionality on an arbitrary qubit \(i\). We unfold the definitions of \(\mathrm{xSupport}\) and \(\mathrm{zSupport}\) as filters, and express intersection membership. By case analysis on \(P_i \in \{ I, X, Y, Z\} \): only \(Y\) satisfies both \(\mathrm{isXType}(Y) = \mathrm{true}\) and \(\mathrm{isZType}(Y) = \mathrm{true}\).

By extensionality on an arbitrary qubit \(i\). We unfold the definitions of \(\mathrm{support}\), \(\mathrm{xSupport}\), and \(\mathrm{zSupport}\) as filters and express union membership. By case analysis on \(P_i \in \{ I, X, Y, Z\} \): \(I\) is in neither support (and not in \(\mathrm{supp}(P)\)), \(X\) is in \(\mathcal{S}_X\) only, \(Z\) is in \(\mathcal{S}_Z\) only, and \(Y\) is in both. In all cases, the nontriviality condition for \(\mathrm{supp}(P)\) matches the disjunction.