MerLean-example

16 Rem 9: Circuit Implementation

The gauging measurement procedure can be implemented by a quantum circuit with no additional qubits beyond the edge qubits. The protocol proceeds as follows:

  1. Initialize each edge qubit \(e\) in state \(|0\rangle _e\).

  2. Apply the entangling circuit \(\prod _v \prod _{e \ni v} \mathrm{CX}_{v \to e}\).

  3. Measure \(X_v\) on all vertex qubits \(v \in V\).

  4. Apply the same entangling circuit again.

  5. Measure \(Z_e\) on all edge qubits and discard them.

  6. Apply byproduct corrections as in Definition 5.

The key insight is that the entangling circuit transforms \(A_v = X_v \prod _{e \ni v} X_e\) into \(X_v\), since \(\mathrm{CX}_{v \to e}\) conjugates \(X_v \mapsto X_v X_e\) and \(X_e \mapsto X_e\). Thus measuring \(X_v\) after the circuit is equivalent to measuring \(A_v\) before it.

16.1 CX Gate Conjugation on Pauli Operators

Definition 315 CX Conjugation
#

Given a qubit space \(W\), a control qubit \(c \in W\), a target qubit \(t \in W\) with \(c \neq t\), and a Pauli operator \(P \in \operatorname {PauliOp}(W)\), the CX conjugation \(\mathrm{CX}_{c \to t}(P)\) is the Pauli operator defined by:

\[ \mathrm{CX}_{c \to t}(P).\mathrm{xVec}(q) = \begin{cases} P.\mathrm{xVec}(q) + P.\mathrm{xVec}(c) & \text{if } q = t, \\ P.\mathrm{xVec}(q) & \text{otherwise,} \end{cases} \]
\[ \mathrm{CX}_{c \to t}(P).\mathrm{zVec}(q) = \begin{cases} P.\mathrm{zVec}(q) + P.\mathrm{zVec}(t) & \text{if } q = c, \\ P.\mathrm{zVec}(q) & \text{otherwise.} \end{cases} \]
Theorem 316 CX Conjugation is Involutive

For any qubit space \(W\), control \(c\), target \(t\) with \(c \neq t\), and Pauli operator \(P \in \operatorname {PauliOp}(W)\),

\[ \mathrm{CX}_{c \to t}(\mathrm{CX}_{c \to t}(P)) = P. \]
Proof

By extensionality, it suffices to show equality of \(\mathrm{xVec}\) and \(\mathrm{zVec}\) for each qubit \(q\). For the \(\mathrm{xVec}\) component: if \(q = t\), then by the definition of CX conjugation,

\[ \mathrm{CX}(\mathrm{CX}(P)).\mathrm{xVec}(t) = (P.\mathrm{xVec}(t) + P.\mathrm{xVec}(c)) + P.\mathrm{xVec}(c) = P.\mathrm{xVec}(t) \]

since \(P.\mathrm{xVec}(c) + P.\mathrm{xVec}(c) = 0\) in \(\mathbb {Z}/2\mathbb {Z}\) by the characteristic-two property. For \(q \neq t\), \(\mathrm{CX}\) acts as the identity, so the result holds by reflexivity.

For the \(\mathrm{zVec}\) component: if \(q = c\), then

\[ \mathrm{CX}(\mathrm{CX}(P)).\mathrm{zVec}(c) = (P.\mathrm{zVec}(c) + P.\mathrm{zVec}(t)) + P.\mathrm{zVec}(t) = P.\mathrm{zVec}(c) \]

by the same characteristic-two cancellation. For \(q \neq c\), the result holds by reflexivity.

Theorem 317 CX Conjugation Distributes over Multiplication

For any Pauli operators \(P, Q \in \operatorname {PauliOp}(W)\),

\[ \mathrm{CX}_{c \to t}(P \cdot Q) = \mathrm{CX}_{c \to t}(P) \cdot \mathrm{CX}_{c \to t}(Q). \]
Proof

