The Solovay–Kitaev theorem, with its gate count

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #116, the last brick of #74's split, and with it link 12.

#115 proved the error side (C²ε_n ≤ (C²ε₀)^{(3/2)ⁿ}) and #117 the length side (ℓ_n ≤ 5ⁿℓ₀). Two things were left: eliminate n between them, and supply the pairing — which word approximates a given U. This file does both, so the chain ends on a single statement about Clifford+T words.

The count

skLevel b ε = ⌈log R / log(3/2)⌉ where R = log ε / log b is how many times the base accuracy's exponent must double-and-a-half to reach ε. ★★ skLevel_rpow_le says that many levels really do reach ε; ★★ five_pow_skLevel_le says five to that power is at most 5·R^c, with

skExponent = log 5 / log (3/2),

and ★ three_lt_skExponent/★ skExponent_lt_four place c in (3, 4) — the literature's ≈ 3.97 — each by one application of Real.log_lt_log to (3/2)³ = 27/8 < 5 < 81/16 = (3/2)⁴. No decimal expansion is claimed.

The pairing

★★★ exists_mem_skWords_norm_sub_le is the recursion: from a net at base accuracy e, the level-n words of #117's shape reach skErr e n on every determinant-one unitary. One level approximates U, takes the residual Δ = U·(ctEval u)⋆, writes it as a group commutator of two near-identity determinant-one factors (#114), approximates those one level down, and reassembles. The reassembled approximant is a word because ★★ star_ctEval identifies #117's ctInvWord with the adjoint — so a group commutator of word values is the value of v ++ w ++ ctInvWord v ++ ctInvWord w, exactly skWords' shape, and the length bound transfers untouched.

Two things had to be built for that step, neither of them bookkeeping:

• ★ ctEval_mem_unitary — words are unitary (hGateM_mem_unitary, tGateM_mem_unitary, which the corpus did not have), so right multiplication by one is an isometry and the residual is as close to 1 as the approximation is good;
• the determinant. #114 needs its input to have determinant one, and a Clifford+T word does not. It is forced: ★ det_ctEval_pow_eight — the determinant of a word is an eighth root of unity, because H² = 1 and T⁸ = 1 and nothing else enters — together with ★★ eq_one_of_pow_eight_eq_one: an eighth root of unity within 1/8 of 1 is 1. That last needs no root-of-unity theory, only (z−1)·∑_{k<8} zᵏ = z⁸ − 1 = 0 and ‖1 − zᵏ‖ ≤ k‖1 − z‖ on the unit circle, which bounds the sum by 28/8 < 8.

#114 was strengthened in place to record that its factors are determinant one (axisRot_det, det_conj_of_mem_unitary), which its construction already gave.

The theorem

★★★ exists_word_approx_polylog: for every determinant-one U and every small enough ε, a Clifford+T word within ε of U of length at most K·log(1/ε)^c.

Honest scope

⚠️ K and ε₀ are existential, by inheritance. #113's net comes from compactness with no bound on its size, and the radius forcing the residual's determinant comes from continuity of det. Neither is quantitative, so no constant here is. The exponent is.

⚠️ The exponent is #117's cost model, not a fact about {H, T}. The letters are H, T and T⁻¹, so inverting a word is free and a level costs five. Over two letters a shortest T⁻¹ is T⁷, a level costs 17, and the exponent is log 17 / log(3/2) ≈ 6.99. #117's ★★ mem_cliffordT_iff_exists_word is what makes the choice free: the three letters generate exactly the submonoid the two do. The literature's 3 + δ needs a different net argument and stays unclaimed.

⚠️ Nothing is computed. The word is produced by a recursion over an existence statement, not by an algorithm, and skErr's constant 33 is a sufficient one rather than the best.

