The Solovay–Kitaev recursion: why the error contracts at exponent 3/2

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

#112 contracts a commutator, #114 produces one, #113 supplies the base case. This file is the step that turns them into a recursion, and the whole content is why the exponent is 3/2 and not 1.

Replace each factor of a commutator by a δ-approximation and the naive estimate is 4δ (#112's norm_groupCommutator_sub_groupCommutator_le) — which contracts nothing, since the input error was already δ. The gain comes from the commutator being bilinear in the deviations from the identity: the leading term is (v - ṽ)w + ṽ(w - w̃) - (w - w̃)v - w̃(v - ṽ), every summand pairing a factor norm with an approximation error. With #114's factors at √(2ε) and the approximations at δ, that is O(√ε · δ) — and with δ = ε it is ε^{3/2}.

What is proved

• ★ norm_mul_sub_mul_le' — the two-factor perturbation bound in any normed ring, ‖AB - A′B′‖ ≤ ‖A - A′‖·‖B‖ + ‖A′‖·‖B - B′‖, which is what makes the pairing visible;
• ★★★ norm_groupCommutator_sub_le — the sharp estimate: ‖[V,W] - [Ṽ,W̃]‖ ≤ 4aδ(1 + a) where a bounds all four distances to the identity and δ the two approximation errors. Against #112's 4δ this is smaller by a factor a, and that factor is the whole algorithm;
• ★★ norm_groupCommutator_sub_le_sqrt — the same estimate at #114's factor size, a = √2·√ε: ‖[V,W] - [Ṽ,W̃]‖ ≤ 4√2·√ε·δ·(1 + √2·√ε), the √ε · δ form the recursion consumes;
• ★★★ skError_le_rpow — the error bookkeeping, in closed form: a sequence with ε_{n+1} ≤ C·ε_n^{3/2} satisfies C²·ε_n ≤ (C²·ε_0)^{(3/2)^n}, by induction through Real.rpow. This is the inequality #116 takes logarithms of.

Honest scope

⚠️ The length half of the recursion is not here, and it is not a formality. The row asked for both bookkeeping facts; this file proves the error one. The length one (ℓ_{n+1} = 5ℓ_n) needs a notion of word length in the generating set, and the corpus has none: cliffordT is Submonoid.closure {H, T}, a set of matrices with no length function, and #113's net is a Finset of matrices rather than of words. Supplying that is new infrastructure (a free monoid on the generators, its evaluation, and the net restated as words), not an exercise.

⚠️ And the exponent 3.97 assumes a gate set closed under inverses, which cliffordT is not. The recursion uses Ṽ⁻¹ and W̃⁻¹; in a monoid generated by H and T alone, T⁻¹ = T⁷, so inverting a word multiplies its length by up to 7 and the per-level factor is 1+1+7+7+1 = 17 rather than 5. The honest exponent for this generating set is therefore log 17 / log(3/2) ≈ 6.99, not log 5 / log(3/2) ≈ 3.97; recovering 3.97 means generating with H, T, T⁻¹ (or S = T² and its inverse), which is a different submonoid from the one #73/#81 prove dense. Nothing below depends on either choice — the error recursion is indifferent to it — but #116 must state which set it means.

⚠️ No approximant is constructed. skError_le_rpow is a statement about real sequences; it says what the recursion's error does given the recurrence, and the recurrence is justified by the estimates above rather than by an implemented algorithm.

References: C. Dawson, M. Nielsen, The Solovay-Kitaev algorithm, Quantum Inf. Comput. 6 (2006) 81, §4–5 (the recursion and its error analysis); M. Nielsen, I. Chuang, Quantum Computation and Quantum Information, Appendix 3; GroupCommutator.lean (#112), CommutatorDecomposition.lean (#114), CliffordTNet.lean (#113); specs/BACKLOG.md #115, #74, #112, #113, #114, #116.

The pairing that makes the exponent 3/2

theorem CSD.SolovayKitaev.norm_mul_sub_mul_le' {E : Type u_1} [NormedRing E] (A B A' B' : E) : ‖A * B - A' * B'‖ ≤ ‖A - A'‖ * ‖B‖ + ‖A'‖ * ‖B - B'‖

★ The two-factor perturbation bound. AB - A′B′ = (A - A′)B + A′(B - B′), so each summand pairs one difference with one factor — which is what lets a small factor norm multiply the approximation error instead of adding to it.

theorem CSD.SolovayKitaev.norm_mul_sub_mul_comm_sub_le {E : Type u_1} [NormedRing E] {V W V' W' : E} {a δ : ℝ} (haW : ‖W - 1‖ ≤ a) (haV' : ‖V' - 1‖ ≤ a) (haV : ‖V - 1‖ ≤ a) (haW' : ‖W' - 1‖ ≤ a) (hδV : ‖V - V'‖ ≤ δ) (hδW : ‖W - W'‖ ≤ δ) : ‖V * W - W * V - (V' * W' - W' * V')‖ ≤ 4 * a * δ

The deviation of a commutator's two factors, as a single product.

theorem CSD.SolovayKitaev.norm_groupCommutator_sub_le {E : Type u_1} [NormedRing E] [StarRing E] [CStarRing E] {V W V' W' : E} (hV : V ∈ unitary E) (hW : W ∈ unitary E) (hV' : V' ∈ unitary E) (hW' : W' ∈ unitary E) {a δ : ℝ} (haV : ‖V - 1‖ ≤ a) (haW : ‖W - 1‖ ≤ a) (haV' : ‖V' - 1‖ ≤ a) (haW' : ‖W' - 1‖ ≤ a) (hδV : ‖V - V'‖ ≤ δ) (hδW : ‖W - W'‖ ≤ δ) : ‖V * W * star V * star W - V' * W' * star V' * star W'‖ ≤ 4 * a * δ * (1 + a)

★★★ The sharp commutator-perturbation estimate, and the reason Solovay–Kitaev converges. Replacing both factors by δ-approximations moves the commutator by at most 4aδ(1 + a), where a bounds the factors' distance to the identity.

#112's norm_groupCommutator_sub_groupCommutator_le gives 4δ, which contracts nothing. The extra factor a here is the whole algorithm: with #114's factors at a = √(2ε) and δ = ε, the output error is O(ε^{3/2}).

theorem CSD.SolovayKitaev.norm_groupCommutator_sub_le_sqrt {E : Type u_1} [NormedRing E] [StarRing E] [CStarRing E] {V W V' W' : E} (hV : V ∈ unitary E) (hW : W ∈ unitary E) (hV' : V' ∈ unitary E) (hW' : W' ∈ unitary E) {ε δ : ℝ} (haV : ‖V - 1‖ ≤ √2 * √ε) (haW : ‖W - 1‖ ≤ √2 * √ε) (haV' : ‖V' - 1‖ ≤ √2 * √ε) (haW' : ‖W' - 1‖ ≤ √2 * √ε) (hδV : ‖V - V'‖ ≤ δ) (hδW : ‖W - W'‖ ≤ δ) : ‖V * W * star V * star W - V' * W' * star V' * star W'‖ ≤ 4 * (√2 * √ε) * δ * (1 + √2 * √ε)

★★ The estimate at #114's factor size. With the factors √2·√ε-close to the identity, the commutator of two δ-approximations is within 4√2·√ε·δ·(1 + √2·√ε) of the commutator — the √ε · δ shape the recursion consumes, which at δ = ε is ε^{3/2}.

The error bookkeeping

theorem CSD.SolovayKitaev.skError_le_rpow {C : ℝ} (hC : 0 < C) {ε : ℕ → ℝ} (hε : ∀ (n : ℕ), 0 ≤ ε n) (hrec : ∀ (n : ℕ), ε (n + 1) ≤ C * ε n ^ (3 / 2)) (n : ℕ) : C ^ 2 * ε n ≤ (C ^ 2 * ε 0) ^ (3 / 2) ^ n

★★★ The recursion's error, in closed form. A sequence obeying ε_{n+1} ≤ C·ε_n^{3/2} satisfies C²·ε_n ≤ (C²·ε_0)^{(3/2)^n}: the error is doubly exponentially small in the number of levels, which is what makes the gate count only polylogarithmic. This is the inequality #116 takes logarithms of.