By extensionality on each qubit \(q\). For the \(\mathrm{xVec}\) component, we unfold the definitions of CX conjugation and Pauli multiplication. In each case (whether \(q = t\) or \(q \neq t\)), the equality reduces to a ring identity in \(\mathbb {Z}/2\mathbb {Z}\). The \(\mathrm{zVec}\) component follows by the analogous argument, splitting on whether \(q = c\) or \(q \neq c\) and verifying the ring identity in each case.

Theorem 318 CX Maps \(X_c\) to \(X_c \cdot X_t\)

For \(c \neq t\),

\[ \mathrm{CX}_{c \to t}(X_c) = X_c \cdot X_t. \]
Proof

By extensionality on each qubit \(q\). For the \(\mathrm{xVec}\) component: if \(q = t\), then the CX conjugation adds \((\operatorname {pauliX} c).\mathrm{xVec}(c) = 1\) to \((\operatorname {pauliX} c).\mathrm{xVec}(t) = 0\), giving \(1\). The product \(X_c \cdot X_t\) has \(\mathrm{xVec}(t) = 0 + 1 = 1\), so they agree. For \(q \neq t\), CX acts as the identity and the values agree by simplification using \(c \neq t\). For the \(\mathrm{zVec}\) component, \(\operatorname {pauliX}\) has zero \(\mathrm{zVec}\) everywhere, so both sides reduce to \(0\) by simplification.

Theorem 319 CX Fixes \(X_t\)

For \(c \neq t\),

\[ \mathrm{CX}_{c \to t}(X_t) = X_t. \]
Proof

By extensionality on each qubit \(q\). For \(\mathrm{xVec}\): if \(q = t\), then \(\mathrm{CX}_{c \to t}(X_t).\mathrm{xVec}(t) = (\operatorname {pauliX} t).\mathrm{xVec}(t) + (\operatorname {pauliX} t).\mathrm{xVec}(c)\). Since \(c \neq t\), we have \((\operatorname {pauliX} t).\mathrm{xVec}(c) = 0\), so this equals \((\operatorname {pauliX} t).\mathrm{xVec}(t)\). For \(q \neq t\), CX acts as the identity. For \(\mathrm{zVec}\): \(\operatorname {pauliX}\) has zero \(\mathrm{zVec}\), so both sides are \(0\).

Theorem 320 CX Fixes \(Z_c\)

For \(c \neq t\),

\[ \mathrm{CX}_{c \to t}(Z_c) = Z_c. \]
Proof

By extensionality on each qubit \(q\). For \(\mathrm{xVec}\): \(\operatorname {pauliZ}\) has zero \(\mathrm{xVec}\), so both sides are \(0\). For \(\mathrm{zVec}\): if \(q = c\), then \(\mathrm{CX}_{c \to t}(Z_c).\mathrm{zVec}(c) = (\operatorname {pauliZ} c).\mathrm{zVec}(c) + (\operatorname {pauliZ} c).\mathrm{zVec}(t)\). Since \(c \neq t\), we have \((\operatorname {pauliZ} c).\mathrm{zVec}(t) = 0\), and the result follows by simplification. For \(q \neq c\), CX acts as the identity.

Theorem 321 CX Maps \(Z_t\) to \(Z_c \cdot Z_t\)

For \(c \neq t\),

\[ \mathrm{CX}_{c \to t}(Z_t) = Z_c \cdot Z_t. \]
Proof

By extensionality on each qubit \(q\). For \(\mathrm{xVec}\): \(\operatorname {pauliZ}\) has zero \(\mathrm{xVec}\), so both sides are \(0\). For \(\mathrm{zVec}\): if \(q = c\), then \(\mathrm{CX}_{c \to t}(Z_t).\mathrm{zVec}(c) = (\operatorname {pauliZ} t).\mathrm{zVec}(c) + (\operatorname {pauliZ} t).\mathrm{zVec}(t)\). Since \(c \neq t\), this is \(0 + 1 = 1\), and \((Z_c \cdot Z_t).\mathrm{zVec}(c) = 1 + 0 = 1\). For \(q \neq c\), we simplify using the condition \(q \neq c\).

