Rem_4: Z-Type Support Convention

Statement

For a Pauli operator $P$, the $Z$-type support of $P$, denoted $\mathcal{S}_Z$, is the set of qubits on which $P$ acts via $Y$ or $Z$ operators. Similarly, the $X$-type support, denoted $\mathcal{S}_X$, is the set of qubits on which $P$ acts via $X$ or $Y$ operators. A Pauli operator $P$ can be written as $P = i^{\sigma} \prod_{v \in \mathcal{S}_X} X_v \prod_{v \in \mathcal{S}_Z} Z_v$ for some phase $\sigma \in \{0,1,2,3\}$. If $P$ commutes with an $X$-type logical operator $L = \prod_v X_v$, then $|\mathcal{S}_Z| \equiv 0 \pmod{2}$ (the $Z$-type support has even cardinality).

Main Definitions

The X-type and Z-type support definitions are in Rem_1_StabilizerCodeConvention. This file focuses on the decomposition and commutation properties.

Main Results

• PauliOp.xzDecomposition : P = i^σ ∏{v ∈ S_X} X_v ∏{v ∈ S_Z} Z_v
• PauliOp.commutes_with_pureX_iff_zSupport_even : P commutes with L = ∏_v X_v iff |S_Z ∩ supp(L)| is even
• PauliOp.commutes_with_XTypeLogical_imp_zSupport_even : If P commutes with X-type logical L, then |S_Z| restricted to supp(L) is even

Corollaries

• The Z-type support has even cardinality when P commutes with an X-type logical over its full support

Recap of X-type and Z-type Support

The definitions are already in Rem_1:

• PauliOp.xSupport P : qubits where P acts as X or Y (X-type)
• PauliOp.zSupport P : qubits where P acts as Z or Y (Z-type)
• StabPauliType.isXType p : true if p is X or Y
• StabPauliType.isZType p : true if p is Z or Y

@[simp]

theorem StabPauliType.X_isXType : X.isXType = true

X and Y contribute to X-type support

@[simp]

theorem StabPauliType.Y_isXType : Y.isXType = true

@[simp]

theorem StabPauliType.Z_isXType : Z.isXType = false

@[simp]

theorem StabPauliType.I_isXType : I.isXType = false

@[simp]

theorem StabPauliType.X_isZType : X.isZType = false

Z and Y contribute to Z-type support

@[simp]

theorem StabPauliType.Y_isZType : Y.isZType = true

@[simp]

theorem StabPauliType.Z_isZType : Z.isZType = true

@[simp]

theorem StabPauliType.I_isZType : I.isZType = false

theorem StabPauliType.Y_isXType_and_isZType : Y.isXType = true ∧ Y.isZType = true

Y is both X-type and Z-type

theorem StabPauliType.isNontrivial_iff_isXType_or_isZType (p : StabPauliType) : p.isNontrivial = true ↔ p.isXType = true ∨ p.isZType = true

A Pauli is nontrivial iff it is X-type or Z-type (or both, i.e., Y)

theorem StabPauliType.X_anticommutes_Z : X.commutes Z = false

The anticommutation rule: X and Z anticommute

theorem StabPauliType.Z_anticommutes_X : Z.commutes X = false

theorem StabPauliType.X_anticommutes_Y : X.commutes Y = false

X and Y anticommute

theorem StabPauliType.Y_anticommutes_X : Y.commutes X = false

theorem StabPauliType.Z_anticommutes_Y : Z.commutes Y = false

Z and Y anticommute

theorem StabPauliType.Y_anticommutes_Z : Y.commutes Z = false

theorem StabPauliType.anticommutes_iff (p q : StabPauliType) : p.commutes q = false ↔ p = X ∧ q = Z ∨ p = Z ∧ q = X ∨ p = X ∧ q = Y ∨ p = Y ∧ q = X ∨ p = Z ∧ q = Y ∨ p = Y ∧ q = Z

Two Paulis anticommute iff one is purely X-type (X) and the other is purely Z-type (Z), or one involves both (Y) and the other involves just one component

theorem StabPauliType.X_commutes_iff (q : StabPauliType) : X.commutes q = true ↔ q.isZType = false

For pure X (not Y), anticommutes with Z-type but not X-type

theorem StabPauliType.Z_commutes_iff (q : StabPauliType) : Z.commutes q = true ↔ q.isXType = false

