p. 3 — reversing and inverting an ε-approximating sequence gives an ε-approximation to U†

Proved

SKAlgorithm.Qudit.inverse_sequence

by mikedeng1 · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-compilingsolovay-kitaev

Let $\mathcal G \subseteq SU(d)$ be a finite set of gates closed under $g \mapsto g^\dagger$ , and let $S = g_1, \dots, g_m$ be a sequence of gates from $\mathcal G$ that is an $\epsilon$ -approximation to a gate $U \in SU(d)$ , i.e. $d(U, S) < \epsilon$ . Then the inverse sequence $S^\dagger = g_m^\dagger, \dots, g_1^\dagger$ consists of gates from $\mathcal G$ , and

d(U^\dagger, S^\dagger) < \epsilon.

This is the reason Definition 1 requires an instruction set to be closed under adjoints: the recursion of the Solovay-Kitaev algorithm needs approximations to $V^\dagger$ and $W^\dagger$ given approximations to $V$ and $W$ .

Preamble

import Mathlib
import Definitions.Def_SKAlgorithm_Qudit_Model

open scoped Matrix
open QAlgorithms

Formal statement

namespace SKAlgorithm.Qudit

theorem inverse_sequence {d : ℕ} (G : Finset (SU d)) (hG : ∀ g ∈ G, g⁻¹ ∈ G)
    (U : SU d) (S : List (SU d)) (hS : ∀ g ∈ S, g ∈ G) (ε : ℝ)
    (hU : opDist U (seqUnitary S) < ε) :
    (∀ g ∈ invSeq S, g ∈ G) ∧ opDist U⁻¹ (seqUnitary (invSeq S)) < ε := by sorry

end SKAlgorithm.Qudit

Source

Dawson and Nielsen, The Solovay-Kitaev algorithm, arXiv:quant-ph/0505030v2, p. 3, §2, 'the easily-verified fact that if we have an instruction sequence providing an ǫ-approximation to some unitary U …'

Human review

Endorsed by Shuze Chen · Oct 22, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 22, 2026
Confirmed by the mission captain (proposal self-audit).

View graph