Traces of Pauli operators, and orthogonality of the Pauli family

This file computes the trace of every Pauli operator toMatrix u and, from it, the trace pairing Tr((toMatrix s)ᴴ * toMatrix t) of any two. The result is the orthogonality relation Tr(s s') = δ_{s,s'} that def:pauli_basis attaches to the normalized n-qubit Pauli basis. The paper uses that relation in two places: for the normalization of the Pauli 2-norm (the norm entering apd:eq:def_high_weight_norm), and in the proof of apd:thm:local_flow_k_local, where the traces Tr(P O^{(g)}) are the coordinates of an orthonormal expansion — which is what makes conjugation act as an orthogonal matrix on coefficient vectors.

Main results

• char_sum: ∑_b (-1)^{u ⬝ᵥ b} = 2^n if u = 0 and 0 otherwise.
• trace_toMatrix_of_x_ne_zero, trace_toMatrix_of_x_eq_zero: the trace of a Pauli operator.
• trace_star_toMatrix_mul: the trace pairing of two Pauli operators, with its two special cases trace_star_toMatrix_mul_eq_zero (orthogonality) and trace_star_toMatrix_mul_self (squared Hilbert–Schmidt norm 2^n).
• trace_star_toMatrix_mul_phaseMul: phase variants of one string are not orthogonal.

The shape of the statement, and the trap in it

Pauli/Matrix.lean represents the whole phase-extended group, 4·4^n elements. That family is not orthogonal and cannot be: toMatrix (phaseMul 1 s) = i · toMatrix s, so a string and its phase multiples are collinear. What is true, and what this file proves, is that the trace pairing sees exactly the (x, z) data:

Tr((toMatrix s)ᴴ * toMatrix t) = 0 unless s.x = t.x and s.z = t.z,

with the value 2^n · i^{phase} when they do agree. So the orthogonal family is the 4^n signless classes, and a statement of orthogonality over PauliString n itself would be false. Anything downstream that wants an orthonormal basis has to choose a phase normalization first: Pauli/Coeff.lean chooses the self-adjoint representative herm, and Pauli/Tensor.lean the positive tensor-product representative tensorRepresentative.

How it is proved

Everything reduces to one character sum. The diagonal of toMatrix u is empty unless u.x = 0, because the entry at (a, a) is non-zero only where a = a + u.x; so

Tr (toMatrix u) = 0 if u.x ≠ 0, Tr (toMatrix u) = i^{u.phase} · ∑_b (-1)^{u.z ⬝ᵥ b} if u.x = 0,

and the sum is 2^n at u.z = 0 and 0 otherwise. The pairing statement then follows from toMatrix_star and toMatrix_mul, since (star s * t).x = s.x + t.x in characteristic two.

The character sum

∑_{b ∈ {0,1}^n} (-1)^{u ⬝ᵥ b} is the orthogonality relation for the additive characters of (ZMod 2)^n, and the engine of everything below.

There are two natural proofs. The one used here factorizes the sign over sites and swaps the sum with the product; the alternative pairs b with b + eᵢ at a site where u is on and cancels signs, via Finset.sum_ninvolution. The factorized proof is preferred because it is shorter, because it proves both branches from one identity rather than arguing u = 0 separately, and because negOnePow_sum and negOnePow_dotProduct are reusable on their own.

theorem Lean4LPD.PauliString.negOnePow_sum {ι : Type u_1} (s : Finset ι) (f : ι → ZMod 2) : negOnePow (∑ i ∈ s, f i) = ∏ i ∈ s, negOnePow (f i)

negOnePow is multiplicative over finite sums: (-1)^{∑ f i} = ∏ (-1)^{f i}.

theorem Lean4LPD.PauliString.negOnePow_dotProduct {n : ℕ} (u b : Bits n) : negOnePow (u ⬝ᵥ b) = ∏ i : Fin n, negOnePow (u i * b i)

The sign of a dot product factorizes over sites.

theorem Lean4LPD.PauliString.sum_negOnePow_mul (a : ZMod 2) : ∑ c : ZMod 2, negOnePow (a * c) = if a = 0 then 2 else 0