For pure Z (not Y), anticommutes with X-type but not Z-type

Commutation of Multi-Qubit Pauli Operators

def PauliOp.zSupportOverlap {n : ℕ} (P Q : PauliOp n) : Finset (Fin n)

The overlap between Z-type support of P and support of Q

Equations

• P.zSupportOverlap Q = P.zSupport ∩ Q.support

def PauliOp.anticommutingPositionsWithPureX {n : ℕ} (P : PauliOp n) (S : Finset (Fin n)) : Finset (Fin n)

The anticommuting positions between P and a pure X operator on support S

Equations

• P.anticommutingPositionsWithPureX S = {i ∈ S | (P.paulis i).isZType = true}

theorem PauliOp.anticommutingPositionsWithPureX_eq {n : ℕ} (P : PauliOp n) (S : Finset (Fin n)) : P.anticommutingPositionsWithPureX S = P.zSupport ∩ S

Alternative characterization: positions where P is Z-type and S has X

theorem PauliOp.commutes_with_pureX_iff {n : ℕ} (P : PauliOp n) (S : Finset (Fin n)) : P.commutes (pureX S) ↔ (P.zSupport ∩ S).card % 2 = 0

P commutes with pureX S iff the number of Z-type positions in S is even

theorem PauliOp.zSupport_inter_even_of_commutes_pureX {n : ℕ} (P : PauliOp n) (S : Finset (Fin n)) (h : P.commutes (pureX S)) : (P.zSupport ∩ S).card % 2 = 0

If P commutes with pureX S, then |P.zSupport ∩ S| is even

theorem PauliOp.commutes_pureX_of_zSupport_inter_even {n : ℕ} (P : PauliOp n) (S : Finset (Fin n)) (h : (P.zSupport ∩ S).card % 2 = 0) : P.commutes (pureX S)

Converse: if |P.zSupport ∩ S| is even, then P commutes with pureX S

def PauliOp.hasEvenCardinality {n : ℕ} (S : Finset (Fin n)) : Prop

Even cardinality characterization

Equations

• PauliOp.hasEvenCardinality S = (S.card % 2 = 0)

@[simp]

theorem PauliOp.hasEvenCardinality_iff {n : ℕ} (S : Finset (Fin n)) : hasEvenCardinality S ↔ S.card % 2 = 0

@[simp]

theorem PauliOp.hasEvenCardinality_empty {n : ℕ} : hasEvenCardinality ∅

Empty set has even cardinality

The Main Theorem: Commutation with X-type Logical

theorem PauliOp.commutes_with_XTypeLogical_imp_zSupport_even {C : StabilizerCode} (P : PauliOp C.n) (L : XTypeLogical C) (h : P.commutes L.op) : (P.zSupport ∩ L.support).card % 2 = 0

Main theorem: If P commutes with an X-type logical operator L = ∏_{v ∈ supp(L)} X_v, then the Z-type support of P restricted to supp(L) has even cardinality.

This is because:

• L acts as X on each qubit in its support
• P and L anticommute at position i iff P is Z-type at i and i ∈ supp(L)
• For P and L to commute overall, the number of anticommuting positions must be even
• Hence |S_Z(P) ∩ supp(L)| ≡ 0 (mod 2)

theorem PauliOp.commutes_with_full_XLogical_imp_zSupport_card_even {C : StabilizerCode} (P : PauliOp C.n) (L : XTypeLogical C) (hfull : L.support = Finset.univ) (h : P.commutes L.op) : P.zSupport.card % 2 = 0

When L has full support (acts on all n qubits), the condition becomes: P commutes with L implies |S_Z(P)| is even

The X-Z Decomposition

def PauliOp.xzExponents (p : StabPauliType) : Fin 2 × Fin 2

Every Pauli type can be written as X^a Z^b for a, b ∈ {0,1} (ignoring phase). I = X^0 Z^0, X = X^1 Z^0, Z = X^0 Z^1, Y = X^1 Z^1 (up to phase i)

Equations

• PauliOp.xzExponents StabPauliType.I = (0, 0)
• PauliOp.xzExponents StabPauliType.X = (1, 0)
• PauliOp.xzExponents StabPauliType.Y = (1, 1)
• PauliOp.xzExponents StabPauliType.Z = (0, 1)

