6 Rem 6: Circuit Implementation of the Gauging Procedure
The gauging procedure can be implemented by a quantum circuit with no additional ancilla qubits beyond the edge qubits. After initializing the edge qubits in \(\ket {0}\), one performs the entangling circuit \(\prod _v \prod _{e \ni v} \mathrm{CX}_{v \to e}\), where \(\mathrm{CX}_{v \to e}\) is a controlled-\(X\) gate with control qubit \(v\) and target qubit \(e\). Next, one projectively measures \(X_v\) on all vertices \(v \in G\) and keeps the post-measurement state. Then one repeats the same entangling circuit \(\prod _v \prod _{e \ni v} \mathrm{CX}_{v \to e}\). Finally, one measures \(Z_e\) on all edge qubits and discards them.
A controlled-\(X\) gate specification for a qubit type \(Q\) consists of:
a control qubit \(c \in Q\),
a target qubit \(t \in Q\),
a proof that \(c \neq t\).
The circuit phases of the gauging circuit are defined as the inductive type with five constructors:
InitializeEdges: Initialize edge qubits in \(\ket {0}\).
FirstEntangling: Apply the first entangling circuit \(\prod _v \prod _{e \ni v} \mathrm{CX}_{v \to e}\).
MeasureXVertices: Measure \(X_v\) on all vertices.
SecondEntangling: Apply the second entangling circuit (identical to the first).
MeasureZEdges: Measure \(Z_e\) on all edges and discard.
The natural ordering of circuit phases is given by the function \(\mathrm{toNat} : \mathrm{CircuitPhase} \to \mathbb {N}\) defined by:
The number of circuit phases is exactly \(5\):
This holds by reflexivity (definitional equality).
For all circuit phases \(p\),
We case-split on \(p\). In each case, \(\mathrm{toNat}(\texttt{InitializeEdges}) = 0 \leq \mathrm{toNat}(p)\), which follows by simplification using the definition of \(\mathrm{toNat}\).
For all circuit phases \(p\),
We case-split on \(p\). In each case, \(\mathrm{toNat}(p) \leq 4 = \mathrm{toNat}(\texttt{MeasureZEdges})\), which follows by simplification using the definition of \(\mathrm{toNat}\).
Given a simple graph \(G = (V, E)\) with decidable adjacency, the entangling circuit \(\prod _v \prod _{e \ni v} \mathrm{CX}_{v \to e}\) is a structure consisting of:
the underlying graph \(G\),
a gate specification: for each vertex \(v \in V\) and each edge \(e\) in the incidence set of \(v\), a \(\mathrm{CX}\) gate with control \(\mathrm{inl}(v) \in V \oplus \mathrm{Sym}_2(V)\) and target \(\mathrm{inr}(e) \in V \oplus \mathrm{Sym}_2(V)\).
For any entangling circuit associated to a graph \(G\),
This follows directly from the handshaking lemma (SimpleGraph.sum_degrees_eq_twice_card_edges).
For any vertex \(v \in V\),
This follows directly from SimpleGraph.card_incidenceFinset_eq_degree.
An \(X\)-measurement specification for a qubit type \(Q\) consists of:
a finite set \(\mathcal{Q} \subseteq Q\) of qubits to measure in the Pauli-\(X\) basis,
a function \(\mathrm{keep} : Q \to \mathrm{Bool}\) indicating whether to keep each qubit after measurement.
A \(Z\)-measurement specification for a qubit type \(Q\) consists of:
a finite set \(\mathcal{Q} \subseteq Q\) of qubits to measure in the Pauli-\(Z\) basis,
a function \(\mathrm{keep} : Q \to \mathrm{Bool}\) indicating whether to keep each qubit after measurement.
The complete gauging circuit for a simple graph \(G = (V,E)\) is a structure consisting of:
the underlying graph \(G\),
a first entangling circuit \(\mathcal{E}_1\) of type \(\mathrm{EntanglingCircuit}(G)\),
an \(X\)-measurement specification on the vertices \(V\),
a second entangling circuit \(\mathcal{E}_2\) of type \(\mathrm{EntanglingCircuit}(G)\),
a \(Z\)-measurement specification on the edge set \(\mathrm{Sym}_2(V)\),
subject to the following conditions:
\(\mathcal{E}_1 = \mathcal{E}_2\) (the two entangling circuits are identical),
the \(X\)-measurement covers all vertices: \(\mathrm{qubits} = V\),
the \(X\)-measurement keeps all qubits: \(\mathrm{keep}(v) = \mathrm{true}\) for all \(v\),
the \(Z\)-measurement covers all edges: \(\mathrm{qubits} = E_G\),
the \(Z\)-measurement discards all qubits: \(\mathrm{keep}(e) = \mathrm{false}\) for all \(e\).
For any gauging circuit \(C\), the two entangling circuits are identical:
This follows directly from the field entangling_identical of the gauging circuit structure.
For any gauging circuit \(C\) and any edge \(e \in E_G\), the initial state of the edge qubit is \(\ket {0}\):
This holds by reflexivity (definitional equality from the \(\mathrm{initialState}\) function).
For any gauging circuit \(C\),
This follows directly from the field x_covers_all.
For any gauging circuit \(C\) and vertex \(v\),
This follows directly from the field x_keeps.
For any gauging circuit \(C\),
This follows directly from the field z_covers_all.
For any gauging circuit \(C\) and edge \(e \in \mathrm{Sym}_2(V)\),
This follows directly from the field z_discards.
The circuit qubit type for a graph \(G = (V,E)\) is an inductive type with two constructors:
\(\mathrm{vertex}(v)\) for \(v \in V\): an original code (vertex) qubit,
\(\mathrm{edge}(e)\) for \(e \in \mathrm{Sym}_2(V)\): an auxiliary (edge) qubit.
The set of all qubits used in a gauging circuit \(C\) for graph \(G\) is
For any gauging circuit \(C\) and any qubit \(q \in \mathrm{allQubits}(C)\), either
That is, every qubit in the circuit is either a vertex qubit or an edge qubit; no additional ancilla qubits are required.
Let \(q \in \mathrm{allQubits}(C)\). By simplification using the definition of \(\mathrm{allQubits}\), membership in the union, and membership in the image, we know that \(q\) belongs to the image of \(\mathrm{vertex}\) over \(V\) or the image of \(\mathrm{edge}\) over \(E_G\). We consider two cases:
Case 1 (\(q\) is in the vertex image): We obtain a vertex \(v\) such that \(q = \mathrm{vertex}(v)\). The left disjunct holds with witness \(v\).
Case 2 (\(q\) is in the edge image): We obtain an edge \(e\) and a proof \(e \in E_G\) such that \(q = \mathrm{edge}(e)\). The right disjunct holds with witnesses \(e\) and the membership proof.
A circuit qubit \(q\) is an edge qubit if it has the form \(\mathrm{edge}(e)\) for some \(e\). Formally,
For any gauging circuit \(C\),
By extensionality, it suffices to show membership equivalence for an arbitrary qubit \(q\). We simplify using the definitions of \(\mathrm{allQubits}\), membership in filtered sets, union, image, and \(\mathrm{isEdge}\).
\((\Rightarrow )\): Suppose \(q \in \mathrm{allQubits}(C)\) and \(\mathrm{isEdge}(q) = \mathrm{true}\). We case-split on \(q\):
If \(q = \mathrm{vertex}(v)\), then \(\mathrm{isEdge}(q) = \mathrm{false}\), contradicting the filter condition.
If \(q = \mathrm{edge}(e)\), we case-split on membership in \(\mathrm{allQubits}\). If \(q\) came from the vertex image, we obtain \(v\) with \(\mathrm{vertex}(v) = \mathrm{edge}(e)\), which is absurd by the injectivity of constructors. If \(q\) came from the edge image, we directly obtain the desired membership.
\((\Leftarrow )\): Suppose there exists \(e \in E_G\) with \(q = \mathrm{edge}(e)\). Then \(q\) is in the right component of the union in \(\mathrm{allQubits}(C)\), and substituting \(q = \mathrm{edge}(e)\) gives \(\mathrm{isEdge}(q) = \mathrm{true}\) by reflexivity.
The circuit consists of exactly five phases:
This follows directly from CircuitPhase.num_phases.
The five phases execute in strict order:
By simplification using the definition of \(\mathrm{toNat}\), this reduces to \(0 {\lt} 1 \land 1 {\lt} 2 \land 2 {\lt} 3 \land 3 {\lt} 4\), which follows by integer arithmetic.
Given a simple graph \(G = (V,E)\), the default gauging circuit \(\mathrm{mkGaugingCircuit}(G)\) is the gauging circuit where:
both entangling circuits use \(\mathrm{CX}\) gates with \(\mathrm{control} = \mathrm{inl}(v)\) and \(\mathrm{target} = \mathrm{inr}(e)\) for each vertex-edge incidence pair,
the \(X\)-measurement covers all vertices with \(\mathrm{keep} = \mathrm{true}\),
the \(Z\)-measurement covers all edges of \(G\) with \(\mathrm{keep} = \mathrm{false}\).
All required conditions (identical entangling circuits, full coverage, keep/discard properties) hold by reflexivity.
The circuit sequence is the ordered list of circuit phases:
The circuit sequence has length \(5\):
This holds by reflexivity.
The circuit sequence is pairwise strictly increasing in phase order.
This is verified by computation (the decide tactic).
The number of CX gates in one round of the entangling circuit for a graph \(G = (V,E)\) is
For any graph \(G\),
Unfolding the definition of \(\mathrm{numCXGates}\), this reduces to \(\sum _{v \in V} \deg (v) = 2|E|\), which follows from the handshaking lemma (sum_degrees_eq_twice_card_edges).
The total number of CX gates in the full gauging circuit (both entangling rounds) is
For any graph \(G\),
Unfolding the definition of \(\mathrm{totalCXGates}\), we have \(\mathrm{totalCXGates}(G) = 2 \cdot \mathrm{numCXGates}(G)\). Rewriting using the result \(\mathrm{numCXGates}(G) = 2|E|\), we obtain \(2 \cdot 2|E| = 4|E|\), which follows by integer arithmetic.