15 Thm 1: Gauging Measurement Correctness
Let \(G\) be a simple graph on vertex set \(V\) with edge set \(E(G)\). Given a binary vector \(c : V \to \mathbb {Z}/2\mathbb {Z}\), define the Pauli operator \(\operatorname {gaussSubsetProduct}(c)\) on the extended qubit system \(V \oplus E(G)\) by:
where \(\delta \) denotes the coboundary map. This represents the product \(\prod _{v \in \operatorname {supp}(c)} A_v\) of Gauss’s law operators, yielding \(X_V(c) \cdot X_E(\delta c)\) on the extended system.
For any binary vector \(c : V \to \mathbb {Z}/2\mathbb {Z}\), the operator \(\operatorname {gaussSubsetProduct}(c)\) is pure \(X\)-type, i.e., its \(Z\)-vector is identically zero.
This holds by definition, since the \(Z\)-vector of \(\operatorname {gaussSubsetProduct}(c)\) is set to \(0\).
The Gauss subset product for the zero vector is the identity operator:
By extensionality, it suffices to show equality of both \(X\)- and \(Z\)-vectors for each qubit. For the \(X\)-vector: if \(q = \operatorname {inl}(v)\), then \(c(v) = 0\) by definition. If \(q = \operatorname {inr}(e)\), we use the fact that \(\delta (0) = 0\) (linearity of the coboundary map), so \((\delta 0)(e) = 0\). For the \(Z\)-vector, both sides are zero by definition.
The Gauss subset product for the all-ones vector equals the logical operator \(L\):
By extensionality, we check each component. For the \(X\)-vector at \(q = \operatorname {inl}(v)\): the Gauss subset product gives \(1\) and the logical operator gives \(1\), so they agree. For \(q = \operatorname {inr}(e)\): we use the fact that the all-ones vector lies in \(\ker (\delta )\) (i.e., \(\delta (\mathbf{1}) = 0\)), which follows from allOnes_mem_ker_coboundary. Rewriting via the kernel membership, we obtain \((\delta \mathbf{1})(e) = 0\), matching the logical operator’s edge component. For the \(Z\)-vector, both are zero.
The Gauss subset product is a group homomorphism: for binary vectors \(c_1, c_2 : V \to \mathbb {Z}/2\mathbb {Z}\),
By extensionality on both components. For the \(X\)-vector at \(q = \operatorname {inl}(v)\): both sides give \((c_1 + c_2)(v) = c_1(v) + c_2(v)\). For \(q = \operatorname {inr}(e)\): by linearity of the coboundary map, \(\delta (c_1 + c_2) = \delta c_1 + \delta c_2\), so the edge components agree. For the \(Z\)-vector: both sides give \(0 + 0 = 0\).
The indicator function of a finset \(S \subseteq V\) as a binary vector:
For any finset \(S \subseteq V\), the product of Gauss’s law operators over \(S\) equals the Gauss subset product of the indicator:
We proceed by induction on \(S\) using finset insertion.
Base case (\(S = \emptyset \)): The empty product is the identity. We show that \(\operatorname {finsetIndicator}(\emptyset ) = 0\) by extensionality (every vertex gives \(0\)), and then \(\operatorname {gaussSubsetProduct}(0) = \mathbf{1}\).
Inductive step: Suppose \(S' = \{ a\} \cup S\) with \(a \notin S\). By the induction hypothesis, \(\prod _{v \in S} A_v = \operatorname {gaussSubsetProduct}(\operatorname {finsetIndicator}(S))\). We rewrite \(\prod _{v \in S'} A_v = A_a \cdot \prod _{v \in S} A_v\) and check equality by extensionality. For the \(X\)-vector at \(\operatorname {inl}(v)\): both sides reduce to \(\operatorname {finsetIndicator}(\{ a\} \cup S)(v)\) by case analysis on whether \(v = a\). For \(\operatorname {inr}(e)\): we decompose the indicator as \(\operatorname {finsetIndicator}(\{ a\} \cup S) = \mathbf{1}_{\{ a\} } + \operatorname {finsetIndicator}(S)\), apply linearity of \(\delta \), and use \(\delta (\mathbf{1}_{\{ a\} }) = \operatorname {coboundaryMap\_ single}\) to match the Gauss operator’s edge component. For the \(Z\)-vector, both sides are zero.
The product of all Gauss’s law operators equals the logical operator:
This follows directly from the Gauss law product theorem (gaussLaw_product).
Two binary vectors \(c, c' : V \to \mathbb {Z}/2\mathbb {Z}\) have the same coboundary if and only if their sum lies in the kernel of \(\delta \):
We prove both directions.
\((\Rightarrow )\): Assume \(\delta c = \delta c'\). By linearity, \(\delta (c + c') = \delta c + \delta c'\). Rewriting with the hypothesis, each component satisfies \(\delta c(e) + \delta c(e) = 0\) by the characteristic-\(2\) identity \(a + a = 0\). Hence \(\delta (c + c') = 0\), so \(c + c' \in \ker (\delta )\).
\((\Leftarrow )\): Assume \(\delta (c + c') = 0\). By linearity, \(\delta c + \delta c' = 0\). For each edge \(e\), we have \(\delta c(e) + \delta c'(e) = 0\), and by the characteristic-\(2\) identity \(a + b = 0 \Rightarrow a = b\), we conclude \(\delta c(e) = \delta c'(e)\). By extensionality, \(\delta c = \delta c'\).
If \(\delta c' = \omega \), then \(\delta c = \omega \) if and only if \(c + c' \in \ker (\delta )\).
Rewriting \(\omega \) as \(\delta c'\) via the hypothesis, this reduces directly to the equivalence \(\delta c = \delta c' \iff c + c' \in \ker (\delta )\).
For a connected graph \(G\), if \(\delta c' = \omega \) and \(\delta c = \omega \), then
where \(\mathbf{1}\) denotes the all-ones vector.
From \(\delta c = \omega = \delta c'\), we obtain \(c + c' \in \ker (\delta )\) by the coboundary preimage shift. Since \(G\) is connected, the kernel classification theorem (ker_coboundary_connected) gives \(c + c' = 0\) or \(c + c' = \mathbf{1}\).
In the first case, for each \(v\) we have \(c(v) + c'(v) = 0\), so \(c(v) = c'(v)\) by the characteristic-\(2\) identity, giving \(c = c'\).
In the second case, \(c(v) + c'(v) = 1\) for all \(v\). Rearranging via \(c(v) = 1 + c'(v) = c'(v) + 1 = (c' + \mathbf{1})(v)\), we get \(c = c' + \mathbf{1}\).
The signed outcome function \(\varepsilon (c)\) for a binary outcome vector \(\varepsilon : V \to \mathbb {Z}/2\mathbb {Z}\) and subset vector \(c : V \to \mathbb {Z}/2\mathbb {Z}\) is:
This encodes the product \(\prod _{v \in \operatorname {supp}(c)} \varepsilon _v\) of \(\pm 1\) outcomes as an additive quantity in \(\mathbb {Z}/2\mathbb {Z}\).
The signed outcome function is a group homomorphism:
Expanding the definition, \(\varepsilon (c_1 + c_2) = \sum _v (c_1(v) + c_2(v)) \cdot \varepsilon (v)\). Distributing the sum gives \(\sum _v c_1(v) \cdot \varepsilon (v) + \sum _v c_2(v) \cdot \varepsilon (v) = \varepsilon (c_1) + \varepsilon (c_2)\), using linearity of addition over the finite sum and the ring identity \((a + b) \cdot c = a \cdot c + b \cdot c\).
The signed outcome for the all-ones vector equals the measurement sign \(\sigma \):
Expanding the definition with \(c = \mathbf{1}\): \(\varepsilon (\mathbf{1}) = \sum _v 1 \cdot \varepsilon (v) = \sum _v \varepsilon (v)\).
For any binary vectors \(\varepsilon \) and \(c'\),
where \(\sigma = \sum _{v \in V} \varepsilon (v)\).
By the additivity of the signed outcome, \(\varepsilon (c' + \mathbf{1}) = \varepsilon (c') + \varepsilon (\mathbf{1})\). Then \(\varepsilon (\mathbf{1}) = \sum _v \varepsilon (v)\) by the all-ones identity.
On vertex qubits, the Pauli operator for subset \(c' + \mathbf{1}\) is the product of the operator for \(c'\) and the logical operator \(L\):
Rewriting via \(\operatorname {gaussSubsetProduct}(\mathbf{1}) = L\) (the all-ones identity), the left-hand side becomes \(\operatorname {gaussSubsetProduct}(c' + \mathbf{1})\), which equals \(\operatorname {gaussSubsetProduct}(c') \cdot \operatorname {gaussSubsetProduct}(\mathbf{1}) = \operatorname {gaussSubsetProduct}(c') \cdot L\) by the additivity of the Gauss subset product.
Given a base vertex \(v_0 \in V\), a family of walks \(\gamma _v : v_0 \leadsto v\) for each \(v \in V\), and an edge outcome vector \(\omega : E(G) \to \mathbb {Z}/2\mathbb {Z}\), the walk parity vector is:
This gives the byproduct correction vector from walk parities.
The walk parity vector at the base vertex \(v_0\) is \(0\), provided \(\gamma _{v_0}\) is the nil walk:
Unfolding the definition of the walk parity vector at \(v_0\), we get \(\operatorname {walkParity}(\omega , \gamma _{v_0})\). Since \(\gamma _{v_0}\) is the nil walk, the walk parity is \(0\).
If all closed walks have zero parity (i.e., \(\operatorname {walkParity}(\omega , c) = 0\) for every closed walk \(c\) at every vertex \(v\)), then for each edge \(e = \{ a, b\} \in E(G)\):
where \(c'\) is the walk parity vector.
Let \(e = \{ a, b\} \) with \(a \sim b\) in \(G\). We construct the closed walk \(p = \gamma _a \cdot (a \to b) \cdot \gamma _b^{-1}\) at \(v_0\). By hypothesis, \(\operatorname {walkParity}(\omega , p) = 0\).
Applying the walk parity append theorem: \(\operatorname {walkParity}(\omega , p) = \operatorname {walkParity}(\omega , \gamma _a) + \operatorname {walkParity}(\omega , (a \to b) \cdot \gamma _b^{-1})\).
Applying the walk parity cons rule: \(\operatorname {walkParity}(\omega , (a \to b) \cdot \gamma _b^{-1}) = \omega (e) + \operatorname {walkParity}(\omega , \gamma _b^{-1})\).
Applying the walk parity reverse rule: \(\operatorname {walkParity}(\omega , \gamma _b^{-1}) = \operatorname {walkParity}(\omega , \gamma _b)\).
Combining: \(c'(a) + (\omega (e) + c'(b)) = 0\). Rearranging in \(\mathbb {Z}/2\mathbb {Z}\): \(c'(a) + c'(b) + \omega (e) = 0\), so \(c'(a) + c'(b) = \omega (e)\). Since \((\delta c')(e) = c'(a) + c'(b)\), we obtain \((\delta c')(e) = \omega (e)\).
The byproduct correction operator equals the pure-\(X\) Pauli operator with \(X\)-vector given by the walk parity vector:
By extensionality on both components. For the \(X\)-vector at vertex \(v\): unfolding the definitions of byproduct correction and walk parity vector, both yield \(\operatorname {walkParity}(\omega , \gamma _v)\). For the \(Z\)-vector: both sides are \(0\).
When all closed walks have zero parity, the walk parity vector \(c'\) satisfies \(\delta c' = \omega \):
By extensionality: for each edge \(e\), the result follows from the per-edge identity established in walkParityVector_coboundary_eq.
The \(\sigma \)-dependent projector pair on vertex qubits, representing the Pauli decomposition of \(\mathbf{1} + \sigma L\):
where the first component is the identity operator and the second has \(X\)-vector \(v \mapsto \sigma \) and \(Z\)-vector \(0\). When \(\sigma = 0\), both components are the identity; when \(\sigma = 1\), the second component is \(L|_V\).
When \(\sigma = 0\), the projector pair is \((\mathbf{1}, \mathbf{1})\), corresponding to \((\mathbf{1} + L)/2\) projecting onto the \(+1\) eigenspace.
Unfolding the definition with \(\sigma = 0\): the first component is \(\mathbf{1}\) by construction. For the second, by extensionality on both \(X\)- and \(Z\)-vectors, the \(X\)-vector gives \(v \mapsto 0\) and the \(Z\)-vector is \(0\), which equals \(\mathbf{1}\).
When \(\sigma = 1\), the second component has \(X\)-vector equal to the all-ones vector, matching \(L\) restricted to vertices:
This holds by definitional equality (reflexivity).
The logical operator \(L\) restricted to vertex qubits only:
i.e., the Pauli operator with \(X\)-vector identically \(1\) and \(Z\)-vector identically \(0\).
The vertex restriction of \(L\) satisfies \(L|_V \cdot L|_V = \mathbf{1}\).
This follows from the general self-inverse property of Pauli operators: \(P \cdot P = \mathbf{1}\) for any Pauli operator \(P\) (since in \(\mathbb {Z}/2\mathbb {Z}\), \(a + a = 0\)).
The byproduct correction operator commutes with \(L|_V\), since both are pure \(X\)-type operators.
The symplectic inner product \(\langle \operatorname {correction}, L|_V \rangle = \sum _v (\operatorname {xVec}_{\mathrm{corr}}(v) \cdot \operatorname {zVec}_{L|_V}(v) + \operatorname {zVec}_{\mathrm{corr}}(v) \cdot \operatorname {xVec}_{L|_V}(v))\). Since \(L|_V\) has \(Z\)-vector \(0\) and the correction has \(Z\)-vector \(0\), every term in the sum is \(0\). Hence the symplectic inner product is \(0\), proving commutativity.
A gauging procedure implements a projective measurement of \(L\) if the following conditions hold:
Sign determination: The measurement sign \(\sigma \) equals \(\sum _{v \in V} \varepsilon _v\), the sum of all Gauss outcomes.
Gauss product: \(\prod _{v \in V} A_v = L\).
Preimage structure: For any \(c'\) with \(\delta c' = \omega \), every \(c\) with \(\delta c = \omega \) satisfies \(c = c'\) or \(c = c' + \mathbf{1}\).
Two terms: \(\operatorname {gaussSubsetProduct}(c' + \mathbf{1}) = \operatorname {gaussSubsetProduct}(c') \cdot L\).
Signed outcome additivity: \(\varepsilon (c' + \mathbf{1}) = \varepsilon (c') + \sigma \).
Walk parity preimage: Under the closed-walk-zero-parity condition, \(\delta (\operatorname {walkParityVector}(\gamma , \omega )) = \omega \).
Correction pure \(X\): The byproduct correction operator has \(Z\)-vector \(0\).
Correction commutes with \(L|_V\): The correction is a pure \(X\)-type operator, hence commutes with \(L|_V\).
Correction self-inverse: Applying the correction twice gives the identity.
Walk independence: Under the closed-walk-zero-parity condition, the walk parity vector is independent of the choice of walks.
If all closed walks have zero parity, then the walk parity vector is independent of the choice of walks: for any two families of walks \(\gamma ^{(1)}_v, \gamma ^{(2)}_v\) from \(v_0\) to \(v\),
By extensionality: for each vertex \(v\), we apply the walk parity well-definedness theorem (walkParity_well_defined), which shows that under the closed-walk-zero-parity hypothesis, \(\operatorname {walkParity}(\omega , \gamma ^{(1)}_v) = \operatorname {walkParity}(\omega , \gamma ^{(2)}_v)\).
(Theorem 1: Gauging Measurement Correctness.) For a connected graph \(G\), the gauging measurement procedure implements a projective measurement of the logical operator \(L = \prod _{v \in V} X_v\).
Given an initial code state \(|\psi \rangle \), the procedure outputs \((\sigma , |\Psi \rangle )\) where:
\(\sigma = \sum _v \varepsilon _v \in \mathbb {Z}/2\mathbb {Z}\) encodes the measurement outcome (\(+1\) or \(-1\)),
The output state satisfies \(|\Psi \rangle \propto (\mathbf{1} + \sigma L)|\psi \rangle \), the projection onto the \(\sigma \)-eigenspace of \(L\).
We verify each condition of the ProjectiveMeasurementOfL structure:
Sign determination: The measurement sign \(\sigma \) equals \(\sum _v \varepsilon _v\) by definition (reflexivity).
Gauss product: \(\prod _{v \in V} A_v = L\) follows directly from the Gauss law product theorem.
Preimage structure: For connected \(G\), if \(\delta c' = \omega \) and \(\delta c = \omega \), then \(c = c'\) or \(c = c' + \mathbf{1}\), as established in the coboundary preimage theorem for connected graphs.
Two terms: \(\operatorname {gaussSubsetProduct}(c' + \mathbf{1}) = \operatorname {gaussSubsetProduct}(c') \cdot L\) follows from the shift identity.
Signed outcome additivity: \(\varepsilon (c' + \mathbf{1}) = \varepsilon (c') + \sigma \) follows from the signed outcome shift.
Walk parity preimage: Under the closed-walk-zero-parity condition, \(\delta c' = \omega \) follows from the walk parity coboundary preimage theorem.
Correction pure \(X\): The \(Z\)-vector of the correction is \(0\) by definition (reflexivity).
Correction commutes with \(L|_V\): Both operators are pure \(X\)-type, so their symplectic inner product vanishes.
Correction self-inverse: This follows from byproductCorrectionOp_mul_self.
Walk independence: Under the closed-walk-zero-parity condition, the walk parity vector is well-defined by walkParityVector_well_defined, which itself relies on walkParity_well_defined.
The effective vertex operator after the gauging procedure equals the projector \(\mathbf{1} + \sigma L\). Specifically, for any binary vectors \(c'\) (the coboundary preimage) and \(\varepsilon \) (the Gauss outcomes), the following hold simultaneously:
\(\operatorname {gaussSubsetProduct}(c')\) restricted to vertex \(X\)-vectors equals \(c'\).
\(\operatorname {gaussSubsetProduct}(c' + \mathbf{1})\) restricted to vertex \(X\)-vectors equals \(c' + \mathbf{1}\).
After byproduct correction (adding \(c'\)), the identity term gives \(c'(v) + c'(v) = 0\) for all \(v\).
After byproduct correction, the \(L\) term gives \((c' + \mathbf{1})(v) + c'(v) = 1\) for all \(v\).
The signed outcomes satisfy \(\varepsilon (c' + \mathbf{1}) = \varepsilon (c') + \sigma \).
Both terms are pure \(X\)-type (have \(Z\)-vector \(0\)).
We verify each component:
(1) By extensionality and simplification of the Gauss subset product definition, the vertex component at \(v\) is \(c'(v)\).
(2) By extensionality and simplification, the vertex component at \(v\) is \((c' + \mathbf{1})(v) = c'(v) + 1\).
(3) For each \(v\), \(c'(v) + c'(v) = 0\) by the characteristic-\(2\) identity \(a + a = 0\).
(4) For each \(v\), \((c'(v) + 1) + c'(v) = 1 + c'(v) + c'(v) = 1 + 0 = 1\), using commutativity of addition, associativity, and the characteristic-\(2\) identity.
(5) This is the signed outcome shift identity: \(\varepsilon (c' + \mathbf{1}) = \varepsilon (c') + \sum _v \varepsilon (v)\).
(6) Both \(Z\)-vectors are \(0\) by definition of the Gauss subset product.
The logical operator is self-inverse: \(L \cdot L = \mathbf{1}\).
This follows from the general Pauli self-inverse property: any Pauli operator \(P\) satisfies \(P \cdot P = \mathbf{1}\) in \(\mathbb {Z}/2\mathbb {Z}\) arithmetic.
The projector \((\mathbf{1} + \sigma L)/2\) is idempotent. At the level of Pauli algebra components:
Hence \((\mathbf{1} + \sigma L) \cdot (\mathbf{1} + \sigma L) = 2(\mathbf{1} + \sigma L)\) since \(\sigma ^2 = 1\) in \(\mathbb {Z}/2\mathbb {Z}\).
The three identities follow from the Pauli self-inverse property (\(L \cdot L = \mathbf{1}\)), the left identity law (\(\mathbf{1} \cdot L = L\)), and the right identity law (\(L \cdot \mathbf{1} = L\)).
The measurement sign is always either \(+1\) or \(-1\): for any gauging outcomes,
This follows directly from the sign dichotomy theorem (sign_dichotomy).
All Gauss’s law measurements are mutually compatible: for any vertices \(v, w \in V\),
This follows directly from gaussLaw_measured_commute.
All edge \(Z\) measurements are mutually compatible: for any edges \(e_1, e_2 \in E(G)\),
This follows directly from edgeZ_measured_commute.
The gauging algorithm is well-defined: the correction operator is independent of the choice of walks. For any two families of walks \(\gamma ^{(1)}, \gamma ^{(2)}\) from the base vertex, under the closed-walk-zero-parity condition:
This follows directly from gaugingAlgorithm_correction_independent.
I’ll start by reading the Lean file to understand its contents.Now I have the full file. Let me produce the LaTeX translation.