References: C. Dawson, M. Nielsen, The Solovay-Kitaev algorithm, Quantum Inf. Comput. 6 (2006) 81, §§3–5; SolovayKitaevStep.lean (#115), CliffordTWords.lean (#117), CliffordTNet.lean (#113), CommutatorDecomposition.lean (#114), CliffordTDensity.lean (#81); specs/BACKLOG.md #116, #74, #113, #114, #115, #117.

The exponent

noncomputable def QuantumInfo.SU2.skExponent : ℝ

The Solovay–Kitaev exponent log 5 / log (3/2), in the three-letter cost model of #117.

Equations

• QuantumInfo.SU2.skExponent = Real.log 5 / Real.log (3 / 2)

theorem QuantumInfo.SU2.log_three_halves_pos : 0 < Real.log (3 / 2)

theorem QuantumInfo.SU2.skExponent_pos : 0 < skExponent

theorem QuantumInfo.SU2.skExponent_lt_four : skExponent < 4

★ The exponent is below 4, because 5 < (3/2)⁴ = 81/16.

theorem QuantumInfo.SU2.three_lt_skExponent : 3 < skExponent

★ And above 3, because (3/2)³ = 27/8 < 5.

The level count

noncomputable def QuantumInfo.SU2.skLevel (b ε : ℝ) : ℕ

The number of recursion levels needed to turn base accuracy b into accuracy ε.

Equations

• QuantumInfo.SU2.skLevel b ε = ⌈Real.log (Real.log ε / Real.log b) / Real.log (3 / 2)⌉₊

theorem QuantumInfo.SU2.one_le_log_ratio {b ε : ℝ} (hb : 0 < b) (hb1 : b < 1) (hε : 0 < ε) (hεb : ε ≤ b) : 1 ≤ Real.log ε / Real.log b

theorem QuantumInfo.SU2.log_ratio_pos {b ε : ℝ} (hb : 0 < b) (hb1 : b < 1) (hε : 0 < ε) (hεb : ε ≤ b) : 0 < Real.log ε / Real.log b

theorem QuantumInfo.SU2.log_ratio_le_three_halves_pow {b ε : ℝ} (hb : 0 < b) (hb1 : b < 1) (hε : 0 < ε) (hεb : ε ≤ b) : Real.log ε / Real.log b ≤ (3 / 2) ^ skLevel b ε

(3/2) to the level is at least the ratio: that many levels really do reach ε.

theorem QuantumInfo.SU2.skLevel_rpow_le {b ε : ℝ} (hb : 0 < b) (hb1 : b < 1) (hε : 0 < ε) (hεb : ε ≤ b) : b ^ (3 / 2) ^ skLevel b ε ≤ ε

★★ The level count reaches the target accuracy.

theorem QuantumInfo.SU2.five_pow_skLevel_le {b ε : ℝ} (hb : 0 < b) (hb1 : b < 1) (hε : 0 < ε) (hεb : ε ≤ b) : 5 ^ skLevel b ε ≤ 5 * (Real.log ε / Real.log b) ^ skExponent

★★ And five to that power is only 5·R^c — the whole polylogarithmic gate count, with c the exponent and R = log ε / log b the ratio of logarithms.

Clifford+T words are unitary, with determinant an eighth root of unity

theorem QuantumInfo.SU2.star_hGateM : star CliffordT.hGateM = CliffordT.hGateM

theorem QuantumInfo.SU2.hGateM_mem_unitary : CliffordT.hGateM ∈ unitary (Matrix (Fin 2) (Fin 2) ℂ)

theorem QuantumInfo.SU2.conj_tPhase : (starRingEnd ℂ) tPhase = tPhaseInv

theorem QuantumInfo.SU2.star_tGateM : star CliffordT.tGateM = !![1, 0; 0, tPhaseInv]

theorem QuantumInfo.SU2.tGateM_mem_unitary : CliffordT.tGateM ∈ unitary (Matrix (Fin 2) (Fin 2) ℂ)

theorem QuantumInfo.SU2.ctGen_mem_unitary (i : Fin 3) : ctGen i ∈ unitary (Matrix (Fin 2) (Fin 2) ℂ)

theorem QuantumInfo.SU2.ctEval_mem_unitary (w : List (Fin 3)) : ctEval w ∈ unitary (Matrix (Fin 2) (Fin 2) ℂ)

★ Every Clifford+T word is a unitary.

theorem QuantumInfo.SU2.star_ctEval (w : List (Fin 3)) : star (ctEval w) = ctEval (ctInvWord w)

★★ The inverse word is the adjoint. #117 produced a left inverse; for a unitary that is the star, so the group commutator of two word values is again a word value.

theorem QuantumInfo.SU2.det_ctGen_pow_eight (i : Fin 3) : (ctGen i).det ^ 8 = 1

theorem QuantumInfo.SU2.det_ctEval_pow_eight (w : List (Fin 3)) : (ctEval w).det ^ 8 = 1

★ The determinant of a word is an eighth root of unity — det H = -1 and det T has order eight, and nothing else enters.

An eighth root of unity near one is one

theorem QuantumInfo.SU2.eq_one_of_pow_eight_eq_one {z : ℂ} (h8 : z ^ 8 = 1) (hz : ‖z - 1‖ ≤ 1 / 8) : z = 1

★★ An eighth root of unity within 1/8 of 1 is 1. The eight roots are 2π/8 apart, so this is a gap statement; the proof needs no root-of-unity theory, only that (z - 1)·∑_{k<8} zᵏ = z⁸ - 1 = 0 and that each ‖1 - zᵏ‖ ≤ k·‖1 - z‖ on the unit circle, which bounds the sum by 28/8 < 8.

theorem QuantumInfo.SU2.exists_det_radius : ∃ (r : ℝ), 0 < r ∧ ∀ (A : Matrix (Fin 2) (Fin 2) ℂ), ‖A - 1‖ < r → ‖A.det - 1‖ ≤ 1 / 8

The radius within which a matrix's determinant is forced within 1/8 of 1: det is continuous, and no constant is claimed.

The error of the recursion

noncomputable def QuantumInfo.SU2.skErr (e : ℝ) : ℕ → ℝ

The error after n levels of the recursion, from base accuracy e. The constant 33 is what the step below actually achieves at √e ≤ 1/2; #115's closed form then applies to it verbatim.

Equations

• QuantumInfo.SU2.skErr e 0 = e
• QuantumInfo.SU2.skErr e n.succ = 33 * QuantumInfo.SU2.skErr e n ^ (3 / 2)

@[simp]

theorem QuantumInfo.SU2.skErr_zero (e : ℝ) : skErr e 0 = e

theorem QuantumInfo.SU2.skErr_succ (e : ℝ) (n : ℕ) : skErr e (n + 1) = 33 * skErr e n ^ (3 / 2)

theorem QuantumInfo.SU2.rpow_three_halves {x : ℝ} (hx : 0 ≤ x) : x ^ (3 / 2) = √x ^ 3

theorem QuantumInfo.SU2.skErr_nonneg {e : ℝ} (he : 0 ≤ e) (n : ℕ) : 0 ≤ skErr e n

theorem QuantumInfo.SU2.skErr_le_base {e : ℝ} (he : 0 ≤ e) (hs : √e ≤ 1 / 33) (n : ℕ) : skErr e n ≤ e

The error never exceeds the base accuracy: the recursion only improves.

theorem QuantumInfo.SU2.step_arith {t : ℝ} (ht0 : 0 ≤ t) (ht : t ≤ 1 / 2) : 4 * (√2 * t + t ^ 2) * t ^ 2 * (1 + (√2 * t + t ^ 2)) ≤ 33 * t ^ 3

The step's arithmetic, stated in the square root alone so that nothing can rewrite inside it.

theorem QuantumInfo.SU2.step_bound {ε : ℝ} (hε : 0 ≤ ε) (hs : √ε ≤ 1 / 2) : 4 * (√2 * √ε + ε) * ε * (1 + (√2 * √ε + ε)) ≤ 33 * ε ^ (3 / 2)

The step's error bound: 4aδ(1+a) at a = √2·√ε + ε and δ = ε is at most 33·ε^{3/2}.

The recursion

theorem QuantumInfo.SU2.exists_mem_skWords_norm_sub_le {F : Finset (List (Fin 3))} {e r : ℝ} (he : 0 ≤ e) (hsmall : √e ≤ 1 / 33) (hr : e < r) (hdet : ∀ (A : Matrix (Fin 2) (Fin 2) ℂ), ‖A - 1‖ < r → ‖A.det - 1‖ ≤ 1 / 8) (hnet : ∀ U ∈ su2Set, ∃ w ∈ F, ‖U - ctEval w‖ ≤ e) (n : ℕ) (U : Matrix (Fin 2) (Fin 2) ℂ) : U ∈ su2Set → ∃ u ∈ skWords F n, ‖U - ctEval u‖ ≤ skErr e n

★★★ The Solovay–Kitaev recursion, over words. From a net at base accuracy e, the level-n words of #117's shape reach accuracy skErr e n on every determinant-one unitary.

This is the pairing #117 declined to make: it says which words approximate a given U. One level: approximate U by a level-n word u; take the residual Δ = U·(ctEval u)⋆, which is within ε of 1 because right multiplication by a unitary is an isometry; write Δ as a group commutator of two factors √(2ε)-close to the identity (#114, which now also records that they are determinant one); approximate those at level n; reassemble.

The reassembled approximant is a word because #117's ctInvWord inverts a word and ★★ star_ctEval identifies that inverse with the adjoint — so the group commutator of two word values is the value of v ++ w ++ ctInvWord v ++ ctInvWord w, which is exactly the shape of skWords, and #117's length bound applies unchanged.

The determinant is the one step that is not formal: the residual must be determinant one to feed #114, and a Clifford+T word is not. It is forced — the determinant of a word is an eighth root of unity (★ det_ctEval_pow_eight), the residual is near 1, and ★★ eq_one_of_pow_eight_eq_one says an eighth root of unity near 1 is 1.

The theorem

theorem QuantumInfo.SU2.exists_word_approx_polylog : ∃ (K : ℝ) (e : ℝ), 0 < K ∧ 0 < e ∧ ∀ (ε : ℝ), 0 < ε → ε ≤ e → ∀ U ∈ su2Set, ∃ (u : List (Fin 3)), ‖U - ctEval u‖ ≤ ε ∧ ↑u.length ≤ K * Real.log ε⁻¹ ^ skExponent

★★★ Solovay–Kitaev, with the gate count: link 12's last statement. For every U of determinant one and every small enough ε, there is a Clifford+T word within ε of U whose length is at most K·log(1/ε)^c, with c = skExponent ∈ (3, 4).

The three inputs meet here: #117's net gives the base case and the length recursion 5ⁿℓ₀, ★★★ exists_mem_skWords_norm_sub_le says which level-n word to take, #115's ★★★ skError_le_rpow turns the per-level contraction into 33²ε_n ≤ (33²ε₀)^{(3/2)ⁿ}, and ★★ skLevel_rpow_le/★★ five_pow_skLevel_le eliminate n between the two.

⚠️ K and ε₀ are existential, and that is inherited, not laziness. #113's net comes from compactness with no bound on its size, and the radius forcing the residual's determinant comes from continuity of det; neither is quantitative, so no constant here can be. What is quantitative is the exponent.

⚠️ The cost model is #117's three letters H, T, T⁻¹ — see this file's header. The literature's 3 + δ needs a different net and stays unclaimed.