SU(2) in axis–angle form, and the dense rotation circle of one Clifford+T word

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #80, part (a) of the re-split row #69 (R-005; specs/magic-plan.md, "The split").

The unit-quaternion parametrisation of the determinant-one 2 × 2 unitaries, written as a matrix directly: su2 w x y z = w·1 − i(x σ₁ + y σ₂ + z σ₃). Its algebra is the quaternion product (★ su2_mul), its determinant is w² + x² + y² + z² (su2_det) and its trace is 2w (su2_trace), so axisRot a b c θ, the rotation by θ about a unit vector (a, b, c), is a one-parameter group in θ (★ axisRot_add) with period 4π (axisRot_add_int_mul_four_pi), continuous in θ (continuous_axisRot).

The Clifford+T word T·HTH of CliffordTAngle.lean is, up to the phase e^{iπ/4}, exactly such a rotation: ★★ htht_eq_su2 gives its quaternion coordinates (cos²(π/8), √2/4, (2−√2)/4, √2/4) — no radicals beyond √2 — and ★ htht_eq_axisRot reads them as the axis (1, √2−1, 1)/‖·‖ and the angle htAngle of #68. Because that angle is an irrational multiple of 2π (and hence of 4π), the powers of the word fill its own rotation circle densely: ★★ mem_closure_range_axisRot.

• su2, ★ su2_mul, su2_one, su2_det, su2_trace;
• axisRot, axisRot_zero, ★ axisRot_add, axisRot_nat_mul, axisRot_add_int_mul_four_pi, continuous_axisRot;
• htSin, htSin_sq, htSin_pos, htA, htB, ★ htAxis_unit — the unit axis, radical-free through the products htSin · htA = √2/4 and htSin · htB = (2−√2)/4;
• ★★ htht_eq_su2, ★ htht_eq_axisRot, htht_pow — the word, its powers, and their phases;
• ★ irrational_htAngle_div_four_pi, dense_closure_htAngle_four_pi;
• ★★ mem_closure_range_axisRot — every rotation about the word's own axis is a limit of integer multiples of its angle, so (up to phase) of its powers.

Honest scope

⚠️ One axis. Filling SU(2) needs a second, non-parallel axis and the Euler decomposition U = R_u(α) R_v(β) R_u(γ): that is BACKLOG #81, done 2026-09-26 in CsdLean4/Mathlib/QuantumInfo/CliffordTDensity.lean, which follows the route worked out here (conjugating by H reflects the axis (1, √2−1, 1) to (1, 1−√2, 1), the two are orthogonal to (1, 0, −1), and the product of the two π-rotations is a rotation about (1, 0, −1) through an angle that is again an irrational multiple of 2π — so two orthogonal dense circles are reachable, where the Euler decomposition is the textbook z-y-z one). Nothing here claims density in U(2).

References: M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information §4.2 (the Bloch/axis–angle form) and §4.5.3; specs/magic-plan.md; specs/BACKLOG.md #80, #81; specs/future-work.md.

The unit-quaternion parametrisation