16.2 The Full Entangling Circuit Action

Definition 322 Entangling Circuit Action

Given a graph \(G\) on vertices \(V\) and a Pauli operator \(P \in \operatorname {PauliOp}(\operatorname {ExtQubit}(G))\), the entangling circuit action is the Pauli operator defined by:

\[ \mathrm{EC}(P).\mathrm{xVec}(q) = \begin{cases} P.\mathrm{xVec}(v) & \text{if } q = \operatorname {inl}(v) \text{ for } v \in V, \\ P.\mathrm{xVec}(e) + \sum _{v \in V} [\! [v \in e]\! ] \cdot P.\mathrm{xVec}(v) & \text{if } q = \operatorname {inr}(e) \text{ for } e \in E, \end{cases} \]
\[ \mathrm{EC}(P).\mathrm{zVec}(q) = \begin{cases} P.\mathrm{zVec}(v) + \sum _{e \in \operatorname {inc}(v)} P.\mathrm{zVec}(e) & \text{if } q = \operatorname {inl}(v) \text{ for } v \in V, \\ P.\mathrm{zVec}(e) & \text{if } q = \operatorname {inr}(e) \text{ for } e \in E, \end{cases} \]

where \([\! [v \in e]\! ]\) denotes the indicator for vertex \(v\) being an endpoint of edge \(e\), and \(\operatorname {inc}(v)\) is the set of edges incident to \(v\).

Theorem 323 Entangling Circuit is Involutive

For any Pauli operator \(P \in \operatorname {PauliOp}(\operatorname {ExtQubit}(G))\),

\[ \mathrm{EC}(\mathrm{EC}(P)) = P. \]

That is, applying the entangling circuit twice gives the identity.

Proof

By extensionality on each qubit \(q\). For the \(\mathrm{xVec}\) component, we consider two cases. If \(q = \operatorname {inl}(w)\) for a vertex \(w\), then \(\mathrm{EC}(\mathrm{EC}(P)).\mathrm{xVec}(\operatorname {inl}(w)) = \mathrm{EC}(P).\mathrm{xVec}(\operatorname {inl}(w)) = P.\mathrm{xVec}(\operatorname {inl}(w))\) by the vertex rule applied twice, and the result follows by simplification. If \(q = \operatorname {inr}(e)\) for an edge \(e\), then we use the edge rule twice: the inner application adds a vertex sum, and the outer application adds the same vertex sum again. Since the vertex rule preserves vertex values, we get \(P.\mathrm{xVec}(\operatorname {inr}(e)) + S + S\) where \(S\) is the vertex sum. By the characteristic-two property \(S + S = 0\) in \(\mathbb {Z}/2\mathbb {Z}\), so this equals \(P.\mathrm{xVec}(\operatorname {inr}(e))\).

For the \(\mathrm{zVec}\) component: if \(q = \operatorname {inl}(w)\), the vertex rule applies twice, adding the sum over incident edges in each application. Since the edge rule preserves edge values, we get \(P.\mathrm{zVec}(\operatorname {inl}(w)) + T + T\) where \(T = \sum _{e \in \operatorname {inc}(w)} P.\mathrm{zVec}(\operatorname {inr}(e))\). Again \(T + T = 0\), so the result follows. If \(q = \operatorname {inr}(e)\), the edge rule gives the identity directly.

Theorem 324 Entangling Circuit Distributes over Multiplication

For any Pauli operators \(P, Q \in \operatorname {PauliOp}(\operatorname {ExtQubit}(G))\),

\[ \mathrm{EC}(P \cdot Q) = \mathrm{EC}(P) \cdot \mathrm{EC}(Q). \]
Proof

