2 Rem 2: Graph Convention
This chapter formalizes the graph convention for the gauging measurement protocol. Given a connected graph \(G = (V_G, E_G)\), we identify vertices with qubits in the support of a logical operator \(L\). Each edge receives an auxiliary gauge qubit initialized in \(\ket {0}\), and dummy vertices (those outside \(\operatorname {supp}(L)\)) receive auxiliary qubits initialized in \(\ket {+}\). The key property is that dummy vertices do not affect the measurement outcome, since measuring \(X\) on \(\ket {+}\) always returns \(+1\).
An inductive type classifying the different types of qubits involved in the gauging measurement protocol:
LogicalSupport: Original code qubits in the support of \(L\).
EdgeQubit: Auxiliary gauge qubits on edges, initialized in \(\ket {0}\).
DummyQubit: Auxiliary qubits for dummy vertices, initialized in \(\ket {+}\).
An inductive type representing the possible initial quantum states for qubits:
zero: The \(\ket {0}\) state (computational basis zero).
plus: The \(\ket {+}\) state, i.e., \((\ket {0} + \ket {1})/\sqrt{2}\).
encoded: Unspecified state (for logical qubits, determined by the encoding).
The function assigning an initial state to each qubit type:
\(\mathrm{LogicalSupport} \mapsto \mathrm{encoded}\) (state determined by the code encoding),
\(\mathrm{EdgeQubit} \mapsto \mathrm{zero}\) (initialized in \(\ket {0}\)),
\(\mathrm{DummyQubit} \mapsto \mathrm{plus}\) (initialized in \(\ket {+}\)).
An inductive type representing possible measurement outcomes for \(X\)-basis measurements:
plus: Outcome \(+1\).
minus: Outcome \(-1\).
A function converting a measurement outcome to a sign \((\pm 1)\) as an integer: \(\mathrm{plus} \mapsto 1\) and \(\mathrm{minus} \mapsto -1\).
Multiplication of measurement outcomes, corresponding to the product of signs:
The result of measuring \(X\) on the \(\ket {+}\) state is defined to be \(\mathrm{plus}\) (i.e., outcome \(+1\)), since \(\ket {+}\) is the \(+1\) eigenstate of the Pauli \(X\) operator.
The \(X\) measurement on the \(\ket {+}\) state always returns the \(\mathrm{plus}\) outcome:
This holds by definitional equality (reflexivity).
A structure capturing the deterministic outcome property of measuring \(X\) on \(\ket {+}\). It consists of:
A state \(\mathrm{is\_ plus\_ state}\) of type \(\mathrm{InitialState}\),
A proof that \(\mathrm{is\_ plus\_ state} = \mathrm{plus}\),
An outcome of type \(\mathrm{GraphMeasurementOutcome}\),
A proof that \(\mathrm{outcome} = \mathrm{plus}\).
A gauging graph convention specifies how a connected graph \(G\) relates to the logical operator \(L\) being measured. It consists of:
A vertex type \(V\) with a \(\mathrm{Fintype}\) instance and decidable equality,
A simple graph structure on \(V\) with decidable adjacency,
A proof that the graph is connected,
A finite set \(\mathrm{logicalSupport} \subseteq V\) representing the support of \(L\),
A proof that \(\mathrm{logicalSupport}\) is nonempty (i.e., \(L\) is nontrivial).
This captures the conventions: (1) vertices of \(G\) are identified with qubits in \(\operatorname {supp}(L)\), (2) each edge \(e \in E_G\) gets an auxiliary gauge qubit in \(\ket {0}\), (3) dummy vertices (\(V_G \setminus \operatorname {supp}(L)\)) get auxiliary qubits in \(\ket {+}\), and (4) dummy vertices have no effect on the measurement outcome.
A vertex \(v\) of a gauging graph \(G\) is a support vertex if \(v \in \mathrm{logicalSupport}(G)\).
A vertex \(v\) of a gauging graph \(G\) is a dummy vertex if \(v \notin \mathrm{logicalSupport}(G)\).
Every vertex \(v\) of a gauging graph \(G\) is either a support vertex or a dummy vertex:
We consider whether \(v \in \mathrm{logicalSupport}(G)\). If \(v \in \mathrm{logicalSupport}(G)\), then the left disjunct holds. If \(v \notin \mathrm{logicalSupport}(G)\), then the right disjunct holds.
Support and dummy vertex classifications are mutually exclusive:
Assume both \(G.\mathrm{isSupportVertex}(v)\) and \(G.\mathrm{isDummyVertex}(v)\) hold. Decomposing this conjunction, we have \(v \in \mathrm{logicalSupport}(G)\) (from the support hypothesis) and \(v \notin \mathrm{logicalSupport}(G)\) (from the dummy hypothesis). This is a contradiction.
The set of dummy vertices of a gauging graph \(G\) is defined as
The number of dummy vertices is \(|\mathrm{dummyVertices}(G)|\).
The vertices of a gauging graph partition into support and dummy vertices:
We first establish that \(V_G = \mathrm{logicalSupport}(G) \cup \mathrm{dummyVertices}(G)\). By extensionality, it suffices to show that for an arbitrary vertex \(v\), \(v \in V_G\) if and only if \(v \in \mathrm{logicalSupport}(G) \cup \mathrm{dummyVertices}(G)\). Simplifying, since every \(v\) is in the universal set, we apply the vertex classification theorem: either \(v\) is a support vertex (left case) or \(v\) is a dummy vertex (right case, using the definition of \(\mathrm{dummyVertices}\) and that \(v \in V_G\)).
Next, we establish that \(\mathrm{logicalSupport}(G)\) and \(\mathrm{dummyVertices}(G)\) are disjoint. By the disjointness criterion for finite sets, suppose \(a \in \mathrm{logicalSupport}(G)\) and \(b \in \mathrm{dummyVertices}(G)\) with \(a = b\). Substituting, the membership in \(\mathrm{dummyVertices}\) (after simplification using its filter definition) gives \(a \notin \mathrm{logicalSupport}(G)\), contradicting \(a \in \mathrm{logicalSupport}(G)\).
Finally, we compute:
where the last step uses the cardinality formula for disjoint unions.
The qubit type assigned to each vertex \(v\) of a gauging graph \(G\):
If \(v\) is a support vertex, then \(\mathrm{vertexQubitType}(v) = \mathrm{LogicalSupport}\).
By simplification using the definition of \(\mathrm{vertexQubitType}\) and the hypothesis that \(v\) is a support vertex, the conditional reduces to the \(\mathrm{LogicalSupport}\) branch.
If \(v\) is a dummy vertex, then \(\mathrm{vertexQubitType}(v) = \mathrm{DummyQubit}\).
Unfolding the definitions of \(\mathrm{vertexQubitType}\) and \(\mathrm{isSupportVertex}\), and simplifying using the negation of membership (from the dummy vertex hypothesis), the conditional evaluates to \(\mathrm{DummyQubit}\).
All edges are assigned the \(\mathrm{EdgeQubit}\) type: for any edge \(e \in E_G\),
The initial state for a vertex qubit \(v\) is determined by its qubit type:
The initial state for an edge qubit is always \(\ket {0}\):
Dummy vertex qubits are initialized in \(\ket {+}\): if \(v\) is a dummy vertex of \(G\), then
Unfolding the definition of \(\mathrm{vertexInitialState}\), we rewrite using the fact that \(\mathrm{vertexQubitType}(v) = \mathrm{DummyQubit}\) (by the dummy vertex qubit type theorem). Then \(\mathrm{initialState}(\mathrm{DummyQubit}) = \mathrm{plus}\) holds by reflexivity.
For any edge \(e\), the edge initial state is \(\ket {0}\):
This holds by definitional equality (reflexivity).
The measurement outcome for a dummy vertex is defined to be \(\mathrm{plus}\) (i.e., \(+1\)), since the dummy qubit is in \(\ket {+}\), which is the \(+1\) eigenstate of \(X\).
Measuring \(X\) on any dummy vertex returns \(+1\):
This holds by definitional equality (reflexivity).
The product of measurement outcomes over any set of dummy vertices equals \(1\):
Let \(S\) be given and assume all vertices in \(S\) are dummy vertices. The product \(\prod _{v \in S} 1 = 1\) follows by simplification using the fact that the product of the constant \(1\) over any finite set equals \(1\).
The number of edges \(|E_G|\) in the gauging graph, which equals the number of gauge qubits.
The total number of auxiliary qubits is the sum of edge qubits and dummy qubits:
The total number of qubits involved in the gauging protocol is the sum of logical support qubits and auxiliary qubits:
The total number of qubits can be expanded as:
By simplification using the definitions of \(\mathrm{totalQubits}\) and \(\mathrm{numAuxiliaryQubits}\), the goal reduces to
which follows by integer arithmetic (associativity of addition).
The effective logical support when gauging \(L\) with dummy vertices is the entire vertex set \(V_G\). This captures the convention that we gauge the operator \(L \cdot \prod _{v \in \mathrm{dummy}} X_v\):
The effective logical support equals the universal set of vertices:
This holds by definitional equality (reflexivity).
The original logical support is contained in the effective logical support:
Let \(v \in \mathrm{logicalSupport}(G)\). By simplification using the definition of \(\mathrm{effectiveLogicalSupport}\), the goal is \(v \in \mathrm{univ}\), which holds since every element belongs to the universal set.
The main theorem of this remark: dummy vertices have no effect on the gauging measurement outcome. For any finite set of dummy vertices, the product of their contributions is \(1\):
Let \(S\) be a set of vertices and assume \(\forall v \in S\), \(G.\mathrm{isDummyVertex}(v)\). We first establish that for each \(v \in S\), the conditional expression \((\text{if } G.\mathrm{isDummyVertex}(v) \text{ then } 1 \text{ else } 0) = 1\). This follows by simplification using the hypothesis \(G.\mathrm{isDummyVertex}(v)\), which makes the conditional evaluate to \(1\).
Rewriting the product using this pointwise equality (via \(\mathrm{Finset.prod\_ congr}\)), we obtain \(\prod _{v \in S} 1 = 1\), which holds by the fact that the product of the constant \(1\) over any finite set equals \(1\).
The contribution of each dummy vertex to the measurement outcome is the neutral element: for any dummy vertex \(v\),
Let \(v\) be a vertex and \(h_v\) a proof that \(v\) is a dummy vertex. By simplification using the definitions of \(\mathrm{dummyVertexMeasurementOutcome}\) (which equals \(\mathrm{plus}\)) and \(\mathrm{plus\_ toSign}\) (which equals \(1\)), we obtain the result.