Assume \(p \neq q\) and the adjacency condition holds. Since \(p \neq q\) implies \(q \neq p\), it remains to check the disjunction. If the edge is a pairing edge \((\operatorname {inl}(i), \operatorname {inr}(i))\), then \((\operatorname {inr}(i), \operatorname {inl}(i))\) is also a pairing edge (by the second disjunct). If the edge is a reverse pairing edge \((\operatorname {inr}(i), \operatorname {inl}(i))\), then \((\operatorname {inl}(i), \operatorname {inr}(i))\) is a pairing edge. If the edge is a dummy subgraph edge with \(G_{\mathrm{dummy}}.\operatorname {Adj}(i, j)\), then by symmetry of \(G_{\mathrm{dummy}}\) we have \(G_{\mathrm{dummy}}.\operatorname {Adj}(j, i)\).

Suppose \(\operatorname {shorGraphAdj}(W, G_{\mathrm{dummy}}, p, p)\) holds. By definition, the first condition requires \(p \neq p\), which is a contradiction.

By the cardinality of a sum type, \(|\operatorname {Fin}(W) \oplus \operatorname {Fin}(W)| = |\operatorname {Fin}(W)| + |\operatorname {Fin}(W)| = W + W = 2W\).

We have \(\operatorname {inl}(i) \neq \operatorname {inr}(i)\) (they are in different summands), and \(i\) witnesses the pairing edge condition \(p = \operatorname {inl}(i) \land q = \operatorname {inr}(i)\).

We must show \(\operatorname {inr}(i) \neq \operatorname {inr}(j)\) and the adjacency condition. For the first, if \(\operatorname {inr}(i) = \operatorname {inr}(j)\) then \(i = j\) by injectivity of \(\operatorname {inr}\), but \(G_{\mathrm{dummy}}\) is loopless so \(i \sim i\) is impossible. For the second, we produce witnesses \(i, j\) with \(G_{\mathrm{dummy}}.\operatorname {Adj}(i, j)\).

Fix a base vertex \(\operatorname {inr}(0)\). It suffices to show that every vertex \(w\) is reachable from \(\operatorname {inr}(0)\).

Case \(w = \operatorname {inr}(j)\): Since \(G_{\mathrm{dummy}}\) is connected, vertex \(0\) is reachable from \(j\) in \(G_{\mathrm{dummy}}\). Applying the graph homomorphism \(\operatorname {shorDummyHom}\) (which maps via \(\operatorname {inr}\)), \(\operatorname {inr}(0)\) is reachable from \(\operatorname {inr}(j)\) in the Shor graph.

Case \(w = \operatorname {inl}(i)\): By the same argument, \(\operatorname {inr}(0)\) can reach \(\operatorname {inr}(i)\) in the Shor graph. The pairing edge gives \(\operatorname {inr}(i) \sim \operatorname {inl}(i)\), so \(\operatorname {inr}(0)\) can reach \(\operatorname {inl}(i)\) by transitivity.

The graph is nonempty since \(W {\gt} 0\) guarantees \(\operatorname {inr}(0)\) exists.

This holds by definition, since \(\operatorname {zVec}\) is defined to be \(0\).

This follows from the fact that every Pauli operator is self-inverse: \(P \cdot P = \mathbf{1}\).