By extensionality on each qubit \(q\). For the \(\mathrm{xVec}\) component with \(q = \operatorname {inl}(w)\): both sides reduce to \(P.\mathrm{xVec}(\operatorname {inl}(w)) + Q.\mathrm{xVec}(\operatorname {inl}(w))\) by the vertex rule. For \(q = \operatorname {inr}(e)\): the left-hand side is \((P.\mathrm{xVec}(e) + Q.\mathrm{xVec}(e)) + \sum _v [\! [v \in e]\! ] (P.\mathrm{xVec}(v) + Q.\mathrm{xVec}(v))\), and the right-hand side is \((P.\mathrm{xVec}(e) + \sum _v [\! [v \in e]\! ] P.\mathrm{xVec}(v)) + (Q.\mathrm{xVec}(e) + \sum _v [\! [v \in e]\! ] Q.\mathrm{xVec}(v))\). Using the ring identity \((a + b) + (c + d) = (a + c) + (b + d)\) and distributing the sum, the equality follows.

For the \(\mathrm{zVec}\) component with \(q = \operatorname {inl}(w)\): both sides expand using the vertex rule, and the equality follows by the same rearrangement and distributivity of the sum over incident edges. For \(q = \operatorname {inr}(e)\): both sides reduce to \(P.\mathrm{zVec}(\operatorname {inr}(e)) + Q.\mathrm{zVec}(\operatorname {inr}(e))\) by the edge rule.

16.3 Symplectic Inner Product Preservation

For any Pauli operators \(P, Q \in \operatorname {PauliOp}(\operatorname {ExtQubit}(G))\),

\[ \langle \mathrm{EC}(P), \mathrm{EC}(Q) \rangle _{\mathrm{symp}} = \langle P, Q \rangle _{\mathrm{symp}}. \]
Proof

We expand the symplectic inner product \(\langle \mathrm{EC}(P), \mathrm{EC}(Q) \rangle _{\mathrm{symp}} = \sum _q \mathrm{EC}(P).\mathrm{xVec}(q) \cdot \mathrm{EC}(Q).\mathrm{zVec}(q) + \mathrm{EC}(P).\mathrm{zVec}(q) \cdot \mathrm{EC}(Q).\mathrm{xVec}(q)\) and split the sum over qubit type (vertices and edges).

For the vertex contribution, each term expands to \(P.\mathrm{xVec}(v) \cdot (Q.\mathrm{zVec}(v) + \sum _{e \in \operatorname {inc}(v)} Q.\mathrm{zVec}(e)) + (P.\mathrm{zVec}(v) + \sum _{e \in \operatorname {inc}(v)} P.\mathrm{zVec}(e)) \cdot Q.\mathrm{xVec}(v)\). We rearrange this as the “main” term \(P.\mathrm{xVec}(v) \cdot Q.\mathrm{zVec}(v) + P.\mathrm{zVec}(v) \cdot Q.\mathrm{xVec}(v)\) plus a “cross” term involving the sums over incident edges.

For the edge contribution, each term expands to \((P.\mathrm{xVec}(e) + \sum _v [\! [v \in e]\! ] P.\mathrm{xVec}(v)) \cdot Q.\mathrm{zVec}(e) + P.\mathrm{zVec}(e) \cdot (Q.\mathrm{xVec}(e) + \sum _v [\! [v \in e]\! ] Q.\mathrm{xVec}(v))\). We similarly separate this into a main term \(P.\mathrm{xVec}(e) \cdot Q.\mathrm{zVec}(e) + P.\mathrm{zVec}(e) \cdot Q.\mathrm{xVec}(e)\) and a cross term.

The main terms sum to \(\langle P, Q \rangle _{\mathrm{symp}}\), so it suffices to show that the total cross terms vanish.

We expand the vertex cross terms: \(\sum _v \sum _{e \in \operatorname {inc}(v)} (P.\mathrm{xVec}(v) \cdot Q.\mathrm{zVec}(e) + P.\mathrm{zVec}(e) \cdot Q.\mathrm{xVec}(v))\) by distributing the multiplication over the sums. Similarly, the edge cross terms expand to \(\sum _e \sum _v [\! [v \in e]\! ] (P.\mathrm{xVec}(v) \cdot Q.\mathrm{zVec}(e) + P.\mathrm{zVec}(e) \cdot Q.\mathrm{xVec}(v))\).

