37 Rem 14: Generalizations of the Gauging Measurement Procedure
This remark describes four directions in which the gauging measurement procedure generalizes beyond Pauli stabilizer codes:
Finite group representations: The procedure applies to any representation of a finite group by operators with a tensor product factorization, not necessarily the logical operators of a quantum error-correcting code.
Non-Pauli operators: The gauging measurement can measure non-Pauli operators, whose measurement can produce magic states (e.g., measurement of Clifford operators in a topological code).
Qudit systems: The procedure extends to qudit systems with \(d {\gt} 2\) levels per site.
Nonabelian groups: The generalization extends to nonabelian groups, but for nonabelian groups, measuring the charge locally does not fix a definite global charge (unlike the abelian case).
The key mathematical distinction is that in abelian groups, products are order-independent (so local measurements determine the global outcome), while in nonabelian groups they are not.
For a commutative group \(G\) and any function \(\mathrm{charges} : \mathrm{Fin}(n) \to G\) and any permutation \(\sigma \) of \(\mathrm{Fin}(n)\),
This is the key property that allows local measurements to determine the global charge.
By rewriting using the fact that composing a product with a permutation \(\sigma \) yields the same result in a commutative group (Equiv.prod_comp), the two products are equal.
For a commutative group \(G\), any function \(\mathrm{charges} : \mathrm{Fin}(n) \to G\), and any two permutations \(\sigma _1, \sigma _2\) of \(\mathrm{Fin}(n)\),
Let \(h_1\) be the result of applying the abelian product order-independence theorem to \(\sigma _1\), and \(h_2\) the result for \(\sigma _2\). Rewriting using both \(h_1\) and \(h_2\), the two permuted products are both equal to the canonical product \(\prod _i \mathrm{charges}(i)\), and hence equal to each other.
The symmetric group \(S_3\) on \(3\) elements is nonabelian: there exist permutations \(a, b \in S_3\) such that \(a \cdot b \neq b \cdot a\).
Define \(\mathrm{swap01}\) to be the transposition \((0\ 1)\) and \(\mathrm{cycle012} = (0\ 2) \circ (0\ 1)\) to be the \(3\)-cycle \((0\ 1\ 2)\). We claim these do not commute. Suppose for contradiction that \(\mathrm{swap01} \cdot \mathrm{cycle012} = \mathrm{cycle012} \cdot \mathrm{swap01}\). Evaluating both sides at \(0\): on the left-hand side, \(\mathrm{swap01}(\mathrm{cycle012}(0)) = 0\) (verified by computation), and on the right-hand side, \(\mathrm{cycle012}(\mathrm{swap01}(0)) = 2\) (verified by computation). Applying the assumed equality at \(0\) gives \(0 = 2\), which is a contradiction by decidable computation.
For a (not necessarily abelian) group \(G\), if there exist elements \(a, b \in G\) such that \(a \cdot b \neq b \cdot a\), then there exist elements \(g_1, g_2 \in G\) whose products differ based on order: \(g_1 \cdot g_2 \neq g_2 \cdot g_1\).
This follows directly from the hypothesis: the witnesses \(a, b\) with \(ab \neq ba\) are exactly the desired \(g_1, g_2\).
There exist permutations \(a, b \in S_3\) such that \(a \cdot b \neq b \cdot a\).
This follows directly from the theorem that \(S_3\) is nonabelian.
For a nonabelian group \(G\) (i.e., one in which there exist \(a, b \in G\) with \(ab \neq ba\)), there exists a function \(\mathrm{charges} : \mathrm{Fin}(2) \to G\) such that
This is why, for nonabelian groups, local measurements do not fix a definite global charge.
From the hypothesis, we obtain elements \(a, b \in G\) with \(ab \neq ba\). Define \(\mathrm{charges}(i) = a\) if \(i = 0\) and \(\mathrm{charges}(i) = b\) otherwise. Simplifying the conditional expressions using the fact that \(1 \neq 0\) in \(\mathrm{Fin}(2)\), the statement \(\mathrm{charges}(0) \cdot \mathrm{charges}(1) \neq \mathrm{charges}(1) \cdot \mathrm{charges}(0)\) reduces to \(ab \neq ba\), which holds by assumption.
A qudit system with local dimension \(d\) and \(n\) sites has total Hilbert space dimension
For any \(n\), \(\mathrm{quditTotalDimension}(2, n) = 2^n\).
This holds by reflexivity (definitional equality).
For any \(n\), \(\mathrm{quditTotalDimension}(3, n) = 3^n\).
This holds by reflexivity (definitional equality).
For any \(d \geq 2\) and \(n {\gt} 0\), the qudit system has positive dimension:
By simplification using the definition of \(\mathrm{quditTotalDimension}\), the goal reduces to showing \(d^n {\gt} 0\). Since \(d \geq 2\), we have \(d {\gt} 0\) (by integer arithmetic), and the result follows from the fact that a positive natural number raised to any power is positive (Nat.pow_pos).
For any \(d {\gt} 2\) and \(n {\gt} 0\), the qudit system has positive dimension:
This confirms the procedure extends to qudits with \(d {\gt} 2\).
We apply qudit_positive_dimension with the bound \(d \geq 2\), which follows from \(d {\gt} 2\) by \(d {\gt} 2 \Rightarrow d \geq 2\) (Nat.le_of_lt), together with the hypothesis \(n {\gt} 0\).
The four directions of generalization for the gauging procedure form an inductive type with constructors:
finiteGroupReps: Any finite group representation with tensor product factorization.
nonPauliOperators: Non-Pauli operators (which can produce magic states).
quditSystems: Qudit systems with \(d {\gt} 2\) levels per site.
nonabelianGroups: Nonabelian groups (with a local-vs-global caveat).
The function \(\mathrm{procedureApplies} : \mathrm{GeneralizationDirection} \to \mathrm{Bool}\) returns true for all four generalization directions, indicating that the gauging procedure applies in each case.
The function \(\mathrm{hasLocalGlobalCaveat} : \mathrm{GeneralizationDirection} \to \mathrm{Bool}\) returns true only for the nonabelian groups direction, indicating that only in this case do local measurements fail to determine the global charge.
For every generalization direction \(\mathrm{dir}\), \(\mathrm{procedureApplies}(\mathrm{dir}) = \mathrm{true}\).
We case-split on \(\mathrm{dir}\). In each of the four cases (finiteGroupReps, nonPauliOperators, quditSystems, nonabelianGroups), the result holds by reflexivity.
For any generalization direction \(\mathrm{dir}\),
We case-split on \(\mathrm{dir}\) and simplify using the definition of \(\mathrm{hasLocalGlobalCaveat}\). In each of the four cases, the biconditional reduces to a trivially decidable proposition.