Transversal Cliffords: a Pauli string factorises, and the transversal Hadamard swaps X and Z

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #62 (b), the general half.

A Pauli string is a tensor product over the qubits — which is obvious on paper and needs saying once in Lean, because pauliMat a b is defined by its entries and blockKron by a product over the blocks. Once said, the conjugation rule of a transversal gate is the single-qubit rule raised to the tensor power, and that is the whole mechanism of transversality.

• permMat σ — the matrix of a basis permutation, with the row/column reindexing lemmas (permMat_mul_apply, mul_permMat_apply) and, for an involution, permMat_conjTranspose, permMat_mul_self, permMat_mem_unitaryGroup. A transversal CNOT is one of these;
• onePauli u v — the single-qubit Pauli X^u Z^v, and ★★ pauliMat_eq_blockKron: pauliMat a b = ⨂ᵢ onePauli (aᵢ) (bᵢ);
• hGateM_mul_onePauli and ★ hGateM_conj_onePauli — H X^u Z^v H = (−1)^{uv} X^v Z^u, the four cases of H X H = Z, H Z H = X;
• hadTransversal n — the Hadamard on every qubit, with hadTransversal_mul_self and hadTransversal_conjTranspose (it is its own inverse and Hermitian);
• ★★ hadTransversal_conj_pauliMat — the transversal Hadamard exchanges the X- and Z-labels of every Pauli string: H^{⊗n} X^a Z^b H^{⊗n} = (−1)^{a·b} X^b Z^a. For a CSS code, where a · b = 0 on the stabiliser labels, the sign is 1 and the group is preserved — which is what the consumer (Empirical/QM/QEC/SteaneFaultyGate.lean) spends it on.

Honest scope

⚠️ Nothing here is about a code: these are identities in the Pauli group and its normaliser. That a particular transversal gate preserves a particular code space is the code's business, and needs the code's labels (for the Steane code, the CSS condition bdot_rowComb_rowComb).

⚠️ The Schrödinger-picture action of a transversal gate on encoded states is not here. What the conjugation rule gives is the Heisenberg picture: where the logical Paulis go.

References: M. Nielsen, I. Chuang, Quantum Computation and Quantum Information §10.4.2 (transversal gates), §10.5.8; A. Steane, PRL 77 (1996); specs/BACKLOG.md #62; specs/steane-plan.md; specs/future-work.md.

Permutation matrices

def QuantumInfo.permMat {α : Type u_1} [DecidableEq α] (σ : α → α) : Matrix α α ℂ

The matrix of a basis permutation: the gate that sends |w⟩ to |σ w⟩. A transversal CNOT is one of these, which is why its logical action needs no amplitudes.

Equations

• QuantumInfo.permMat σ = Matrix.of fun (z w : α) => if z = σ w then 1 else 0

theorem QuantumInfo.permMat_apply {α : Type u_1} [DecidableEq α] (σ : α → α) (z w : α) : permMat σ z w = if z = σ w then 1 else 0

theorem QuantumInfo.permMat_mul_apply {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] {σ : α → α} (hσ : Function.Involutive σ) (M : Matrix α β ℂ) (z : α) (c : β) : (permMat σ * M) z c = M (σ z) c

A permutation matrix on the left reindexes the rows by the permutation.

theorem QuantumInfo.mul_permMat_apply {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] (σ : α → α) (M : Matrix β α ℂ) (z : β) (c : α) : (M * permMat σ) z c = M z (σ c)

A permutation matrix on the right reindexes the columns.

theorem QuantumInfo.permMat_conjTranspose {α : Type u_1} [DecidableEq α] {σ : α → α} (hσ : Function.Involutive σ) : (permMat σ).conjTranspose = permMat σ

theorem QuantumInfo.permMat_mul_self {α : Type u_1} [Fintype α] [DecidableEq α] {σ : α → α} (hσ : Function.Involutive σ) : permMat σ * permMat σ = 1

theorem QuantumInfo.permMat_mem_unitaryGroup {α : Type u_1} [Fintype α] [DecidableEq α] {σ : α → α} (hσ : Function.Involutive σ) : permMat σ ∈ Matrix.unitaryGroup α ℂ

A Pauli string is a tensor product over the qubits

def QuantumInfo.onePauli (u v : Fin 2) : Matrix (Fin 2) (Fin 2) ℂ

The single-qubit Pauli X^u Z^v: it moves |w⟩ to |w + u⟩ and signs it by (−1)^{v w}.

Equations

• QuantumInfo.onePauli u v = Matrix.of fun (z w : Fin 2) => if w = z + u then QuantumInfo.signChar (v * w) else 0

theorem QuantumInfo.onePauli_apply (u v z w : Fin 2) : onePauli u v z w = if w = z + u then signChar (v * w) else 0

theorem QuantumInfo.pauliMat_eq_blockKron {n : ℕ} (a b : Fin n → Fin 2) : pauliMat a b = blockKron fun (i : Fin n) => onePauli (a i) (b i)

★★ A Pauli string is the tensor product of its single-qubit Paulis.

The single-qubit Hadamard on a Pauli

theorem QuantumInfo.hGateM_mul_onePauli (u v : Fin 2) : CliffordT.hGateM * onePauli u v = signChar (u * v) • onePauli v u * CliffordT.hGateM

H X^u Z^v = (−1)^{uv} X^v Z^u H: the Hadamard moved across a Pauli, with one factor of H on each side, so the √2 never has to be squared.

theorem QuantumInfo.hGateM_conj_onePauli (u v : Fin 2) : CliffordT.hGateM * onePauli u v * CliffordT.hGateM = signChar (u * v) • onePauli v u

★ H X^u Z^v H = (−1)^{uv} X^v Z^u — the four cases H I H = I, H X H = Z, H Z H = X, H (XZ) H = −XZ.

The transversal Hadamard

noncomputable def QuantumInfo.hadTransversal (n : ℕ) : Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ

The transversal Hadamard: the Hadamard on every one of the n qubits.

Equations

• QuantumInfo.hadTransversal n = QuantumInfo.blockKron fun (x : Fin n) => QuantumInfo.CliffordT.hGateM

theorem QuantumInfo.hadTransversal_mul_self {n : ℕ} : hadTransversal n * hadTransversal n = 1

theorem QuantumInfo.hGateM_conjTranspose : CliffordT.hGateM.conjTranspose = CliffordT.hGateM

theorem QuantumInfo.hadTransversal_conjTranspose {n : ℕ} : (hadTransversal n).conjTranspose = hadTransversal n

theorem QuantumInfo.hadTransversal_conj_pauliMat {n : ℕ} (a b : Fin n → Fin 2) : hadTransversal n * pauliMat a b * hadTransversal n = signChar (bdot a b) • pauliMat b a

★★ The transversal Hadamard exchanges the X- and Z-labels of a Pauli string, with the sign (−1)^{a·b}: the single-qubit rule raised to the tensor power. On a CSS code's stabiliser labels a · b = 0, so the group is preserved elementwise.