14 Def 5: Gauging Measurement Algorithm
The gauging measurement procedure measures a logical operator \(L = \prod _{v \in V} X_v\) by introducing auxiliary edge qubits, measuring Gauss’s law operators \(A_v\) and edge qubits \(Z_e\), and applying byproduct corrections. We formalize the classical data and processing of the algorithm: measurement outcomes \((\varepsilon _v, \omega _e)\), the sign \(\sigma = \sum _v \varepsilon _v\) (in \(\mathbb {Z}/2\mathbb {Z}\)), the byproduct correction rule based on walk parities, and the commutativity of all measured operators.
We use \(\mathbb {Z}/2\mathbb {Z}\) for measurement outcomes: \(0 \leftrightarrow +1\), \(1 \leftrightarrow -1\). Products of \(\pm 1\) values correspond to sums in \(\mathbb {Z}/2\mathbb {Z}\).
The input data for the gauging measurement procedure consists of:
A connected graph \(G = (V, E)\) with \(V\) the support of the logical operator \(L = \prod _{v \in V} X_v\).
A distinguished base vertex \(v_0 \in V\) for byproduct correction.
A proof that \(G\) is connected.
The measurement outcomes from the gauging procedure. We use \(\mathbb {Z}/2\mathbb {Z}\) to represent \(\pm 1\) outcomes (\(0 \leftrightarrow +1\), \(1 \leftrightarrow -1\)):
\(\varepsilon _v \in \mathbb {Z}/2\mathbb {Z}\): the outcome of measuring Gauss’s law operator \(A_v\) for each \(v \in V\).
\(\omega _e \in \mathbb {Z}/2\mathbb {Z}\): the outcome of measuring \(Z_e\) for each \(e \in E\).
The measurement sign \(\sigma = \sum _{v \in V} \varepsilon _v \in \mathbb {Z}/2\mathbb {Z}\), encoding the product of all Gauss’s law outcomes. This is the measurement result of the logical operator \(L = \prod _{v \in V} X_v\): \(\sigma = 0\) means the \(+1\) eigenvalue, \(\sigma = 1\) means \(-1\).
Given edge measurement outcomes \(\omega \) and a walk \(w\) in \(G\) from \(u\) to \(v\), the walk parity is the \(\mathbb {Z}/2\mathbb {Z}\)-sum of \(\omega (e)\) over all edges \(e\) traversed by the walk:
The walk parity of the trivial (nil) walk at any vertex \(v\) is \(0\).
By simplification using the definition of walk parity and the fact that the nil walk has no darts, the sum is empty and equals \(0\).
For an adjacency \(h : G.\mathrm{Adj}(u, v)\) and a walk \(p\) from \(v\) to \(w\), the walk parity of the extended walk \(\operatorname {cons}(h, p)\) satisfies:
By simplification using the definition of walk parity and the fact that \(\operatorname {darts}(\operatorname {cons}(h, p))\) prepends the dart for edge \(\{ u,v\} \) to \(\operatorname {darts}(p)\), the map and sum decompose as the first term plus the remaining sum.
For walks \(p : u \to v\) and \(q : v \to w\), the walk parity is additive:
We proceed by induction on \(p\).
Base case (\(p = \mathrm{nil}\)): The concatenation \(\mathrm{nil} \cdot q = q\), and \(\operatorname {walkParity}(\omega , \mathrm{nil}) = 0\), so the result follows by simplification.
Inductive step (\(p = \operatorname {cons}(h, p')\)): We have \(\operatorname {cons}(h, p') \cdot q = \operatorname {cons}(h, p' \cdot q)\). Rewriting using the cons formula twice and the inductive hypothesis, we get
which follows by ring arithmetic.
For any walk \(p : u \to v\), reversing the walk does not change its parity:
We proceed by induction on \(p\).
Base case (\(p = \mathrm{nil}\)): Both sides are \(0\) by simplification.
Inductive step (\(p = \operatorname {cons}(h, p')\) where \(h : G.\mathrm{Adj}(a, b)\) and \(p' : b \to c\)): The reverse is \(\operatorname {reverse}(\operatorname {cons}(h, p')) = \operatorname {reverse}(p') \cdot \operatorname {cons}(\bar{h}, \mathrm{nil})\). Rewriting using the append formula, the cons formula, the nil formula, and the inductive hypothesis, we obtain
Since \(\{ b,a\} = \{ a,b\} \) as \(\operatorname {Sym2}\) elements (by \(\operatorname {Sym2.eq\_ swap}\)), the terms match and the result follows by ring arithmetic.
For a single-edge walk along adjacency \(h : G.\mathrm{Adj}(u, v)\),
Rewriting using the cons formula and the nil formula, the result reduces to \(\omega (\{ u,v\} ) + 0 = \omega (\{ u,v\} )\), which holds by \(\operatorname {add\_ zero}\).
For two walks \(p, q : u \to v\), the sum of their parities equals the parity of the closed walk \(p \cdot q^{\mathrm{rev}}\):
Rewriting the right-hand side using the append additivity formula and the reversal invariance, this is immediate.
If all closed walks have zero parity, i.e., \(\operatorname {walkParity}(\omega , c) = 0\) for every closed walk \(c : v \to v\), then for any two walks \(p, q : u \to v\),
Let \(h\) be the hypothesis applied to the closed walk \(p \cdot q^{\mathrm{rev}}\) at vertex \(u\). Rewriting \(h\) using the append additivity and reversal invariance, we obtain \(\operatorname {walkParity}(\omega , p) + \operatorname {walkParity}(\omega , q) = 0\). Since we work in \(\mathbb {Z}/2\mathbb {Z}\), the characteristic-two property (\(a + b = 0 \Rightarrow a = b\)) gives the result.
The byproduct correction at vertex \(v\), given a specific walk \(\gamma \) from \(v_0\) to \(v\), is defined as the walk parity:
Here \(c(v) = 1\) means “apply \(X_v\)” (corresponding to \(\prod _{e \in \gamma } \omega _e = -1\) in \(\pm 1\) notation).
The byproduct correction at the base vertex \(v_0\) using the trivial walk is \(0\):
By simplification using the definition of byproduct correction, this reduces to the walk parity of the nil walk, which is \(0\).
If all closed walks have zero parity, then the byproduct correction at vertex \(v\) is independent of the choice of walk from \(v_0\) to \(v\): for any two walks \(\gamma _1, \gamma _2 : v_0 \to v\),
This follows directly from the well-definedness of walk parity (Theorem 256) applied to \(\gamma _1\) and \(\gamma _2\).
The byproduct correction Pauli operator for a given walk assignment: for each vertex \(v\), apply \(X_v\) if and only if \(c(v) = 1\). Formally, this is the Pauli operator with
The byproduct correction operator has no \(Z\)-component:
This holds by definition (reflexivity), since the \(\mathrm{zVec}\) field is defined to be \(0\).
The byproduct correction operator is self-inverse:
By extensionality, it suffices to show equality for both the \(x\)-vector and \(z\)-vector components for each vertex \(v\).
For the \(x\)-vector: by simplification using the multiplication formula and the identity \(x\)-vector, this reduces to \(c(v) + c(v) = 0\), which holds by the characteristic-two property \(a + a = 0\) in \(\mathbb {Z}/2\mathbb {Z}\).
For the \(z\)-vector: by simplification using the multiplication formula and the fact that \(\mathrm{zVec} = 0\) by definition, this reduces to \(0 + 0 = 0\).
The classical output of the gauging measurement algorithm, consisting of:
The measurement sign \(\sigma \in \mathbb {Z}/2\mathbb {Z}\): \(0 \leftrightarrow +1\) eigenvalue of \(L\), \(1 \leftrightarrow -1\) eigenvalue.
The byproduct correction vector \(c : V \to \mathbb {Z}/2\mathbb {Z}\), where \(c(v) = 1\) means apply \(X_v\).
The gauging measurement algorithm: given input data, measurement outcomes, and a choice of walks from \(v_0\) to each vertex, computes the classical output:
\(\operatorname {sign} = \sum _{v \in V} \varepsilon _v\) (the sum of all Gauss outcomes in \(\mathbb {Z}/2\mathbb {Z}\)).
\(\operatorname {correction}(v) = \operatorname {walkParity}(\gamma _v, \omega )\) (the parity of edge outcomes along the walk from \(v_0\) to \(v\)).
If all closed walks have zero parity, then two different walk choices produce the same correction vector:
By extensionality, it suffices to show equality at each vertex \(v\). This follows directly from the well-definedness of the byproduct correction (Theorem 259) applied to \(\mathrm{walks}_1(v)\) and \(\mathrm{walks}_2(v)\).
The proposition that \(\sigma = 0 \pmod{2}\), meaning the \(+1\) eigenvalue of \(L\) was measured.
The proposition that \(\sigma = 1 \pmod{2}\), meaning the \(-1\) eigenvalue of \(L\) was measured.
The measurement sign is always \(0\) or \(1\) in \(\mathbb {Z}/2\mathbb {Z}\):
This follows from the fact that every element of \(\mathbb {Z}/2\mathbb {Z}\) is either \(0\) or \(1\), which is verified by case analysis (\(\operatorname {fin\_ cases}\)) and simplification.
The Gauss’s law operator measured at vertex \(v\) in step 3 of the gauging procedure:
on the extended qubit system \(V \oplus E\). This is the abbreviation for \(\operatorname {gaussLawOp}(G, v)\).
The edge \(Z\) operator measured at edge \(e\) in step 4 of the gauging procedure:
defined as \(\operatorname {pauliZ}(\operatorname {inr}(e))\).
All Gauss’s law operators commute: for any vertices \(v, w \in V\),
They can be measured in any order in step 3.
This follows directly from the commutativity of Gauss’s law operators (Theorem 117).
All edge \(Z\) operators commute: for any edges \(e_1, e_2 \in E\),
They can be measured in any order in step 4.
By simplification using the definitions of edge \(Z\) operators, Pauli commutation, and the symplectic inner product, the goal reduces to showing a Finset sum equals zero. For each qubit \(q\), the summand involves \(\operatorname {pauliZ}\) which has zero \(x\)-vector, so each term is \(0 \cdot z + x \cdot 0 = 0\). The sum of zeros is zero.
The product of all Gauss’s law operators equals the logical operator \(L = \prod _{v \in V} X_v\):
This is why \(\sigma = \sum _v \varepsilon _v\) gives the measurement result of \(L\).
This follows directly from the Gauss’s law product theorem (Theorem 128).
The edge \(Z\) operator \(Z_e\) has no \(X\)-support:
By simplification using the definitions of the edge \(Z\) operator and \(\operatorname {pauliZ}\), the \(x\)-vector is identically zero.
The Gauss’s law operator \(A_v\) has no \(Z\)-support:
By simplification using the definition of the Gauss’s law operator measured, the \(z\)-vector is identically zero.
Each Gauss’s law operator is self-inverse:
This follows directly from the fact that every Pauli operator is self-inverse (\(P \cdot P = \mathbf{1}\)).
Each edge \(Z\) operator is self-inverse:
This follows directly from the fact that every Pauli operator is self-inverse (\(P \cdot P = \mathbf{1}\)).
I’ll start by reading the Lean file to understand its contents.Now I have a thorough understanding of the file. Let me produce the complete LaTeX translation.