Pauli $X$ -strings are unitary

Proved

StabilizerRank.pauli_x_string_unitary

by WillR · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

clifford-grouppauli-groupquantum-computingstabilizer-rank

Let $x$ be an $n$ -bit string and let $X^x$ be the corresponding Pauli $X$ -string, the tensor product of Pauli $X$ operators on the qubits where $x$ is true (formally pauliMatrix x 0, with trivial $Z$ component). Then $X^x$ is unitary: it acts on the computational basis by the permutation $y \mapsto x \oplus y$ with all phases equal to $1$ , so $X^x (X^x)^* = 1$ . This is the unitarity half of the fact that $X$ -strings are Clifford unitaries, which exhibits every computational-basis state as a stabilizer state.

Preamble

import Definitions.Def_StabilizerRank

Formal statement

namespace StabilizerRank

theorem pauli_x_string_unitary {n : ℕ} (x : Bits n) :
    pauliMatrix x 0 ∈ Matrix.unitaryGroup (Bits n) ℂ := by sorry

end StabilizerRank

Source

Standard Pauli/Clifford theory (e.g. Nielsen-Chuang, Chapter 10); X-string unitarity as needed for the stabilizer-state basis of the StabilizerRank mission.

View graph

Pauli XXX-strings are unitary

Pauli $X$ -strings are unitary