We rewrite the vertex cross sum by converting the sum over \(e \in \operatorname {inc}(v)\) into a sum over all edges with an indicator function \([\! [v \in e]\! ]\), then swap the summation order. After the swap, the vertex cross sum equals the edge cross sum. Since both are the same element of \(\mathbb {Z}/2\mathbb {Z}\), their sum is \(X + X = 0\) by the characteristic-two property.

Theorem 326 Entangling Circuit Preserves Commutation

For any Pauli operators \(P, Q \in \operatorname {PauliOp}(\operatorname {ExtQubit}(G))\),

\[ \operatorname {PauliCommute}(\mathrm{EC}(P), \mathrm{EC}(Q)) \iff \operatorname {PauliCommute}(P, Q). \]
Proof

We unfold the definition of \(\operatorname {PauliCommute}\) in terms of the symplectic inner product, and rewrite using the fact that the entangling circuit preserves the symplectic inner product.

16.4 Main Theorem: Entangling Circuit Transforms \(A_v\) to \(X_v\)

Theorem 327 Entangling Circuit Transforms \(A_v\) to \(X_v\)

For every vertex \(v \in V\),

\[ \mathrm{EC}(A_v) = X_v, \]

where \(A_v = \operatorname {gaussLawOp}(G, v)\) is the Gauss law operator and \(X_v = \operatorname {pauliX}(\operatorname {inl}(v))\).

Proof

By extensionality on each qubit \(q\).

For the \(\mathrm{xVec}\) component: if \(q = \operatorname {inl}(w)\) for a vertex \(w\), then \(\mathrm{EC}(A_v).\mathrm{xVec}(\operatorname {inl}(w))\) equals \(A_v.\mathrm{xVec}(\operatorname {inl}(w))\) by the vertex rule, which equals \([\! [w = v]\! ]\) by the definition of \(A_v\), matching \((\operatorname {pauliX}(\operatorname {inl}(v))).\mathrm{xVec}(\operatorname {inl}(w))\).

If \(q = \operatorname {inr}(e)\) for an edge \(e\), then \(\mathrm{EC}(A_v).\mathrm{xVec}(\operatorname {inr}(e))\) equals \(A_v.\mathrm{xVec}(\operatorname {inr}(e)) + \sum _w [\! [w \in e]\! ] \cdot A_v.\mathrm{xVec}(\operatorname {inl}(w))\). By the definition of \(A_v\), the first term is \([\! [v \in e]\! ]\) and the sum \(\sum _w [\! [w \in e]\! ] \cdot [\! [w = v]\! ]\) simplifies to \([\! [v \in e]\! ]\) (by evaluating the sum with the Kronecker delta). Thus the total is \([\! [v \in e]\! ] + [\! [v \in e]\! ] = 0\) in \(\mathbb {Z}/2\mathbb {Z}\), matching the right-hand side \((\operatorname {pauliX}(\operatorname {inl}(v))).\mathrm{xVec}(\operatorname {inr}(e)) = 0\).

For the \(\mathrm{zVec}\) component: if \(q = \operatorname {inl}(w)\), then since \(A_v\) has zero \(\mathrm{zVec}\), we get \(0 + \sum _{e \in \operatorname {inc}(w)} 0 = 0\), matching \((\operatorname {pauliX}).\mathrm{zVec} = 0\). If \(q = \operatorname {inr}(e)\), then \(\mathrm{EC}(A_v).\mathrm{zVec}(\operatorname {inr}(e)) = A_v.\mathrm{zVec}(\operatorname {inr}(e)) = 0\).

Theorem 328 Entangling Circuit Transforms \(X_v\) to \(A_v\)

For every vertex \(v \in V\),

\[ \mathrm{EC}(X_v) = A_v. \]
Proof

