The rotation angle of T·HTH is an irrational multiple of π

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

T·HTH is e^{iπ/4} times an element of SU(2) whose half-trace is cos²(π/8) (trace_htht, det_htht): a rotation by the angle htAngle with cos(htAngle/2) = cos²(π/8), so cos htAngle = (2√2 − 1)/4. That angle is an irrational multiple of 2π, which is why the powers of one Clifford+T word already fill a whole one-parameter rotation subgroup — the engine of Clifford+T universality.

The obstruction is arithmetic. If θ is a rational multiple of 2π then e^{iθ} is a root of unity, hence an algebraic integer, and so is its inverse, so 2 cos θ is an algebraic integer (★ isIntegral_two_mul_cos_of_eq_two_pi_mul, a general fact Mathlib lacks at the pin). But x = 2 cos htAngle = √2 − 1/2 satisfies x² + x = 7/4, so if it were an algebraic integer then 7/4 would be one too, and ℤ is integrally closed in ℚ (★ not_isIntegral_of_sq_add_self_eq).

• ★ isIntegral_two_mul_cos_of_eq_two_pi_mul — 2 cos(2πq) is an algebraic integer;
• ★ not_isIntegral_of_sq_add_self_eq — no algebraic integer satisfies x² + x = 7/4;
• htHalfAngle, htAngle; cos_sq_pi_div_eight, cos_htHalfAngle, cos_htAngle;
• ★★ irrational_htAngle_div_two_pi — htAngle/(2π) is irrational;
• ★ denseRange_zsmul_htAngle — the integer multiples of htAngle are dense in the circle ℝ/2πℤ; ★★ exists_zsmul_htAngle_approx — the concrete form: every angle is approximated by k·htAngle modulo 2π, to any accuracy;
• hGateM, tGateM, htht; trace_htht, det_htht, ★ trace_htht_eq_cos_htAngle — the gate's angle is htAngle: tr(T·HTH) = 2 cos(htAngle/2) e^{iπ/4} and det(T·HTH) = e^{iπ/2}.

Honest scope

⚠️ This is the angle of one Clifford+T word and the density of its own powers. That ⟨H, T⟩ is dense in U(2) modulo phase needs a second axis and the Euler decomposition: BACKLOG #81, done 2026-09-26 in CsdLean4/Mathlib/QuantumInfo/CliffordTDensity.lean. The extension to U(2ⁿ) is #70–#73. No efficiency claim: Solovay–Kitaev is #74 and is not attempted.

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 (the Solovay–Kitaev setting); specs/magic-plan.md; specs/BACKLOG.md #68; specs/future-work.md.

Two cosines of rational angles are algebraic integers

theorem isIntegral_two_mul_cos_of_eq_two_pi_mul {θ : ℝ} {q : ℚ} (hθ : θ = 2 * Real.pi * ↑q) : IsIntegral ℤ (2 * Real.cos θ)

★ 2 cos θ is an algebraic integer whenever θ is a rational multiple of 2π: e^{iθ} is then a root of unity, so it and its inverse are algebraic integers, and 2 cos θ is their sum.

x² + x = 7/4 has no algebraic-integer solution

theorem not_isIntegral_of_sq_add_self_eq {x : ℝ} (hx : x ^ 2 + x = 7 / 4) : ¬IsIntegral ℤ x

★ No algebraic integer satisfies x² + x = 7/4: it would make 7/4 an algebraic integer, and ℤ is integrally closed in ℚ.

The angle of T·HTH

noncomputable def QuantumInfo.CliffordT.htHalfAngle : ℝ

Half the rotation angle of T·HTH: the angle whose cosine is cos²(π/8).

Equations

• QuantumInfo.CliffordT.htHalfAngle = Real.arccos (Real.cos (Real.pi / 8) ^ 2)

noncomputable def QuantumInfo.CliffordT.htAngle : ℝ

The rotation angle of T·HTH.

Equations

• QuantumInfo.CliffordT.htAngle = 2 * QuantumInfo.CliffordT.htHalfAngle

theorem QuantumInfo.CliffordT.cos_sq_pi_div_eight : Real.cos (Real.pi / 8) ^ 2 = (2 + √2) / 4

theorem QuantumInfo.CliffordT.cos_htHalfAngle : Real.cos htHalfAngle = Real.cos (Real.pi / 8) ^ 2

theorem QuantumInfo.CliffordT.sq_sqrt_two : √2 ^ 2 = 2

theorem QuantumInfo.CliffordT.cos_htAngle : Real.cos htAngle = (2 * √2 - 1) / 4

