By simplification using the definition of compatibility, this is immediate since \(X = X \land Z = Z\) holds.

By simplification using the definition of compatibility, this is immediate since \(Z = Z \land X = X\) holds.

We perform case analysis on \(p\). In each case (\(I\), \(X\), \(Y\), \(Z\)), simplification using the definition of compatibility shows that neither conflicting conjunction holds.

By simplification using the definition of compatibility, since \(I \neq X\) and \(I \neq Z\).

By simplification using the definition of compatibility, since \(I \neq X\) and \(I \neq Z\).

By unfolding the definition of compatibility, the result follows by propositional tautology: the two conjunctions simply swap the roles of \(p\) and \(q\).

Let \(i\) be an arbitrary qubit index. By hypothesis, \(\mathrm{compatible}(P_i, Q_i)\) holds. Applying the symmetry of compatibility (Lemma 274), we obtain \(\mathrm{compatible}(Q_i, P_i)\).

Let \(i\) be an arbitrary qubit index. The identity operator has Pauli type \(I\) at every position, and \(I\) is compatible with any Pauli type by Lemma 272.

Let \(i\) be an arbitrary qubit index. The identity operator has Pauli type \(I\) at every position, and any Pauli type is compatible with \(I\) by Lemma 273.

Let \(L_1 \in \{ L\} \) and \(L_2 \in \{ L\} \). Since both are singletons, \(L_1 = L\) and \(L_2 = L\). Substituting, for any qubit \(i\), we need \(\mathrm{compatible}(L_i, L_i)\), which holds by self-compatibility (Lemma 271).

Let \(i\) be an arbitrary qubit. We unfold the definition of overlap degree. Then:

where the first inequality holds because filtering a finite set can only reduce its cardinality, and the second inequality is our hypothesis.

Let \(i\) be an arbitrary qubit. We unfold the definition of overlap degree. The filtered set is a subset of \(\{ L\} \), so its cardinality is at most \(|\{ L\} | = 1\).

This follows directly from the fact that \(|\{ L\} | = 1\).

Let \(i\) be an arbitrary qubit index. We consider two cases. If \(i \in \mathrm{support}(L_1.\mathrm{op})\), then by disjointness \(i \notin \mathrm{support}(L_2.\mathrm{op})\). Unfolding the definition of support, \(L_2.\mathrm{op}\) has Pauli type \(I\) at position \(i\). By simplification with \(h_2\), the identity is compatible on the right (Lemma 273). If \(i \notin \mathrm{support}(L_1.\mathrm{op})\), then \(L_1.\mathrm{op}\) has Pauli type \(I\) at position \(i\), and compatibility follows from the identity being compatible on the left (Lemma 272).

Let \(L_1 \in \mathcal{L}\) and \(L_2 \in \mathcal{L}\). We consider whether \(L_1 = L_2\). If \(L_1 = L_2\), then after substitution, for any qubit \(i\) we need \(\mathrm{compatible}(L_{1,i}, L_{1,i})\), which holds by self-compatibility. If \(L_1 \ne L_2\), then by pairwise disjointness they have disjoint support, and the result follows from Lemma 291.

Let \(i\) be an arbitrary qubit. We unfold the definition of overlap degree. Suppose for contradiction that the overlap degree exceeds \(1\). Then \(1 {\lt} |\{ L \in \mathcal{L} \mid i \in \mathrm{support}(L.\mathrm{op})\} |\). By the pigeonhole principle (one-lt-card), there exist distinct \(L_1, L_2\) in the filtered set with \(L_1 \ne L_2\). Extracting membership from the filter, both \(L_1\) and \(L_2\) have \(i\) in their support and belong to \(\mathcal{L}\). By pairwise disjointness, \(\mathrm{support}(L_1.\mathrm{op}) \cap \mathrm{support}(L_2.\mathrm{op}) = \emptyset \). But \(i\) belongs to both supports, hence \(i \in \mathrm{support}(L_1.\mathrm{op}) \cap \mathrm{support}(L_2.\mathrm{op})\), contradicting the intersection being empty.

We take \(P = \mathrm{fromDisjoint}(\mathcal{L}, h)\). By construction, \(P.\mathrm{logicals} = \mathcal{L}\) and \(P.\mathrm{overlapBound} = 1\), both holding by reflexivity.

This follows directly from \(\mathrm{Nat.div\_ mul\_ cancel}\) applied to the divisibility hypothesis \(m \mid d\).

We unfold the definitions of majority threshold and number of parallel measurements. Using the hypothesis \(m {\gt} 0\), the equality \(m = ((2m - 1) + 1) / 2\) follows by integer arithmetic (omega).

This holds by definitional equality (reflexivity).

This holds by definitional equality (reflexivity).

This follows from \(\mathrm{Nat.div\_ self}\) applied to \(d {\gt} 0\), giving \(d / d = 1\).

This holds by definitional equality (reflexivity).

This follows from \(\mathrm{Nat.div\_ one}\), giving \(d / 1 = d\).

We prove both directions separately.

Forward direction: Assume both conditions hold, i.e., we have \(h_{\mathrm{comm}} : \mathrm{CommutativityCondition}(\mathcal{L})\) and \(h_{\mathrm{bound}} : \mathrm{BoundedOverlapCondition}(\mathcal{L}, k)\). We construct \(P\) as the structure \((\mathcal{L}, k, h_{\mathrm{comm}}, h_{\mathrm{bound}})\). Then \(P.\mathrm{logicals} = \mathcal{L}\) and \(P.\mathrm{overlapBound} = k\), both by reflexivity.

Backward direction: Assume there exists \(P\) with \(P.\mathrm{logicals} = \mathcal{L}\) and \(P.\mathrm{overlapBound} = k\). Substituting, the commutativity and bounded overlap conditions are exactly the fields \(P.\mathrm{commutativity}\) and \(P.\mathrm{boundedOverlap}\).

We unfold the definition of \(\mathrm{numParallelMeasurements}\). Using \(m {\gt} 0\), we exhibit the witness \(m - 1\) satisfying \(2m - 1 = 2(m - 1) + 1\), which holds by integer arithmetic (omega).

This follows directly from \(\mathrm{Nat.odd\_ iff.mp}\) applied to the fact that the number of parallel measurements is odd (Lemma 311).