Documentation

QEC1.Remarks.Rem_14_Generalizations

Rem_14: Generalizations of the Gauging Measurement Procedure #

Statement #

The gauging measurement procedure generalizes beyond Pauli stabilizer codes:

  1. Finite group representations: The procedure can be applied to any representation of a finite group by operators that have a tensor product factorization. The representation need not form the logical operators of a quantum error-correcting code.

  2. Non-Pauli operators: The gauging measurement can measure non-Pauli operators, whose measurement can produce magic states. An example is the measurement of Clifford operators in a topological code.

  3. Qudit systems: The procedure extends to qudit systems with d > 2 levels per site.

  4. Nonabelian groups: The generalization extends to nonabelian groups. However, for nonabelian groups, measuring the charge locally does not fix a definite global charge (unlike the abelian case where local measurements determine the global outcome).

Main Results #

Approach #

This remark describes conceptual generalizations rather than stating theorems. We formalize the key mathematical distinction: in abelian groups products are order-independent, while in nonabelian groups they are not. This captures the essence of point 4.

Section 1: Abelian Groups - Product is Order Independent #

For abelian groups, the product ∏_v g_v is well-defined regardless of the order of multiplication. This means local measurement outcomes uniquely determine the global charge.

source
theorem QEC1.Generalizations.abelian_product_order_independent {G : Type u_1} [CommGroup G] [Fintype G] {n : ℕ} (charges : Fin n → G) (σ : Equiv.Perm (Fin n)) :
∏ i : Fin n, charges i = ∏ i : Fin n, charges (σ i)

For abelian (commutative) groups, the product of elements is independent of order. This is the key property that allows local measurements to determine global charge.

source
theorem QEC1.Generalizations.abelian_any_two_orderings_equal {G : Type u_1} [CommGroup G] [Fintype G] {n : ℕ} (charges : Fin n → G) (σ₁ σ₂ : Equiv.Perm (Fin n)) :
∏ i : Fin n, charges (σ₁ i) = ∏ i : Fin n, charges (σ₂ i)

Specifically, for any two permutations of the same elements, the product is equal.

Section 2: Nonabelian Groups - Product Depends on Order #

For nonabelian groups, the product depends on the order of multiplication. This means local measurement outcomes do NOT uniquely determine the global charge. We demonstrate this with a concrete example using the symmetric group S₃.

source
theorem QEC1.Generalizations.S3_nonabelian :
∃ (a : Equiv.Perm (Fin 3)) (b : Equiv.Perm (Fin 3)), a * b ≠ b * a

The symmetric group S₃ on 3 elements is nonabelian.

source
theorem QEC1.Generalizations.nonabelian_product_order_dependent {G : Type u_1} [Group G] (h_nonab : ∃ (a : G) (b : G), a * b ≠ b * a) :
∃ (g₁ : G) (g₂ : G), g₁ * g₂ ≠ g₂ * g₁

For a nonabelian group, there exist elements whose products differ based on order. This is the mathematical content of "local measurements don't fix global charge".

source
theorem QEC1.Generalizations.S3_order_matters :
∃ (a : Equiv.Perm (Fin 3)) (b : Equiv.Perm (Fin 3)), a * b ≠ b * a

Concrete demonstration: In S₃, we can find two elements that give different products depending on multiplication order.

source
theorem QEC1.Generalizations.nonabelian_different_orderings_different_results {G : Type u_1} [Group G] (h_nonab : ∃ (a : G) (b : G), a * b ≠ b * a) :
∃ (charges : Fin 2 → G), charges 0 * charges 1 ≠ charges 1 * charges 0

For a function assigning group elements to sites, different orderings give different products in a nonabelian group.

Section 3: Qudit Systems #

The procedure extends to qudit systems with d > 2 levels per site. The key point is that the dimension d ≥ 2 is a parameter, not fixed to 2.

source
def QEC1.Generalizations.quditTotalDimension (d n : ℕ) :
ℕ

A qudit system has local dimension d ≥ 2. The total Hilbert space dimension is d^n.

Equations
Instances For
    source
    theorem QEC1.Generalizations.qubit_is_d_equals_2 (n : ℕ) :
    quditTotalDimension 2 n = 2 ^ n

    Qubits are the special case d = 2.

    source
    theorem QEC1.Generalizations.qutrit_is_d_equals_3 (n : ℕ) :
    quditTotalDimension 3 n = 3 ^ n

    Qutrits are the case d = 3.

    source
    theorem QEC1.Generalizations.qudit_positive_dimension {d n : ℕ} (hd : d ≥ 2) (_hn : n > 0) :
    quditTotalDimension d n > 0

    For any d ≥ 2, the qudit system has positive dimension (when n > 0).

    source
    theorem QEC1.Generalizations.qudit_extension_valid {d n : ℕ} (hd : d > 2) (hn : n > 0) :
    quditTotalDimension d n > 0

    The procedure extends to qudits: d > 2 still gives positive dimension.

    Section 4: Summary of Generalizations #

    The four generalizations and their key properties:

    1. Finite group representations: Any finite group G with tensor-factorized representation works.
    2. Non-Pauli operators: Can measure Clifford and more general operators (may produce magic states).
    3. Qudit systems: d > 2 works just as well as d = 2.
    4. Nonabelian groups: Procedure extends, but local ↛ global (unlike abelian case).

    The key mathematical distinction (abelian vs nonabelian) is captured by:

    source
    inductive QEC1.Generalizations.GeneralizationDirection :
    Type

    The four directions of generalization for the gauging procedure

    Instances For
      source
      instance QEC1.Generalizations.instDecidableEqGeneralizationDirection :
      DecidableEq GeneralizationDirection
      Equations
      source
      instance QEC1.Generalizations.instReprGeneralizationDirection :
      Repr GeneralizationDirection
      Equations
      source
      def QEC1.Generalizations.instReprGeneralizationDirection.repr :
      GeneralizationDirection → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def QEC1.Generalizations.procedureApplies :
        GeneralizationDirection → Bool

        All four generalizations preserve applicability of the gauging procedure

        Equations
        Instances For
          source
          def QEC1.Generalizations.hasLocalGlobalCaveat :
          GeneralizationDirection → Bool

          Only nonabelian groups have the "local doesn't determine global" caveat

          Equations
          Instances For
            source
            theorem QEC1.Generalizations.all_directions_applicable (dir : GeneralizationDirection) :
            procedureApplies dir = true
            source
            theorem QEC1.Generalizations.only_nonabelian_has_caveat (dir : GeneralizationDirection) :
            hasLocalGlobalCaveat dir = true ↔ dir = GeneralizationDirection.nonabelianGroups

            Summary #

            This formalization captures Remark 14 about generalizations of the gauging measurement procedure:

            Key Theorems:

            1. abelian_product_order_independent: For abelian groups, ∏_v g_v is independent of ordering. This means local measurements uniquely determine the global charge.

            2. S3_nonabelian: S₃ is nonabelian (concrete witness of non-commutativity).

            3. nonabelian_different_orderings_different_results: For nonabelian groups, different orderings of local charges can give different global products. This is why local measurements don't fix a definite global charge.

            4. qudit_positive_dimension / qudit_extension_valid: Qudit systems with d > 2 have well-defined positive dimension, so the procedure extends.

            The Four Generalizations:

            The mathematical essence is captured by the abelian vs nonabelian distinction: products commute in abelian groups (order doesn't matter) but not in nonabelian groups (order matters, so local measurements can't uniquely determine the global charge).