The Pauli operators and their 𝔽₂-symplectic algebra (GK-1)

Category: 1-Mathlib (CSD-free).

The n-qubit Pauli operators X^a Z^b (a b : Fin n → Fin 2) as concrete coordinate operators on the register, with the algebra that makes the stabiliser formalism tick (plan specs/gottesman-knill-plan.md, brick GK-1):

• ★ The group law (pauliOp_mul): X^a Z^b · X^{a'} Z^{b'} = (−1)^{b·a'} X^{a+a'} Z^{b+b'} — the Pauli family is closed under composition, with the phase governed by the 𝔽₂ pairing.
• ★ Commutation is the symplectic form (pauliOp_comm/pauliOp_comm_of_symp): the composition mismatch is exactly χ(a·b' + b·a'), so two Paulis commute iff the symplectic form of their labels vanishes in 𝔽₂.
• Character orthogonality (sum_pauliSign): ∑_z (−1)^{b·z} = 2ⁿ·[b = 0], hence ★ every non-identity Pauli is traceless (pauliOp_trace) — the seed of the stabiliser-state uniqueness argument (tr(2⁻ⁿ ∑_{s∈S} s) = 1, GK-3, not attempted here).
• Unitarity in the coordinate sense (inner_pauliOp): Paulis preserve the inner product.

Design note: every sign is signChar of an 𝔽₂-valued form (bdot), never an ℕ parity — so sign bookkeeping reduces to Fin 2 identities in finitely many generalized atoms, closed by decide. Fin 2 carries the ZMod 2 ring structure (Fin.instCommRing), so ring is available for the form algebra; the one genuinely characteristic-2 fact, v + v = 0, is fin2_add_self.

The sign character and the 𝔽₂ pairing

def QuantumInfo.signChar (v : Fin 2) : ℂ

The sign character on 𝔽₂: χ(0) = 1, χ(1) = −1.

Equations

• QuantumInfo.signChar v = if v = 0 then 1 else -1

@[simp]

theorem QuantumInfo.signChar_zero : signChar 0 = 1

theorem QuantumInfo.signChar_add (u v : Fin 2) : signChar (u + v) = signChar u * signChar v

theorem QuantumInfo.signChar_mul_self (u : Fin 2) : signChar u * signChar u = 1

theorem QuantumInfo.conj_signChar (u : Fin 2) : (starRingEnd ℂ) (signChar u) = signChar u

theorem QuantumInfo.signChar_sum {κ : Type u_1} (s : Finset κ) (f : κ → Fin 2) : signChar (∑ i ∈ s, f i) = ∏ i ∈ s, signChar (f i)

χ turns 𝔽₂ sums into products.

theorem QuantumInfo.fin2_add_self (v : Fin 2) : v + v = 0

The characteristic-2 fact: every bit is its own inverse.

def QuantumInfo.bdot {n : ℕ} (b z : Fin n → Fin 2) : Fin 2

The 𝔽₂ pairing b·z = ∑ᵢ bᵢzᵢ (valued in Fin 2).

Equations

• QuantumInfo.bdot b z = ∑ i : Fin n, b i * z i

theorem QuantumInfo.bdot_add_right {n : ℕ} (b z w : Fin n → Fin 2) : bdot b (z + w) = bdot b z + bdot b w

theorem QuantumInfo.bdot_add_left {n : ℕ} (b b' z : Fin n → Fin 2) : bdot (b + b') z = bdot b z + bdot b' z

@[simp]

theorem QuantumInfo.bdot_zero_right {n : ℕ} (b : Fin n → Fin 2) : bdot b 0 = 0

@[simp]

theorem QuantumInfo.bdot_zero_left {n : ℕ} (z : Fin n → Fin 2) : bdot 0 z = 0

theorem QuantumInfo.bdot_comm {n : ℕ} (b z : Fin n → Fin 2) : bdot b z = bdot z b

theorem QuantumInfo.bdot_update {n : ℕ} (b z : Fin n → Fin 2) (k : Fin n) (v : Fin 2) : bdot b (Function.update z k v) = bdot b z + b k * (z k + v)

The pairing against a point update: b·(z[k := v]) = b·z + bₖ(zₖ + v).

theorem QuantumInfo.bdot_update_left {n : ℕ} (b z : Fin n → Fin 2) (k : Fin n) (v : Fin 2) : bdot (Function.update b k v) z = bdot b z + z k * (b k + v)

The pairing against a point update in the first slot.

def QuantumInfo.pauliSign {n : ℕ} (b z : Fin n → Fin 2) : ℂ

The Pauli sign (−1)^{b·z} as χ(b·z).

Equations

• QuantumInfo.pauliSign b z = QuantumInfo.signChar (QuantumInfo.bdot b z)

theorem QuantumInfo.pauliSign_add_right {n : ℕ} (b z w : Fin n → Fin 2) : pauliSign b (z + w) = pauliSign b z * pauliSign b w

theorem QuantumInfo.pauliSign_add_left {n : ℕ} (b b' z : Fin n → Fin 2) : pauliSign (b + b') z = pauliSign b z * pauliSign b' z

theorem QuantumInfo.pauliSign_mul_self {n : ℕ} (b z : Fin n → Fin 2) : pauliSign b z * pauliSign b z = 1

@[simp]

theorem QuantumInfo.pauliSign_zero_left {n : ℕ} (z : Fin n → Fin 2) : pauliSign 0 z = 1

theorem QuantumInfo.conj_pauliSign {n : ℕ} (b z : Fin n → Fin 2) : (starRingEnd ℂ) (pauliSign b z) = pauliSign b z

The Pauli operators

noncomputable def QuantumInfo.pauliOp {n : ℕ} (a b : Fin n → Fin 2) (ψ : QReg n) : QReg n

The Pauli operator X^a Z^b on the register: coordinate (X^a Z^b ψ)(z) = (−1)^{b·(z+a)} ψ(z+a) — bit-flip by a, phase by b.

Equations

• QuantumInfo.pauliOp a b ψ = (WithLp.equiv 2 ((Fin n → Fin 2) → ℂ)).symm fun (z : Fin n → Fin 2) => QuantumInfo.pauliSign b (z + a) * ψ.ofLp (z + a)

@[simp]

theorem QuantumInfo.pauliOp_apply {n : ℕ} (a b : Fin n → Fin 2) (ψ : QReg n) (z : Fin n → Fin 2) : (pauliOp a b ψ).ofLp z = pauliSign b (z + a) * ψ.ofLp (z + a)

@[simp]

theorem QuantumInfo.pauliOp_zero {n : ℕ} (ψ : QReg n) : pauliOp 0 0 ψ = ψ

The identity-label Pauli is the identity.

theorem QuantumInfo.pauliOp_smul {n : ℕ} (a b : Fin n → Fin 2) (c : ℂ) (ψ : QReg n) : pauliOp a b (c • ψ) = c • pauliOp a b ψ

The Pauli operator is homogeneous.

theorem QuantumInfo.pauliOp_add {n : ℕ} (a b : Fin n → Fin 2) (ψ χ : QReg n) : pauliOp a b (ψ + χ) = pauliOp a b ψ + pauliOp a b χ

The Pauli operator is additive.

theorem QuantumInfo.pauliOp_sum {n : ℕ} {κ : Type u_1} (a b : Fin n → Fin 2) (s : Finset κ) (f : κ → QReg n) : pauliOp a b (∑ k ∈ s, f k) = ∑ k ∈ s, pauliOp a b (f k)

The Pauli operator commutes with finite sums.

theorem QuantumInfo.pauliOp_basisState {n : ℕ} (a b w : Fin n → Fin 2) : pauliOp a b (basisState w) = pauliSign b w • basisState (w + a)

The Pauli action on a basis state: X^a Z^b |w⟩ = (−1)^{b·w} |w + a⟩.

theorem QuantumInfo.pauliOp_mul {n : ℕ} (a b a' b' : Fin n → Fin 2) (ψ : QReg n) : pauliOp a b (pauliOp a' b' ψ) = pauliSign b a' • pauliOp (a + a') (b + b') ψ

★ The Pauli group law: X^a Z^b · X^{a'} Z^{b'} = (−1)^{b·a'} · X^{a+a'} Z^{b+b'}. The family is closed under composition; the phase is the 𝔽₂ pairing b·a'.

theorem QuantumInfo.pauliOp_comm {n : ℕ} (a b a' b' : Fin n → Fin 2) (ψ : QReg n) : pauliOp a b (pauliOp a' b' ψ) = signChar (bdot a b' + bdot b a') • pauliOp a' b' (pauliOp a b ψ)

★ Commutation is the symplectic form: the composition mismatch between X^a Z^b · X^{a'} Z^{b'} and its reverse is exactly χ(a·b' + b·a') — the two Paulis commute iff the 𝔽₂ symplectic form of their labels vanishes.

theorem QuantumInfo.pauliOp_comm_of_symp {n : ℕ} (a b a' b' : Fin n → Fin 2) (h : bdot a b' + bdot b a' = 0) (ψ : QReg n) : pauliOp a b (pauliOp a' b' ψ) = pauliOp a' b' (pauliOp a b ψ)

Two Paulis with vanishing symplectic form commute.

Character orthogonality and tracelessness

theorem QuantumInfo.sum_signChar_mul (u : Fin 2) : ∑ v : Fin 2, signChar (u * v) = if u = 0 then 2 else 0

One-bit character orthogonality: ∑_v χ(u·v) = 2·[u = 0].

theorem QuantumInfo.sum_pauliSign {n : ℕ} (b : Fin n → Fin 2) : ∑ z : Fin n → Fin 2, pauliSign b z = if b = 0 then 2 ^ n else 0

Character orthogonality: ∑_z (−1)^{b·z} = 2ⁿ·[b = 0].

theorem QuantumInfo.pauliOp_trace {n : ℕ} (a b : Fin n → Fin 2) : ∑ z : Fin n → Fin 2, (pauliOp a b (basisState z)).ofLp z = if a = 0 ∧ b = 0 then 2 ^ n else 0

★ Non-identity Paulis are traceless: the diagonal sum of X^a Z^b over the computational basis is 2ⁿ at the identity label and 0 otherwise. This is the seed of the stabiliser-projector trace argument (GK-3 in the plan).

Unitarity in the coordinate sense

theorem QuantumInfo.inner_pauliOp {n : ℕ} (a b : Fin n → Fin 2) (ψ φ : QReg n) : inner ℂ (pauliOp a b ψ) (pauliOp a b φ) = inner ℂ ψ φ

Paulis preserve the inner product: the reindexing z ↦ z + a is a bijection and the sign is real of modulus one.