SU(2) is compact, so the Clifford+T words contain a finite ε-net

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #113, the second brick of #74's split.

Solovay–Kitaev's base case needs a finite set of words within ε₀ of every target. #81 gives density (det_one_mem_cliffordTLim), and density alone gives one word per target — a set with no finiteness and no bound. Compactness is what upgrades it, and that is all this file does.

What is proved

• ★★ IsCompact.exists_finite_net — the general statement, in any metric space: a compact set inside the closure of D is covered by finitely many ε-balls centred in D. Density plus compactness gives a finite net; neither alone does;
• ★ isClosed_unitaryGroup — the unitary group of any finite index type is closed, as the preimage of {1} under U ↦ U⋆U. Mathlib has IsCompact.matrix for entrywise-compact sets but nothing about the unitary group, so this is new here;
• ★★ isCompact_su2Set — the special unitary 2 × 2 matrices are compact: closed (the unitary condition and det = 1 are both closed conditions) and inside the closed unit ball, because a unitary has operator norm 1 in the C*-norm;
• ★★★ exists_finite_cliffordT_net — the base case: for every ε > 0 there is a Finset of genuine Clifford+T words such that every determinant-one unitary is within ε of one of them.

Honest scope

⚠️ Existence, not construction. The net comes from elim_finite_subcover, so nothing here bounds its cardinality or the length of its words. That is not a gap to be filled later by the same argument: it is why Solovay–Kitaev needs a recursion on top of the net (#115), and why the net is the O(1) base of the algorithm rather than the algorithm.

⚠️ ε₀ is not calibrated. The recursion needs the base accuracy to be below the contraction threshold of #112 (δ < 1/2); this file produces a net for every ε, and choosing the one the recursion wants is #115's business.

⚠️ The route is not the one #113 recorded. The row proposed the su2 parametrisation — SU(2) as the continuous image of the unit sphere in ℝ⁴ — which would need the surjectivity of that parametrisation onto the determinant-one unitaries, and the corpus has no such statement. Closed and bounded in a finite-dimensional space is shorter and needs nothing new, so that is what is used; the sphere picture appears nowhere below.

⚠️ Modulo phase is not addressed. The net is for det = 1; the phase quotient of exists_phase_mem_cliffordTLim is untouched, as in #81.

References: C. Dawson, M. Nielsen, The Solovay-Kitaev algorithm, Quantum Inf. Comput. 6 (2006) 81, §3 (the ε₀-net as the base case); M. Nielsen, I. Chuang, Quantum Computation and Quantum Information, Appendix 3; CliffordTDensity.lean (#81), GroupCommutator.lean (#112); specs/BACKLOG.md #113, #74, #81, #112, #115, #116.

Density plus compactness gives a finite net

theorem IsCompact.exists_finite_net {X : Type u_1} [MetricSpace X] {K D : Set X} (hK : IsCompact K) (hKD : K ⊆ closure D) {ε : ℝ} (hε : 0 < ε) : ∃ (F : Finset X), ↑F ⊆ D ∧ ∀ x ∈ K, ∃ y ∈ F, dist x y < ε

★★ A compact set inside the closure of D has a finite ε-net drawn from D. Density on its own gives one point of D per target; compactness is what makes finitely many of them enough.

The unitary group is closed

theorem QuantumInfo.SU2.isClosed_unitaryGroup {n : Type u_1} [Fintype n] [DecidableEq n] : IsClosed ↑(Matrix.unitaryGroup n ℂ)

★ The unitary group is closed, as the preimage of {1} under U ↦ U U⋆.

SU(2) is compact

def QuantumInfo.SU2.su2Set : Set (Matrix (Fin 2) (Fin 2) ℂ)

The determinant-one unitaries: the target set Solovay–Kitaev approximates.

Equations

• QuantumInfo.SU2.su2Set = {U : Matrix (Fin 2) (Fin 2) ℂ | U ∈ Matrix.unitaryGroup (Fin 2) ℂ ∧ U.det = 1}

theorem QuantumInfo.SU2.isClosed_su2Set : IsClosed su2Set

theorem QuantumInfo.SU2.su2Set_subset_closedBall : su2Set ⊆ Metric.closedBall 0 1

A unitary has operator norm 1, so the target set sits in the closed unit ball.

theorem QuantumInfo.SU2.isCompact_su2Set : IsCompact su2Set

★★ The special unitary 2 × 2 matrices are compact: closed, and bounded because a unitary has operator norm 1.

The base case

theorem QuantumInfo.SU2.su2Set_subset_closure_cliffordT : su2Set ⊆ closure ↑cliffordT

#81's density, as an inclusion of sets.

theorem QuantumInfo.SU2.exists_finite_cliffordT_net {ε : ℝ} (hε : 0 < ε) : ∃ (F : Finset (Matrix (Fin 2) (Fin 2) ℂ)), (∀ A ∈ F, A ∈ cliffordT) ∧ ∀ U ∈ su2Set, ∃ A ∈ F, dist U A < ε

★★★ The base case of Solovay–Kitaev. For every ε > 0 there are finitely many genuine Clifford+T words such that every determinant-one unitary is within ε of one of them.

Density (#81) gives one word per target; compactness of the target set turns that into a finite list. ⚠️ Existence only — the net's size and its words' lengths are not bounded here, which is exactly why the recursion is needed on top of it.