noncomputable def QuantumInfo.SU2.su2 (w x y z : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

su2 w x y z = w·1 − i(x σ₁ + y σ₂ + z σ₃): the quaternion w + xi + yj + zk as a 2 × 2 complex matrix. It has determinant w² + x² + y² + z².

Equations

• QuantumInfo.SU2.su2 w x y z = !![↑w - Complex.I * ↑z, -Complex.I * (↑x - Complex.I * ↑y); -Complex.I * (↑x + Complex.I * ↑y), ↑w + Complex.I * ↑z]

theorem QuantumInfo.SU2.su2_mul (w x y z w' x' y' z' : ℝ) : su2 w x y z * su2 w' x' y' z' = su2 (w * w' - x * x' - y * y' - z * z') (w * x' + x * w' + y * z' - z * y') (w * y' - x * z' + y * w' + z * x') (w * z' + x * y' - y * x' + z * w')

★ The quaternion product.

theorem QuantumInfo.SU2.su2_one : su2 1 0 0 0 = 1

theorem QuantumInfo.SU2.su2_det (w x y z : ℝ) : (su2 w x y z).det = ↑(w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2)

theorem QuantumInfo.SU2.su2_trace (w x y z : ℝ) : (su2 w x y z).trace = 2 * ↑w

Rotation by an angle about an axis

noncomputable def QuantumInfo.SU2.axisRot (a b c θ : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The rotation by θ about the unit vector (a, b, c).

Equations

• QuantumInfo.SU2.axisRot a b c θ = QuantumInfo.SU2.su2 (Real.cos (θ / 2)) (a * Real.sin (θ / 2)) (b * Real.sin (θ / 2)) (c * Real.sin (θ / 2))

@[simp]

theorem QuantumInfo.SU2.axisRot_zero (a b c : ℝ) : axisRot a b c 0 = 1

theorem QuantumInfo.SU2.axisRot_det {a b c : ℝ} (hu : a ^ 2 + b ^ 2 + c ^ 2 = 1) (θ : ℝ) : (axisRot a b c θ).det = 1

A rotation about a unit axis has determinant one.

theorem QuantumInfo.SU2.axisRot_add {a b c : ℝ} (hu : a ^ 2 + b ^ 2 + c ^ 2 = 1) (α β : ℝ) : axisRot a b c (α + β) = axisRot a b c α * axisRot a b c β

★ The rotations about a fixed unit axis form a one-parameter group.

theorem QuantumInfo.SU2.axisRot_nat_mul {a b c : ℝ} (hu : a ^ 2 + b ^ 2 + c ^ 2 = 1) (θ : ℝ) (k : ℕ) : axisRot a b c (↑k * θ) = axisRot a b c θ ^ k

theorem QuantumInfo.SU2.axisRot_add_int_mul_four_pi (a b c θ : ℝ) (k : ℤ) : axisRot a b c (θ + ↑k * (4 * Real.pi)) = axisRot a b c θ

The rotations have period 4π in the angle (a 2π rotation is −1).

theorem QuantumInfo.SU2.continuous_axisRot (a b c : ℝ) : Continuous (axisRot a b c)

The Clifford+T word in axis–angle form

theorem QuantumInfo.SU2.sqrt_two_ne_zero : √2 ≠ 0

noncomputable def QuantumInfo.SU2.htSin : ℝ

sin(htAngle/2), the sine of the half-angle of T·HTH.

Equations

• QuantumInfo.SU2.htSin = Real.sin QuantumInfo.CliffordT.htHalfAngle

theorem QuantumInfo.SU2.sqrt_two_lt_two : √2 < 2

theorem QuantumInfo.SU2.htSin_sq : htSin ^ 2 = (10 - 4 * √2) / 16

theorem QuantumInfo.SU2.htSin_nonneg : 0 ≤ htSin

theorem QuantumInfo.SU2.htSin_pos : 0 < htSin

theorem QuantumInfo.SU2.htSin_ne_zero : htSin ≠ 0

noncomputable def QuantumInfo.SU2.htA : ℝ

The first and third components of the unit axis of T·HTH.

Equations

• QuantumInfo.SU2.htA = √2 / 4 / QuantumInfo.SU2.htSin

noncomputable def QuantumInfo.SU2.htB : ℝ

The second component of the unit axis of T·HTH.

Equations

• QuantumInfo.SU2.htB = (2 - √2) / 4 / QuantumInfo.SU2.htSin

theorem QuantumInfo.SU2.htSin_mul_htA : htSin * htA = √2 / 4

theorem QuantumInfo.SU2.htSin_mul_htB : htSin * htB = (2 - √2) / 4

theorem QuantumInfo.SU2.htAxis_unit : htA ^ 2 + htB ^ 2 + htA ^ 2 = 1

★ The axis is a unit vector.

theorem QuantumInfo.SU2.htht_eq_su2 : CliffordT.htht = tPhase • su2 ((2 + √2) / 4) (√2 / 4) ((2 - √2) / 4) (√2 / 4)

★★ The Clifford+T word in quaternion coordinates: T·HTH = e^{iπ/4}·su2(cos²(π/8), √2/4, (2−√2)/4, √2/4).

theorem QuantumInfo.SU2.htht_eq_axisRot : CliffordT.htht = tPhase • axisRot htA htB htA CliffordT.htAngle

★ The word is its own rotation: T·HTH = e^{iπ/4}·R_n̂(htAngle) with the unit axis n̂ = (1, √2−1, 1)/‖·‖.

theorem QuantumInfo.SU2.htht_pow (k : ℕ) : CliffordT.htht ^ k = tPhase ^ k • axisRot htA htB htA (↑k * CliffordT.htAngle)

The powers of the word are its rotation's multiples, up to the phase.

The dense rotation circle

theorem QuantumInfo.SU2.irrational_htAngle_div_four_pi : Irrational (CliffordT.htAngle / (4 * Real.pi))

theorem QuantumInfo.SU2.dense_closure_htAngle_four_pi : Dense ↑(AddSubgroup.closure {CliffordT.htAngle, 4 * Real.pi})

theorem QuantumInfo.SU2.mem_closure_range_axisRot (α : ℝ) : axisRot htA htB htA α ∈ closure (Set.range fun (k : ℤ) => axisRot htA htB htA (↑k * CliffordT.htAngle))

★★ The word's powers fill its own rotation circle. Every rotation about the axis of T·HTH is a limit of integer multiples of its angle — equivalently, up to phase, of its powers (htht_pow).