We unfold the definitions of \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\) and show the sum \(\sum _{v} (P.\mathrm{xVec}(v) \cdot Q.\mathrm{zVec}(v) + P.\mathrm{zVec}(v) \cdot Q.\mathrm{xVec}(v)) = 0\). We apply \(\operatorname {Finset.sum\_ eq\_ zero}\) and consider an arbitrary vertex \(v\). Unfolding the disjointness hypothesis via \(\operatorname {Finset.disjoint\_ left}\), we case-split on whether \(v \in \operatorname {supp}(P)\). If \(v \in \operatorname {supp}(P)\), then by disjointness \(v \notin \operatorname {supp}(Q)\), so \(Q.\mathrm{xVec}(v) = 0\) and \(Q.\mathrm{zVec}(v) = 0\), making the summand zero by simplification. If \(v \notin \operatorname {supp}(P)\), then \(P.\mathrm{xVec}(v) = 0\) and \(P.\mathrm{zVec}(v) = 0\), again making the summand zero.

Let \(i, j \in \operatorname {Fin}(m)\). We case-split on whether \(i = j\). If \(i = j\), then we substitute and apply \(\operatorname {pauliCommute\_ self}\). If \(i \neq j\), then by the pairwise disjointness hypothesis we have \(\operatorname {DisjointSupports}(P_i, P_j)\), and we apply the theorem \(\operatorname {disjoint\_ supports\_ imply\_ commutation}\).

We unfold the definition of \(\operatorname {DisjointSupports}\) and apply the commutativity of the \(\operatorname {Disjoint}\) predicate (\(\operatorname {disjoint\_ comm}\)).

We unfold the definition and simplify using the fact that the support of the identity operator is empty (\(\operatorname {support\_ one}\)).

Let \(v\) be a qubit with \(v \in \operatorname {supp}(P)\) and \(v \in \operatorname {supp}(Q)\). We take the left disjunct: by the same-type X overlap hypothesis, \(P.\mathrm{zVec}(v) = 0\) and \(Q.\mathrm{zVec}(v) = 0\).

Let \(v\) be a qubit with \(v \in \operatorname {supp}(P)\) and \(v \in \operatorname {supp}(Q)\). We take the right disjunct: by the same-type Z overlap hypothesis, \(P.\mathrm{xVec}(v) = 0\) and \(Q.\mathrm{xVec}(v) = 0\).

Let \(v\) be a qubit with \(v \in \operatorname {supp}(P)\) and \(v \in \operatorname {supp}(Q)\). We derive a contradiction: by \(\operatorname {Finset.disjoint\_ left}\) applied to the disjointness hypothesis, \(v \in \operatorname {supp}(P)\) and \(v \in \operatorname {supp}(Q)\) cannot both hold.

We unfold \(\operatorname {PauliCommute}\) and \(\operatorname {symplecticInner}\) and apply \(\operatorname {Finset.sum\_ eq\_ zero}\). For each vertex \(v\), we case-split on whether \(v \in \operatorname {supp}(P)\). If \(v \in \operatorname {supp}(P)\), we further case-split on whether \(v \in \operatorname {supp}(Q)\). If both hold, we obtain from the same-type overlap hypothesis that either (\(P.\mathrm{zVec}(v) = 0\) and \(Q.\mathrm{zVec}(v) = 0\)) or (\(P.\mathrm{xVec}(v) = 0\) and \(Q.\mathrm{xVec}(v) = 0\)). In either case, the cross terms in the symplectic inner product vanish by simplification. If \(v \notin \operatorname {supp}(Q)\), then \(Q.\mathrm{xVec}(v) = 0\) and \(Q.\mathrm{zVec}(v) = 0\), giving zero. If \(v \notin \operatorname {supp}(P)\), then \(P.\mathrm{xVec}(v) = 0\) and \(P.\mathrm{zVec}(v) = 0\), giving zero.

This follows directly from \(\operatorname {gaussLawOp\_ zVec}\).

Let \(v\) be any qubit in both supports. Since \(P.\mathrm{zVec} = 0\) and \(Q.\mathrm{zVec} = 0\) globally, evaluating at \(v\) gives \(P.\mathrm{zVec}(v) = 0\) and \(Q.\mathrm{zVec}(v) = 0\) by congruence.

By the pure X same-type overlap lemma, \(P\) and \(Q\) have same-type X overlap. By the implication from X overlap to same-type overlap, they have same-type overlap. By the theorem that same-type overlap implies commutation, they commute.

We construct a proof that \(P\) and \(Q\) have same-type Z overlap: for any qubit \(v\) in both supports, since \(P.\mathrm{xVec} = 0\) and \(Q.\mathrm{xVec} = 0\) globally, evaluating at \(v\) gives \(P.\mathrm{xVec}(v) = 0\) and \(Q.\mathrm{xVec}(v) = 0\). By the implication from Z overlap to same-type overlap, they have same-type overlap. By the theorem that same-type overlap implies commutation, they commute.

We unfold the definition of \(\operatorname {qubitParticipationCount}\) and apply \(\operatorname {Finset.card\_ le\_ one}\). We must show that if \(i\) and \(j\) are both in the filter (i.e., \(v \in \operatorname {supp}(P_i)\) and \(v \in \operatorname {supp}(P_j)\)), then \(i = j\). Suppose for contradiction that \(i \neq j\). Then by pairwise disjointness, \(\operatorname {supp}(P_i)\) and \(\operatorname {supp}(P_j)\) are disjoint, so by \(\operatorname {Finset.disjoint\_ left}\), \(v\) cannot belong to both—contradiction.

This follows directly from the theorem that disjoint participation is at most 1, applied to each qubit \(v\).

We unfold the definition. The filter of \(\operatorname {Fin}(m)\) has cardinality at most \(|\operatorname {Fin}(m)| = m\) by \(\operatorname {Finset.card\_ filter\_ le}\) and \(\operatorname {Finset.card\_ fin}\).

We unfold the definition and rewrite the cardinalities of the filter sets using \(\operatorname {Finset.card\_ filter}\) as sums of indicator functions (\(\operatorname {Finset.sum\_ boole}\)). We then interchange the order of summation using \(\operatorname {Finset.sum\_ comm}\). The resulting inner sums are shown equal by extensionality and simplification.

This follows directly from the definition of \(\operatorname {ParallelLDPCBound}\) applied to \(v\).

Both components follow directly: pairwise commutation from \(\operatorname {pairwise\_ disjoint\_ implies\_ pairwise\_ commute}\), and the LDPC bound from \(\operatorname {disjoint\_ implies\_ LDPC\_ bound}\).