theorem QuantumInfo.CliffordT.sq_add_self_two_mul_cos_htAngle : (2 * Real.cos htAngle) ^ 2 + 2 * Real.cos htAngle = 7 / 4

theorem QuantumInfo.CliffordT.irrational_htAngle_div_two_pi : Irrational (htAngle / (2 * Real.pi))

★★ The angle of T·HTH is an irrational multiple of 2π.

theorem QuantumInfo.CliffordT.denseRange_zsmul_htAngle : DenseRange fun (k : ℤ) => k • ↑htAngle

★ The integer multiples of htAngle are dense in the circle ℝ/2πℤ.

theorem QuantumInfo.CliffordT.dense_closure_htAngle : Dense ↑(AddSubgroup.closure {htAngle, 2 * Real.pi})

The subgroup generated by htAngle and 2π is dense in ℝ.

theorem QuantumInfo.CliffordT.exists_zsmul_htAngle_approx (α : ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ (k : ℤ) (m : ℤ), |↑k * htAngle + ↑m * (2 * Real.pi) - α| < ε

★★ Every angle is an integer multiple of htAngle modulo 2π, to any accuracy. This is the form the gate-approximation argument consumes: repeating the Clifford+T word T·HTH k times realises any rotation about its axis, as closely as required.

The gate

noncomputable def QuantumInfo.CliffordT.hGateM : Matrix (Fin 2) (Fin 2) ℂ

The Hadamard as a 2 × 2 matrix.

Equations

• QuantumInfo.CliffordT.hGateM = (↑√2)⁻¹ • !![1, 1; 1, -1]

noncomputable def QuantumInfo.CliffordT.tGateM : Matrix (Fin 2) (Fin 2) ℂ

The T gate as a 2 × 2 matrix.

Equations

• QuantumInfo.CliffordT.tGateM = !![1, 0; 0, QuantumInfo.tPhase]

noncomputable def QuantumInfo.CliffordT.htht : Matrix (Fin 2) (Fin 2) ℂ

The Clifford+T word T·H·T·H.

Equations

• QuantumInfo.CliffordT.htht = QuantumInfo.CliffordT.tGateM * QuantumInfo.CliffordT.hGateM * QuantumInfo.CliffordT.tGateM * QuantumInfo.CliffordT.hGateM

theorem QuantumInfo.CliffordT.sqrt_two_inv_sq_two : (↑√2)⁻¹ * (↑√2)⁻¹ * 2 = 1

theorem QuantumInfo.CliffordT.htht_eq : htht = ((↑√2)⁻¹ * (↑√2)⁻¹) • !![1 + tPhase, 1 - tPhase; tPhase * (1 - tPhase), tPhase * (1 + tPhase)]

theorem QuantumInfo.CliffordT.trace_htht : htht.trace = (1 + tPhase) ^ 2 / 2

The trace of the Clifford+T word: (1 + e^{iπ/4})²/2.

theorem QuantumInfo.CliffordT.det_htht : htht.det = tPhase ^ 2

The determinant of the Clifford+T word: e^{iπ/2} = i.

noncomputable def QuantumInfo.CliffordT.tPhase8 : ℂ

e^{iπ/8}, the square root of the T phase.

Equations

• QuantumInfo.CliffordT.tPhase8 = Complex.exp (↑(Real.pi / 8) * Complex.I)

theorem QuantumInfo.CliffordT.tPhase8_sq : tPhase8 ^ 2 = tPhase

theorem QuantumInfo.CliffordT.tPhase8_ne_zero : tPhase8 ≠ 0

theorem QuantumInfo.CliffordT.tPhase8_add_inv : tPhase8 + tPhase8⁻¹ = 2 * ↑(Real.cos (Real.pi / 8))

theorem QuantumInfo.CliffordT.one_add_tPhase : 1 + tPhase = 2 * ↑(Real.cos (Real.pi / 8)) * tPhase8

1 + e^{iπ/4} = 2 cos(π/8) e^{iπ/8}.

theorem QuantumInfo.CliffordT.trace_htht_eq_cos_htAngle : htht.trace = 2 * ↑(Real.cos (htAngle / 2)) * tPhase

★ The gate's rotation angle is htAngle: tr(T·HTH) = 2 cos(htAngle/2) e^{iπ/4}, and det(T·HTH) = e^{iπ/2} (det_htht), so e^{−iπ/4}·T·HTH lies in SU(2) with half-trace cos(htAngle/2) = cos²(π/8): it is a rotation by htAngle.