Empirical/QM: Single-qubit gates (Hadamard, Phase S, Phase T)

Category: 3-Local (promotion-ready to 2-Framework on demand; content is QM-generic and Cat-2 candidate parallel to NoCloning).

Pure linear-algebra definitions + unitarity properties for the canonical single-qubit gates. No CSD ontology; the CSD-side reading lives in the companion Empirical/CSD/Gates/SingleQubit.lean.

Contents

• qmH: Hadamard (1/√2) !![1, 1; 1, -1]. Involutive (qmH * qmH = 1), Hermitian (qmH_hermitian), unitary (qmH_unitary).
• qmS: Phase !![1, 0; 0, I]. Diagonal; qmS² = qmZ (Pauli Z); unitary (qmS_unitary).
• qmT: π/4-phase !![1, 0; 0, exp(iπ/4)]. Diagonal; qmT² = qmS; unitary (qmT_unitary).

qmZ is included as an auxiliary (also re-exportable; conventional Pauli σ_z). (The unitarity lemmas were added 2026-08-29: an audit found the header promising them while only the squaring identities were proved — the sibling MultiQubit.lean standard, Gᴴ * G = 1, now holds here too.)

Naming

qm-prefixed matrix-level gates, serving the density-matrix / CSD-gates ecosystem (Empirical/CSD/Gates/, Einselection.lean). The coordinate-operator siblings on the register live in the Cat-1 tree (Mathlib/QuantumInfo/Clifford.lean's sGate/hGate, Magic.lean's tGate — where T² = S is tGate_tGate); the two layers serve different consumer bases and neither derives from the other. The CSD-side companion uses csd-prefixed names.

Experimental provenance

These are standard textbook gates; specific experimental verification is unit-test-level (gate fidelity measurements in any QC platform). No single named experiment.

Auxiliary: Pauli Z

noncomputable def CSD.Empirical.QM.Gates.qmZ : Matrix (Fin 2) (Fin 2) ℂ

Pauli σ_z = !![1, 0; 0, -1]. Auxiliary for qmS² = qmZ.

Equations

• CSD.Empirical.QM.Gates.qmZ = !![1, 0; 0, -1]

Hadamard

noncomputable def CSD.Empirical.QM.Gates.qmH : Matrix (Fin 2) (Fin 2) ℂ

Hadamard gate H = (1/√2) !![1, 1; 1, -1].

Equations

• CSD.Empirical.QM.Gates.qmH = (↑√2)⁻¹ • !![1, 1; 1, -1]

theorem CSD.Empirical.QM.Gates.qmH_mul_self : qmH * qmH = 1

H * H = I. Hadamard is involutive.

theorem CSD.Empirical.QM.Gates.qmH_hermitian : qmH.conjTranspose = qmH

Hᴴ = H: the Hadamard is Hermitian (real symmetric).

theorem CSD.Empirical.QM.Gates.qmH_unitary : qmH.conjTranspose * qmH = 1

Hᴴ * H = 1: the Hadamard is unitary (Hermitian + involutive).

Phase S

noncomputable def CSD.Empirical.QM.Gates.qmS : Matrix (Fin 2) (Fin 2) ℂ

Phase gate S = !![1, 0; 0, I].

Equations

• CSD.Empirical.QM.Gates.qmS = !![1, 0; 0, Complex.I]

theorem CSD.Empirical.QM.Gates.qmS_sq : qmS * qmS = qmZ

S² = Z.

theorem CSD.Empirical.QM.Gates.qmS_unitary : qmS.conjTranspose * qmS = 1

Sᴴ * S = 1: the phase gate is unitary (conj i · i = 1).

Phase T

noncomputable def CSD.Empirical.QM.Gates.qmT : Matrix (Fin 2) (Fin 2) ℂ

Phase gate T = !![1, 0; 0, exp(iπ/4)]. Diagonal eighth-root-of-unity factor on the second basis state.

Equations

• CSD.Empirical.QM.Gates.qmT = !![1, 0; 0, Complex.exp (Complex.I * (↑Real.pi / 4))]

theorem CSD.Empirical.QM.Gates.qmT_sq : qmT * qmT = qmS

T² = S. Follows from exp(iπ/4)² = exp(iπ/2) = i.

theorem CSD.Empirical.QM.Gates.qmT_unitary : qmT.conjTranspose * qmT = 1

Tᴴ * T = 1: the T gate is unitary (e^{−iπ/4} · e^{iπ/4} = 1).