@[simp]

theorem PauliOp.xzExponents_I : xzExponents StabPauliType.I = (0, 0)

@[simp]

theorem PauliOp.xzExponents_X : xzExponents StabPauliType.X = (1, 0)

@[simp]

theorem PauliOp.xzExponents_Y : xzExponents StabPauliType.Y = (1, 1)

@[simp]

theorem PauliOp.xzExponents_Z : xzExponents StabPauliType.Z = (0, 1)

theorem PauliOp.xzExponents_fst_eq_one_iff_isXType (p : StabPauliType) : (xzExponents p).1 = 1 ↔ p.isXType = true

The X exponent is 1 iff the Pauli is X-type

theorem PauliOp.xzExponents_snd_eq_one_iff_isZType (p : StabPauliType) : (xzExponents p).2 = 1 ↔ p.isZType = true

The Z exponent is 1 iff the Pauli is Z-type

structure PauliOp.XZDecomposition {n : ℕ} (P : PauliOp n) : Prop

The X-Z decomposition of a Pauli operator: P = i^σ ∏{v ∈ S_X} X_v ∏{v ∈ S_Z} Z_v

This structure captures that any Pauli operator factors into X-part and Z-part.

• xSupport_correct : P.xSupport = {i : Fin n | (xzExponents (P.paulis i)).1 = 1}

  The X-type support is exactly the qubits where P has X component

• zSupport_correct : P.zSupport = {i : Fin n | (xzExponents (P.paulis i)).2 = 1}

  The Z-type support is exactly the qubits where P has Z component

theorem PauliOp.xzDecomposition {n : ℕ} (P : PauliOp n) : P.XZDecomposition

Every Pauli operator has an X-Z decomposition

@[simp]

theorem PauliOp.xSupport_eq_filter {n : ℕ} (P : PauliOp n) : P.xSupport = {i : Fin n | P.paulis i = StabPauliType.X ∨ P.paulis i = StabPauliType.Y}

X-type support equals {v : P.paulis v ∈ {X, Y}}

@[simp]

theorem PauliOp.zSupport_eq_filter {n : ℕ} (P : PauliOp n) : P.zSupport = {i : Fin n | P.paulis i = StabPauliType.Z ∨ P.paulis i = StabPauliType.Y}

Z-type support equals {v : P.paulis v ∈ {Z, Y}}

Corollaries

@[simp]

theorem PauliOp.pureX_zSupport_empty {n : ℕ} (S : Finset (Fin n)) : (pureX S).zSupport = ∅

The Z-type support of a pure X operator is empty

@[simp]

theorem PauliOp.pureX_commutes_self {n : ℕ} (S : Finset (Fin n)) : (pureX S).commutes (pureX S)

A pure X operator always commutes with itself

theorem PauliOp.pureX_commutes_pureX {n : ℕ} (S T : Finset (Fin n)) : (pureX S).commutes (pureX T)

Two pure X operators always commute

theorem PauliOp.xSupport_inter_zSupport {n : ℕ} (P : PauliOp n) : P.xSupport ∩ P.zSupport = {i : Fin n | P.paulis i = StabPauliType.Y}

The intersection of X-type support and Z-type support gives qubits with Y

theorem PauliOp.support_eq_xSupport_union_zSupport {n : ℕ} (P : PauliOp n) : P.support = P.xSupport ∪ P.zSupport

The support of P is the union of pure X positions and pure Z positions and Y positions

Summary

The Z-type support convention establishes:

1. X-type Support S_X: Qubits where P acts as X or Y (has X component)

2. Z-type Support S_Z: Qubits where P acts as Z or Y (has Z component)

3. Decomposition: P = i^σ ∏{v ∈ S_X} X_v ∏{v ∈ S_Z} Z_v for some phase σ ∈ {0,1,2,3}

4. Key Commutation Property: If P commutes with an X-type logical operator L = ∏_{v ∈ supp(L)} X_v, then |S_Z ∩ supp(L)| ≡ 0 (mod 2)

   This is because:

   • P anticommutes with X at position i iff P is Z-type at i
   • P and L anticommute iff the number of such positions in supp(L) is odd
   • For commutation, this number must be even

This property is fundamental to the gauging construction: it ensures that deformed operators (which must commute with the logical L) have edge-paths with even boundary, making them well-defined.