Clifford+T fills SU(2): two orthogonal dense circles and the Euler decomposition

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #81, part (b2) of R-005; the single-qubit half of Clifford+T universality. #68 and #80 built one dense circle, #84 the Euler decomposition; this file closes the gap between them.

★★ det_one_mem_cliffordTLim: every determinant-one 2 × 2 unitary is a limit of Clifford+T words, and hence ★★ exists_phase_mem_cliffordTLim: Clifford+T is dense in U(2) modulo phase. The obstruction that shaped the proof is worth recording: no two axes in the Clifford orbit of the word's own axis are orthogonal, so a third axis has to be manufactured, and the mechanism is the cross product.

The second axis. The π rotation about the word's axis (htA, htB, htA) — available because #80's circle is dense and the closure is closed — followed by H, is a rotation about (1, 0, -1)/√2, the cross product of the two axes (★ axisRot_htAxis_pi_mul_hGateM; the y components cancel because the word's axis has equal x and z components). Its angle wAngle satisfies 2 cos wAngle = (6 + 16√2)/17.

That angle is irrational over 2π, and the cheap test of #68 cannot see it: x² + x = q needs an integer linear coefficient, and here the minimal polynomial is X² - (12/17)X - 28/17. So this file proves the general form, ★ not_isIntegral_of_quadratic: a monic rational quadratic whose linear coefficient is not an integer has no algebraic-integer root, because the minimal polynomial of an algebraic integer has integer coefficients and, for an irrational root, that quadratic is the minimal polynomial. With #68's isIntegral_two_mul_cos_of_eq_two_pi_mul that gives ★★ irrational_wAngle_div_two_pi.

Two orthogonal circles. Conjugating the new circle by Z = T⁴ reflects its axis to (1, 0, 1)/√2 (★★ axisRot_uAxis_mem), which is orthogonal to it. The Euler decomposition about that pair, ★★ exists_euler_two_axes, comes from #84's z-y-z form by two conjugations: R_z(π/2) turns the y axis into x (rzMat_conj_ryMat), and R_y(π/4) tilts z and x onto (1, 0, 1)/√2 and (1, 0, -1)/√2 (ryMat_conj_rzMat, ryMat_conj_axisRot_x).

• ★ not_isIntegral_of_quadratic;
• htB_pos, htA_sq, htB_sq — the word's axis in closed form, htA² = (5 + 2√2)/17;
• wHalfCos, wAngle, wHalfCos_sq, wHalfCos_mem, cos_wAngle_half, sin_wAngle_half, two_mul_cos_wAngle, irrational_two_mul_cos_wAngle, not_isIntegral_two_mul_cos_wAngle, ★★ irrational_wAngle_div_two_pi, irrational_wAngle_div_four_pi;
• axisRot_neg_axis, ryMat_conj_rzMat, ryMat_conj_axisRot_x, rzMat_conj_ryMat, conj_mul_three, exists_euler_zxz, ★★ exists_euler_two_axes;
• hGateM_mul_self, tGateM_pow, tGateM_pow_eight, pow_mul_pow_eq_one, cliffordT, cliffordTLim, hGateM_mem, tGateM_mem, cliffordT_le_lim, isClosed_cliffordTLim;
• mem_closure_range_axisRot_of_irrational, axisRot_int_mul_mem, ★ axisRot_mem_of_irrational — one rotation with an irrationally related angle gives the whole circle, inside any closed submonoid containing it and its inverse;
• wAxis_unit, uAxis_unit, sqrt_two_inv_eq, hGateM_eq_smul_su2, ★ axisRot_htAxis_pi_mul_hGateM;
• htht_mem, hthtInv_mem, htht_mul_inv, axisRot_htAxis_eight, irrational_eight_htAngle, ★★ axisRot_htAxis_mem — the first circle;
• piRot_mul_hGateM_mem, hGateM_mul_piRot_mem, piRot_mul_hGateM_mul_inv, axisRot_wAxis_four, irrational_four_wAngle, ★★ axisRot_wAxis_mem — the second;
• zGateM, tPhase_pow_four, zGateM_eq, zGateM_conj_su2, zGateM_conj_axisRot, ★★ axisRot_uAxis_mem — the third, orthogonal to the second;
• ★★ det_one_mem_cliffordTLim, ★★ exists_phase_mem_cliffordTLim.

Honest scope

⚠️ One qubit, and density rather than exactness: the statement is that SU(2) lies in the topological closure of the Clifford+T monoid, which is what a synthesis theorem needs and all that is true (the monoid itself is countable). The n-qubit statement is BACKLOG #73, which assembles this with #70, #71 and #85. ⚠️ No efficiency claim. How many gates an ε-approximation costs is Solovay–Kitaev, BACKLOG #74, deliberately not claimed.

References: M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information §4.5.3 and Exercise 4.11; C. M. Dawson, M. A. Nielsen, quant-ph/0505030 §2; CsdLean4/Mathlib/QuantumInfo/CliffordTAngle.lean and SU2Rotation.lean for the first circle, EulerDecomposition.lean for the z-y-z form; specs/magic-plan.md; specs/BACKLOG.md #81, #73; specs/future-work.md.

No algebraic integer satisfies a monic rational quadratic with a fractional coefficient

theorem not_isIntegral_of_quadratic {x : ℝ} {p q : ℚ} (hx : x ^ 2 + ↑p * x + ↑q = 0) (hirr : Irrational x) (hp : p.den ≠ 1) : ¬IsIntegral ℤ x

★ A monic rational quadratic whose linear coefficient is not an integer has no algebraic-integer root, provided the root is irrational: the minimal polynomial of an algebraic integer has integer coefficients, and for an irrational root this quadratic is the minimal polynomial. The x² + x = 7/4 helper of #68 is the case where the trick is cheaper; this is the general form, needed because the second axis of #81 has 17 in its denominators.

The word's axis in closed form

theorem QuantumInfo.SU2.htB_pos : 0 < htB

theorem QuantumInfo.SU2.htA_sq : htA ^ 2 = (5 + 2 * √2) / 17

theorem QuantumInfo.SU2.htB_sq : htB ^ 2 = (7 - 4 * √2) / 17

The second axis and its angle

The π rotation about the word's axis, followed by H, is a rotation about (1, 0, -1)/√2: the cross product of the two axes. Its angle is wAngle.

noncomputable def QuantumInfo.SU2.wHalfCos : ℝ

The cosine of half the second rotation's angle.

Equations

• QuantumInfo.SU2.wHalfCos = -(√2 * QuantumInfo.SU2.htA)

noncomputable def QuantumInfo.SU2.wAngle : ℝ

The angle of the second rotation.

Equations

• QuantumInfo.SU2.wAngle = 2 * Real.arccos QuantumInfo.SU2.wHalfCos

theorem QuantumInfo.SU2.wHalfCos_sq : wHalfCos ^ 2 = (10 + 4 * √2) / 17

theorem QuantumInfo.SU2.sqrt_two_lt_seven_quarters : √2 < 7 / 4

theorem QuantumInfo.SU2.wHalfCos_sq_lt_one : wHalfCos ^ 2 < 1

theorem QuantumInfo.SU2.wHalfCos_mem : -1 ≤ wHalfCos ∧ wHalfCos ≤ 1

theorem QuantumInfo.SU2.cos_wAngle_half : Real.cos (wAngle / 2) = wHalfCos

theorem QuantumInfo.SU2.sin_wAngle_half : Real.sin (wAngle / 2) = htB

theorem QuantumInfo.SU2.two_mul_cos_wAngle : 2 * Real.cos wAngle = (6 + 16 * √2) / 17

The second angle in the form the algebraic-integer test wants.

theorem QuantumInfo.SU2.irrational_two_mul_cos_wAngle : Irrational (2 * Real.cos wAngle)

theorem QuantumInfo.SU2.not_isIntegral_two_mul_cos_wAngle : ¬IsIntegral ℤ (2 * Real.cos wAngle)

theorem QuantumInfo.SU2.irrational_wAngle_div_two_pi : Irrational (wAngle / (2 * Real.pi))

★★ The second angle is an irrational multiple of 2π, so the powers of the second rotation fill its own circle.

theorem QuantumInfo.SU2.irrational_wAngle_div_four_pi : Irrational (wAngle / (4 * Real.pi))

Conjugation moves the axis

theorem QuantumInfo.SU2.axisRot_neg_axis (a b c θ : ℝ) : axisRot (-a) (-b) (-c) θ = axisRot a b c (-θ)

theorem QuantumInfo.SU2.ryMat_conj_rzMat (t : ℝ) : Euler.ryMat (Real.pi / 4) * Euler.rzMat t * Euler.ryMat (-(Real.pi / 4)) = axisRot (√2 / 2) 0 (√2 / 2) t

Conjugating a z rotation by R_y(π/4) tilts its axis to (1, 0, 1)/√2.

theorem QuantumInfo.SU2.ryMat_conj_axisRot_x (t : ℝ) : Euler.ryMat (Real.pi / 4) * axisRot 1 0 0 t * Euler.ryMat (-(Real.pi / 4)) = axisRot (√2 / 2) 0 (-(√2 / 2)) t

Conjugating an x rotation by R_y(π/4) tilts its axis to (1, 0, -1)/√2.

theorem QuantumInfo.SU2.rzMat_conj_ryMat (γ : ℝ) : Euler.rzMat (-(Real.pi / 2)) * Euler.ryMat γ * Euler.rzMat (Real.pi / 2) = axisRot 1 0 0 γ

Conjugating a y rotation by R_z(-π/2) turns its axis into x.

The Euler decomposition about two explicit orthogonal axes

theorem QuantumInfo.SU2.conj_mul_three {g g' A B C : Matrix (Fin 2) (Fin 2) ℂ} (h : g' * g = 1) : g * A * g' * (g * B * g') * (g * C * g') = g * (A * B * C) * g'

theorem QuantumInfo.SU2.exists_euler_zxz {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) (hdet : U.det = 1) : ∃ (β : ℝ) (γ : ℝ) (δ : ℝ), U = Euler.rzMat β * axisRot 1 0 0 γ * Euler.rzMat δ

The z-x-z Euler decomposition, from the z-y-z one by conjugating with R_z(π/2).

theorem QuantumInfo.SU2.exists_euler_two_axes {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) (hdet : U.det = 1) : ∃ (β : ℝ) (γ : ℝ) (δ : ℝ), U = axisRot (√2 / 2) 0 (√2 / 2) β * axisRot (√2 / 2) 0 (-(√2 / 2)) γ * axisRot (√2 / 2) 0 (√2 / 2) δ

★★ The Euler decomposition about the two orthogonal axes (1, 0, ±1)/√2: every determinant-one unitary is a product of three rotations about them, alternating. These are the two axes the Clifford+T words reach.

The generators as a monoid

theorem QuantumInfo.SU2.hGateM_mul_self : CliffordT.hGateM * CliffordT.hGateM = 1

theorem QuantumInfo.SU2.tGateM_pow (n : ℕ) : CliffordT.tGateM ^ n = !![1, 0; 0, tPhase ^ n]

theorem QuantumInfo.SU2.tGateM_pow_eight : CliffordT.tGateM ^ 8 = 1

theorem QuantumInfo.SU2.pow_mul_pow_eq_one {A B : Matrix (Fin 2) (Fin 2) ℂ} (h : A * B = 1) (n : ℕ) : A ^ n * B ^ n = 1

noncomputable def QuantumInfo.SU2.cliffordT : Submonoid (Matrix (Fin 2) (Fin 2) ℂ)

The monoid of Clifford+T words on one qubit.

Equations

• QuantumInfo.SU2.cliffordT = Submonoid.closure {QuantumInfo.CliffordT.hGateM, QuantumInfo.CliffordT.tGateM}

noncomputable def QuantumInfo.SU2.cliffordTLim : Submonoid (Matrix (Fin 2) (Fin 2) ℂ)

The limits of Clifford+T words: a closed submonoid of the 2 × 2 matrices.

Equations

• QuantumInfo.SU2.cliffordTLim = QuantumInfo.SU2.cliffordT.topologicalClosure

theorem QuantumInfo.SU2.hGateM_mem : CliffordT.hGateM ∈ cliffordT

theorem QuantumInfo.SU2.tGateM_mem : CliffordT.tGateM ∈ cliffordT

theorem QuantumInfo.SU2.cliffordT_le_lim : cliffordT ≤ cliffordTLim

theorem QuantumInfo.SU2.isClosed_cliffordTLim : IsClosed ↑cliffordTLim

A dense circle of angles fills the circle

theorem QuantumInfo.SU2.mem_closure_range_axisRot_of_irrational {a b c θ : ℝ} (hirr : Irrational (θ / (4 * Real.pi))) (α : ℝ) : axisRot a b c α ∈ closure (Set.range fun (k : ℤ) => axisRot a b c (↑k * θ))

The rotations about a fixed axis by the integer multiples of an angle that is an irrational multiple of 4π are dense in the whole circle of rotations about that axis.

theorem QuantumInfo.SU2.axisRot_int_mul_mem {K : Submonoid (Matrix (Fin 2) (Fin 2) ℂ)} {a b c θ : ℝ} (hu : a ^ 2 + b ^ 2 + c ^ 2 = 1) (hg : axisRot a b c θ ∈ K) (hg' : axisRot a b c (-θ) ∈ K) (k : ℤ) : axisRot a b c (↑k * θ) ∈ K

theorem QuantumInfo.SU2.axisRot_mem_of_irrational {K : Submonoid (Matrix (Fin 2) (Fin 2) ℂ)} (hK : IsClosed ↑K) {a b c θ : ℝ} (hu : a ^ 2 + b ^ 2 + c ^ 2 = 1) (hirr : Irrational (θ / (4 * Real.pi))) (hg : axisRot a b c θ ∈ K) (hg' : axisRot a b c (-θ) ∈ K) (α : ℝ) : axisRot a b c α ∈ K

★ One rotation with an irrationally related angle gives the whole circle, inside any closed submonoid that contains it and its inverse.

The two circles the words reach

theorem QuantumInfo.SU2.wAxis_unit : (√2 / 2) ^ 2 + 0 ^ 2 + (-(√2 / 2)) ^ 2 = 1

theorem QuantumInfo.SU2.uAxis_unit : (√2 / 2) ^ 2 + 0 ^ 2 + (√2 / 2) ^ 2 = 1

theorem QuantumInfo.SU2.sqrt_two_inv_eq : (√2)⁻¹ = √2 / 2

theorem QuantumInfo.SU2.hGateM_eq_smul_su2 : CliffordT.hGateM = Complex.I • su2 0 (√2)⁻¹ 0 (√2)⁻¹

H is the π rotation about (1, 0, 1)/√2, up to the phase i.

theorem QuantumInfo.SU2.axisRot_htAxis_pi_mul_hGateM : axisRot htA htB htA Real.pi * CliffordT.hGateM = Complex.I • axisRot (√2 / 2) 0 (-(√2 / 2)) wAngle

★ The second axis. The π rotation about the word's axis, followed by H, is (up to the phase i) a rotation about (1, 0, -1)/√2 — the cross product of the two axes — through wAngle.

The first circle is reached by the word's powers

theorem QuantumInfo.SU2.htht_mem : CliffordT.htht ∈ cliffordT

theorem QuantumInfo.SU2.hthtInv_mem : CliffordT.hGateM * CliffordT.tGateM ^ 7 * CliffordT.hGateM * CliffordT.tGateM ^ 7 ∈ cliffordT

theorem QuantumInfo.SU2.htht_mul_inv : CliffordT.htht * (CliffordT.hGateM * CliffordT.tGateM ^ 7 * CliffordT.hGateM * CliffordT.tGateM ^ 7) = 1

theorem QuantumInfo.SU2.axisRot_htAxis_eight : axisRot htA htB htA (8 * CliffordT.htAngle) = CliffordT.htht ^ 8

theorem QuantumInfo.SU2.axisRot_htAxis_eight_mem : axisRot htA htB htA (8 * CliffordT.htAngle) ∈ cliffordTLim

theorem QuantumInfo.SU2.axisRot_htAxis_neg_eight_mem : axisRot htA htB htA (-(8 * CliffordT.htAngle)) ∈ cliffordTLim

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

theorem QuantumInfo.SU2.axisRot_htAxis_mem (α : ℝ) : axisRot htA htB htA α ∈ cliffordTLim

★★ Every rotation about the word's own axis is a limit of Clifford+T words.

The second circle

theorem QuantumInfo.SU2.piRot_mul_hGateM_mem : axisRot htA htB htA Real.pi * CliffordT.hGateM ∈ cliffordTLim

theorem QuantumInfo.SU2.hGateM_mul_piRot_mem : CliffordT.hGateM * axisRot htA htB htA (-Real.pi) ∈ cliffordTLim

theorem QuantumInfo.SU2.piRot_mul_hGateM_mul_inv : axisRot htA htB htA Real.pi * CliffordT.hGateM * (CliffordT.hGateM * axisRot htA htB htA (-Real.pi)) = 1

theorem QuantumInfo.SU2.axisRot_wAxis_four : (axisRot htA htB htA Real.pi * CliffordT.hGateM) ^ 4 = axisRot (√2 / 2) 0 (-(√2 / 2)) (4 * wAngle)

theorem QuantumInfo.SU2.irrational_four_wAngle : Irrational (4 * wAngle / (4 * Real.pi))

theorem QuantumInfo.SU2.axisRot_wAxis_mem (α : ℝ) : axisRot (√2 / 2) 0 (-(√2 / 2)) α ∈ cliffordTLim

★★ Every rotation about (1, 0, -1)/√2 is a limit of Clifford+T words.

The third circle: conjugating by Z

noncomputable def QuantumInfo.SU2.zGateM : Matrix (Fin 2) (Fin 2) ℂ

Z, as the fourth power of T.

Equations

• QuantumInfo.SU2.zGateM = QuantumInfo.CliffordT.tGateM ^ 4

theorem QuantumInfo.SU2.tPhase_pow_four : tPhase ^ 4 = -1

theorem QuantumInfo.SU2.zGateM_eq : zGateM = !![1, 0; 0, -1]

theorem QuantumInfo.SU2.zGateM_conj_su2 (w x y z : ℝ) : zGateM * su2 w x y z * zGateM = su2 w (-x) (-y) z

theorem QuantumInfo.SU2.zGateM_conj_axisRot (α : ℝ) : zGateM * axisRot (√2 / 2) 0 (-(√2 / 2)) (-α) * zGateM = axisRot (√2 / 2) 0 (√2 / 2) α

theorem QuantumInfo.SU2.axisRot_uAxis_mem (α : ℝ) : axisRot (√2 / 2) 0 (√2 / 2) α ∈ cliffordTLim

★★ Every rotation about (1, 0, 1)/√2 is a limit of Clifford+T words — the Z conjugate of the second circle, and the axis orthogonal to it.

Clifford+T fills SU(2)

theorem QuantumInfo.SU2.det_one_mem_cliffordTLim {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) (hdet : U.det = 1) : U ∈ cliffordTLim

★★ Every determinant-one 2 × 2 unitary is a limit of Clifford+T words. The two circles (1, 0, ±1)/√2 are orthogonal, so the Euler decomposition about them writes any such unitary as a product of three rotations, each of them a limit of words.

theorem QuantumInfo.SU2.exists_phase_mem_cliffordTLim {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin 2) ℂ) : ∃ (φ : ℝ), Euler.expI φ • U ∈ cliffordTLim

★★ Clifford+T is dense in U(2) modulo phase: every 2 × 2 unitary becomes a limit of Clifford+T words after multiplication by one phase.