Since \(\operatorname {xVec}(v) = 1 \neq 0\) for all \(v\), every vertex is in the support of \(L'\). The support filter returns all of \(\operatorname {univ}\), so the weight equals \(|\operatorname {Fin}(W) \oplus \operatorname {Fin}(W)| = W + W = 2W\).

By extensionality, we check each component. For \(\operatorname {xVec}\): on \(\operatorname {inl}(i)\), \(1 = 1 + 0\); on \(\operatorname {inr}(i)\), \(1 = 0 + 1\). For \(\operatorname {zVec}\): on all vertices, \(0 = 0 + 0\). Each case follows by simplification of the multiplication definition.

This holds by definition.

This holds by definition.

Both operators are pure \(X\)-type, so they commute by the commutativity of Pauli operator multiplication.

This follows from the general self-inverse property of Pauli operators.

This follows from the general self-inverse property of Pauli operators.

Decompose the sum over the sum type: \(\sum _{v} f(v) = \sum _{i} f(\operatorname {inl}(i)) + \sum _{j} f(\operatorname {inr}(j))\). Since each dummy outcome \(\varepsilon _{\operatorname {inr}(j)} = 0\) by hypothesis, the second sum vanishes, leaving only \(\sum _i \varepsilon _{\operatorname {inl}(i)}\).

By extensionality and simplification of the \(\operatorname {gaussLawOp}\) definition, every component of the \(\operatorname {zVec}\) is \(0\).

This follows directly by symmetry from \(\operatorname {gaussLaw\_ product}(\operatorname {ShorGraph}(W, G_{\mathrm{dummy}}))\).

This is a direct application of the general \(\operatorname {entanglingCircuit\_ transforms\_ gaussLaw}\) theorem to the Shor graph.

This is a direct application of \(\operatorname {entanglingCircuit\_ transforms\_ pauliX\_ to\_ gaussLaw}\) to the Shor graph.

This is a direct application of \(\operatorname {entanglingCircuitAction\_ involutive}\) to the Shor graph.

This is the symmetric form of \(\operatorname {entanglingCircuit\_ preserves\_ commutation}\) applied to the Shor graph.

Suppose \(\operatorname {inl}(i) \sim \operatorname {inl}(j)\). Decomposing the adjacency disjunction: a pairing edge would require \(\operatorname {inl}(j) = \operatorname {inr}(k)\), which contradicts the type; a reverse pairing edge requires \(\operatorname {inl}(i) = \operatorname {inr}(k)\), another contradiction; a dummy subgraph edge requires \(\operatorname {inl}(i) = \operatorname {inr}(a)\), again a contradiction. All cases are impossible.

(\(\Rightarrow \)) If \(\operatorname {inl}(i) \sim \operatorname {inr}(j)\), then among the three disjuncts, only the pairing edge case is consistent with the types: there exists \(k\) with \(\operatorname {inl}(i) = \operatorname {inl}(k)\) and \(\operatorname {inr}(j) = \operatorname {inr}(k)\), giving \(i = k = j\).

(\(\Leftarrow \)) If \(i = j\), substitute and apply \(\operatorname {shor\_ pairing\_ edge}\).

(\(\Rightarrow \)) If \(\operatorname {inr}(i) \sim \operatorname {inr}(j)\), then among the disjuncts, only the dummy subgraph case is type-consistent: there exist \(a, b\) with \(\operatorname {inr}(i) = \operatorname {inr}(a)\), \(\operatorname {inr}(j) = \operatorname {inr}(b)\), and \(G_{\mathrm{dummy}}.\operatorname {Adj}(a, b)\). By injectivity, \(i = a\) and \(j = b\), so \(G_{\mathrm{dummy}}.\operatorname {Adj}(i, j)\).

(\(\Leftarrow \)) Apply \(\operatorname {shor\_ dummy\_ edge}\).

By extensionality, a vertex \(q\) is in the neighbor set if and only if \(q = \operatorname {inr}(i)\). For \(q = \operatorname {inl}(j)\), adjacency is impossible by the no-support-support-edges theorem. For \(q = \operatorname {inr}(j)\), adjacency holds if and only if \(i = j\) by the support-dummy characterization, so \(q = \operatorname {inr}(i)\).

By the neighbor set characterization, the neighbor set is \(\{ \operatorname {inr}(i)\} \), which has cardinality \(1\).

By extensionality. For a vertex \(q\): if \(q = \operatorname {inl}(j)\), then \(\operatorname {inr}(i) \sim \operatorname {inl}(j)\) iff \(j = i\) (by symmetry and the support-dummy characterization), corresponding to membership in \(\{ \operatorname {inl}(i)\} \). If \(q = \operatorname {inr}(j)\), then \(\operatorname {inr}(i) \sim \operatorname {inr}(j)\) iff \(G_{\mathrm{dummy}}.\operatorname {Adj}(i, j)\) (by the dummy-dummy characterization), corresponding to \(j \in N_{G_{\mathrm{dummy}}}(i)\). The disjointness of the two parts follows because \(\operatorname {inl}(i) \neq \operatorname {inr}(j)\) for all \(j\).

This follows directly by case analysis on the adjacency disjunction from the definition of \(\operatorname {shorGraphAdj}\).

This is a direct application of \(\operatorname {gaussLaw\_ commute}\) to the Shor graph.

This follows from the general self-inverse property of Pauli operators.

This is a direct application of \(\operatorname {gaussLaw\_ product}\) to the Shor graph.

This is a conjunction of previously proved results: connectivity from \(\operatorname {shorGraph\_ connected}\), vertex count from \(\operatorname {shorGraph\_ card}\), commutation from \(\operatorname {shor\_ gauss\_ operators\_ commute}\), self-inverseness from \(\operatorname {shor\_ gauss\_ self\_ inverse}\), the product formula from \(\operatorname {shor\_ product\_ measurement}\), and degree from \(\operatorname {shor\_ support\_ degree\_ eq\_ one}\).

By the neighbor set characterization, the neighbor set of \(\operatorname {inr}(i)\) is \(\{ \operatorname {inl}(i)\} \cup \operatorname {inr}(N_{G_{\mathrm{dummy}}}(i))\). These two sets are disjoint (different summands), so the cardinality is \(1 + |N_{G_{\mathrm{dummy}}}(i)| = 1 + \deg _{G_{\mathrm{dummy}}}(i)\).

Since each support vertex has degree \(1\), the sum is \(\sum _{i} 1 = W\).

Substituting \(\deg (\operatorname {inr}(i)) = 1 + \deg _{G_{\mathrm{dummy}}}(i)\) and distributing the sum: \(\sum _i (1 + \deg _{G_{\mathrm{dummy}}}(i)) = \sum _i 1 + \sum _i \deg _{G_{\mathrm{dummy}}}(i) = W + \sum _i \deg _{G_{\mathrm{dummy}}}(i)\).

This is the handshaking lemma applied to the Shor graph.

This follows from the decomposition of sums over a sum type: \(\sum _{v \in A \oplus B} f(v) = \sum _{a \in A} f(\operatorname {inl}(a)) + \sum _{b \in B} f(\operatorname {inr}(b))\).

This is the standard graph-theoretic fact that a connected graph on \(n\) vertices has at least \(n-1\) edges.

By the dummy degree formula, \(\deg (\operatorname {inr}(i)) = 1 + \deg _{G_{\mathrm{dummy}}}(i) \le 1 + d = d + 1\).

We consider two cases. If \(v = \operatorname {inl}(i)\), then \(\deg (v) = 1 \le d + 1\) (since \(d \ge 0\)). If \(v = \operatorname {inr}(i)\), the bound follows from \(\operatorname {shor\_ dummy\_ degree\_ bound}\).

Rewriting: \(2|E| = \sum _v \deg (v)\) by the handshaking lemma. Then decompose the sum as \(\sum _{\operatorname {inl}} + \sum _{\operatorname {inr}} = W + (W + \sum _i \deg _{G_{\mathrm{dummy}}}(i))\) using the previously established support and dummy degree sums.

This is the standard handshaking lemma for \(G_{\mathrm{dummy}}\).