Rewriting the goal using the fact that \(\mathrm{EC}(A_v) = X_v\), it suffices to show \(\mathrm{EC}(\mathrm{EC}(A_v)) = A_v\). This follows directly from the involutivity of the entangling circuit action.

Theorem 329 Measuring \(X_v\) After Circuit Equals Measuring \(A_v\)

For every vertex \(v \in V\),

\[ \mathrm{EC}(A_v) = X_v. \]

That is, measuring \(X_v\) in the entangled frame is equivalent to measuring the Gauss law operator \(A_v\) in the original frame.

Proof

This follows directly from the theorem that the entangling circuit transforms \(A_v\) to \(X_v\).

16.5 Effect on Edge \(Z\) Operators

For an edge \(e \in E(G)\), the entangling circuit transforms \(Z_e\) into the operator with \(\mathrm{xVec} = 0\) and

\[ \mathrm{zVec}(q) = \begin{cases} [\! [w \in e]\! ] & \text{if } q = \operatorname {inl}(w), \\[\! [e' = e]\! ]& \text{if } q = \operatorname {inr}(e’). \end{cases} \]

That is, \(\mathrm{EC}(Z_e)\) acts as \(Z\) on the edge \(e\) and on both its endpoint vertices.

Proof

By extensionality on each qubit \(q\).

For the \(\mathrm{xVec}\) component: both vertex and edge cases give \(0\), since \(\operatorname {pauliZ}\) has zero \(\mathrm{xVec}\) and the vertex sums involve zero terms.

For the \(\mathrm{zVec}\) component with \(q = \operatorname {inl}(w)\): we compute \(\mathrm{EC}(Z_e).\mathrm{zVec}(\operatorname {inl}(w)) = (\operatorname {pauliZ}(\operatorname {inr}(e))).\mathrm{zVec}(\operatorname {inl}(w)) + \sum _{e' \in \operatorname {inc}(w)} (\operatorname {pauliZ}(\operatorname {inr}(e))).\mathrm{zVec}(\operatorname {inr}(e'))\). The first term is \(0\) (since \(\operatorname {inl}(w) \neq \operatorname {inr}(e)\)), and the sum \(\sum _{e' \in \operatorname {inc}(w)} [\! [e' = e]\! ]\) equals \([\! [e \in \operatorname {inc}(w)]\! ]\). By the characterization of incident edges, \(e \in \operatorname {inc}(w)\) if and only if \(w \in e\), so this gives \([\! [w \in e]\! ]\) as required.

For the \(\mathrm{zVec}\) component with \(q = \operatorname {inr}(e')\): by the edge rule, \(\mathrm{EC}(Z_e).\mathrm{zVec}(\operatorname {inr}(e')) = (\operatorname {pauliZ}(\operatorname {inr}(e))).\mathrm{zVec}(\operatorname {inr}(e')) = [\! [e' = e]\! ]\).

16.6 Circuit Protocol Steps

Theorem 331 Step 2: Circuit Transforms \(A_v\) to \(X_v\)

For every vertex \(v \in V\),

\[ \mathrm{EC}(A_v) = X_v. \]
Proof

This follows directly from the key result that the entangling circuit transforms \(A_v\) to \(X_v\).

Theorem 332 Step 4: Applying Circuit Twice is Identity

For any Pauli operator \(P\),

\[ \mathrm{EC}(\mathrm{EC}(P)) = P. \]
Proof

This follows directly from the involutivity of the entangling circuit action.

Theorem 333 Steps 2+3+4: Measuring \(X_v\) in CX Frame Equals Measuring \(A_v\)

For every vertex \(v \in V\),

\[ \mathrm{EC}(X_v) = A_v. \]
Proof

This follows directly from the inverse direction of the circuit transformation.

Theorem 334 Edge Measurements Return to Original Frame

For any edge \(e \in E(G)\),

\[ \mathrm{EC}(\mathrm{EC}(Z_e)) = Z_e. \]

After applying the entangling circuit a second time (step 4), edge \(Z\) measurements are back in the original frame.

