Distance-Independent Universality of Clifford+T
Jens Palsberg, Keli Huang, Abdullah Almanei
quant-ph
Oct 2, 2026 · v1
TL;DR
The universality theorem for Clifford+T with respect to any projective distance measure is formally proved in Lean.
Abstract
A well-known theorem states that the Clifford+T gate set is universal for quantum computing. The theorem combines approximation using a distance measure on unitary matrices with equality up to global phase. Previous proofs combine these two notions for specific distance measures, but do not identify the properties that govern how they work together. Which properties are sufficient to state and prove the theorem? We answer this question by defining projective distance measures using four axioms. We prove that the universality theorem holds for every distance measure satisfying these axioms. Thus, our formulation of the theorem is independent of any particular choice of distance measure. We show that the Hilbert-Schmidt distance is already a projective distance measure. We also develop a general construction that transforms a large class of distance measures into projective distance measures and apply it to obtain projective versions of the operator-norm distance, the Frobenius distance, and the trace distance. Finally, we formalize the proof of the universality theorem in Lean.
Problem
Proofs that the Clifford+T gate set is universal combine approximation under a distance measure with equality up to global phase. Existing proofs do this for specific distance measures and do not say which properties make the two notions work together.
Approach
Projective distance measures are defined by four axioms that extend traditional distance properties with projective (global-phase) invariance. Universality is proved for every such measure in three steps. First, any unitary is decomposed up to phase into Clifford+Rz gates. Second, Rz gates are approximated using a gate G1 built from T and H. A general construction, minimizing over global phase, turns traditional distances into projective ones. The full proof is formalized in Lean.
Results
Clifford+T is universal with respect to any projective distance measure. The Hilbert-Schmidt distance is shown to be projective, and projective versions of the operator-norm, Frobenius, and trace distances are obtained. The theorem is mechanically verified in Lean.