One site's contribution: 2 at a = 0 and 0 at a = 1. This vanishing is the whole content of the character sum.

theorem Lean4LPD.PauliString.char_sum (n : ℕ) (u : Bits n) : ∑ b : Bits n, negOnePow (u ⬝ᵥ b) = if u = 0 then 2 ^ n else 0

The Pauli character sum: 2^n at the trivial character, 0 otherwise.

The diagonal

theorem Lean4LPD.PauliString.diag_ne_zero_iff {n : ℕ} (u : PauliString n) (a : Bits n) : a = a + u.x ↔ u.x = 0

In characteristic two a shift fixes a basis label only when it is trivial, so toMatrix u has a non-empty diagonal exactly when its X-part vanishes.

theorem Lean4LPD.PauliString.toMatrix_diag_of_x_ne_zero {n : ℕ} {u : PauliString n} (hu : u.x ≠ 0) (a : Bits n) : u.toMatrix a a = 0

theorem Lean4LPD.PauliString.toMatrix_diag_of_x_eq_zero {n : ℕ} {u : PauliString n} (hu : u.x = 0) (a : Bits n) : u.toMatrix a a = iPow u.phase * negOnePow (u.z ⬝ᵥ a)

The trace

theorem Lean4LPD.PauliString.trace_toMatrix_of_x_ne_zero {n : ℕ} {u : PauliString n} (hu : u.x ≠ 0) : u.toMatrix.trace = 0

A Pauli operator with a non-trivial X-part is traceless: it is a permutation matrix pattern with no fixed points.

theorem Lean4LPD.PauliString.trace_toMatrix_of_x_eq_zero {n : ℕ} {u : PauliString n} (hu : u.x = 0) : u.toMatrix.trace = iPow u.phase * ∑ b : Bits n, negOnePow (u.z ⬝ᵥ b)

With a trivial X-part the trace is the phase times a character sum over the Z-part.

Orthogonality

The trace pairing sees the (x, z) data and nothing else. This is the relation Tr(s s') = δ_{s,s'} of def:pauli_basis, stated for the phase-extended group rather than for a normalized basis — which is the form that holds for PauliString n, since the group itself is not an orthogonal family.

theorem Lean4LPD.PauliString.star_mul_x {n : ℕ} (s t : PauliString n) : (star s * t).x = s.x + t.x

theorem Lean4LPD.PauliString.star_mul_z {n : ℕ} (s t : PauliString n) : (star s * t).z = s.z + t.z

theorem Lean4LPD.PauliString.trace_star_toMatrix_mul {n : ℕ} (s t : PauliString n) : (star s.toMatrix * t.toMatrix).trace = if s.x = t.x ∧ s.z = t.z then 2 ^ n * iPow (star s * t).phase else 0

The trace pairing of two Pauli operators. Zero unless the two strings carry the same X- and Z-parts; 2^n times a fourth root of unity when they do.

theorem Lean4LPD.PauliString.trace_star_toMatrix_mul_eq_zero {n : ℕ} {s t : PauliString n} (h : ¬(s.x = t.x ∧ s.z = t.z)) : (star s.toMatrix * t.toMatrix).trace = 0

Two Pauli strings differing in their X- or Z-part are orthogonal operators.

theorem Lean4LPD.PauliString.trace_star_toMatrix_mul_self {n : ℕ} (s : PauliString n) : (star s.toMatrix * s.toMatrix).trace = 2 ^ n

Every Pauli operator has squared Hilbert–Schmidt norm 2^n. With the 2^{-n/2} normalization of def:pauli_basis this is the diagonal case Tr(s s) = 1 of its orthonormality relation.

theorem Lean4LPD.PauliString.trace_star_toMatrix_mul_phaseMul {n : ℕ} (k : ZMod 4) (s : PauliString n) : (star s.toMatrix * (phaseMul k s).toMatrix).trace = 2 ^ n * iPow k

Phase variants are not orthogonal, and this records why the orthogonal family is the 4^n signless classes rather than the 4·4^n group elements: i·s pairs with s to give 2^n · i, not 0. Anything that wants an orthonormal basis must normalize the phase first.