Proof

This follows directly from the involutivity of the entangling circuit action applied to \(Z_e\).

16.7 Simultaneous Transformation and Consistency

Theorem 335 All Gauss Operators Simultaneously Transform to \(X_v\)

For all vertices \(v \in V\) simultaneously,

\[ \mathrm{EC}(A_v) = X_v. \]
Proof

Let \(v\) be an arbitrary vertex. The result follows directly from the key transformation theorem applied to each \(v\).

Theorem 336 Product of Transformed Operators Equals Logical Operator

The product of all vertex \(X\) operators equals the logical operator:

\[ \prod _{v \in V} X_v = L, \]

where \(L = \operatorname {logicalOp}(G)\).

Proof

By extensionality on each qubit \(q\).

For the \(\mathrm{xVec}\) component: we rewrite the product’s \(\mathrm{xVec}\) as a sum over all vertices using the product formula for Pauli operators. If \(q = \operatorname {inl}(w)\) for a vertex \(w\), then \(\sum _v (\operatorname {pauliX}(\operatorname {inl}(v))).\mathrm{xVec}(\operatorname {inl}(w)) = \sum _v [\! [w = v]\! ]\). Evaluating using the indicator sum identity \(\sum _{v \in V} [\! [w = v]\! ] = 1\) (since \(w \in V\)), this gives \(1\), which matches \(\operatorname {logicalOp}(G).\mathrm{xVec}(\operatorname {inl}(w)) = 1\). If \(q = \operatorname {inr}(e)\) for an edge \(e\), then \(\sum _v (\operatorname {pauliX}(\operatorname {inl}(v))).\mathrm{xVec}(\operatorname {inr}(e)) = 0\) since \(\operatorname {inl}(v) \neq \operatorname {inr}(e)\) for all \(v\), matching \(\operatorname {logicalOp}(G).\mathrm{xVec}(\operatorname {inr}(e)) = 0\).

For the \(\mathrm{zVec}\) component: we rewrite the product’s \(\mathrm{zVec}\) as a sum. Since \(\operatorname {pauliX}\) has zero \(\mathrm{zVec}\), the sum is \(0\) for all qubits, matching \(\operatorname {logicalOp}(G).\mathrm{zVec} = 0\).

Theorem 337 Entangling Circuit Preserves Logical Operator

The entangling circuit fixes the logical operator:

\[ \mathrm{EC}(L) = L. \]
Proof

By extensionality on each qubit \(q\).

For the \(\mathrm{xVec}\) component: if \(q = \operatorname {inl}(w)\), then \(\mathrm{EC}(L).\mathrm{xVec}(\operatorname {inl}(w)) = L.\mathrm{xVec}(\operatorname {inl}(w))\) by the vertex rule and the result follows by simplification. If \(q = \operatorname {inr}(e)\) for an edge \(e\), then \(\mathrm{EC}(L).\mathrm{xVec}(\operatorname {inr}(e)) = L.\mathrm{xVec}(\operatorname {inr}(e)) + \sum _v [\! [v \in e]\! ] \cdot L.\mathrm{xVec}(\operatorname {inl}(v))\). Since \(L.\mathrm{xVec}(\operatorname {inr}(e)) = 0\) and \(L.\mathrm{xVec}(\operatorname {inl}(v)) = 1\) for all \(v\), this equals \(\sum _v [\! [v \in e]\! ]\). Writing \(e = \{ a, b\} \) with \(a \neq b\) (since \(G\) has no loops), we compute \(\sum _v [\! [v \in e]\! ] = [\! [a \in e]\! ] + [\! [b \in e]\! ] = 1 + 1 = 0\) in \(\mathbb {Z}/2\mathbb {Z}\), matching \(L.\mathrm{xVec}(\operatorname {inr}(e)) = 0\).

For the \(\mathrm{zVec}\) component: since \(L.\mathrm{zVec} = 0\) everywhere, both vertex and edge cases give \(0\).