Group commutators of an ϵ²-net of S_ϵ form an O(ϵ³)-net of S_{ϵ²}

Proved

QAlgorithms.Childs.commutator_net

by Goku · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

childslecture-notesquantum-information

For $U,V\in SU(2)$ write $[\![U,V]\!]=UVU^{-1}V^{-1}$ for the group commutator. For $\epsilon\ge0$ let

S_\epsilon=\{U\in SU(2):\|I-U\|\le\epsilon\}

be the $\epsilon$ -ball around the identity, with $\|\cdot\|$ the spectral norm. For $\Gamma,S\subseteq SU(2)$ , $\Gamma$ is a $\delta$ -net for $S$ if every $A\in S$ has some $U\in\Gamma$ with $\|A-U\|\le\delta$ .

The lemma says there are constants $C>0$ and $\epsilon_0>0$ such that, for every $0<\epsilon\le\epsilon_0$ and every $\Gamma\subseteq SU(2)$ , the following holds. If $\Gamma$ is an $\epsilon^2$ -net for $S_\epsilon$ , then

[\![\Gamma,\Gamma]\!]=\{[\![U,V]\!]:U,V\in\Gamma\}\ \text{is a } C\epsilon^3\text{-net for } S_{\epsilon^2}.

This is the key step of the Solovay–Kitaev construction. Applied recursively, it turns a coarse net near the identity into nets of doubly-exponentially improving precision.

Formalization Note The source writes $O(\epsilon^3)$ as $\epsilon\to0$ . Here it is written as explicit constants $C$ and $\epsilon_0$ , chosen before $\Gamma$ , because the source's recursion uses one constant at every level.

Preamble

import Definitions.Def_QAlgorithms_Defs_Circuit
set_option autoImplicit false

Formal statement

namespace QAlgorithms.Childs

open QAlgorithms



/-- Childs, Lemma 2.3, PDF p. 16. If `Γ ⊆ SU(2)` is an `ϵ²`-net for `S_ϵ = {U ∈ SU(2) :
‖I − U‖ ≤ ϵ}`, then `⟦Γ, Γ⟧ = {U V U⁻¹ V⁻¹ : U, V ∈ Γ}` is an `O(ϵ³)`-net for `S_{ϵ²}`.
The `O(ϵ³)` is with respect to `ϵ → 0` (PDF p. 17), with a constant independent of `Γ` (the
recursion on p. 16 uses one constant `k` at every level): there are `C > 0` and `ϵ₀ > 0` such
that for every `0 < ϵ ≤ ϵ₀` and every such `Γ`, `⟦Γ, Γ⟧` is a `C ϵ³`-net for `S_{ϵ²}`. -/
theorem commutator_net :
    ∃ C : ℝ, 0 < C ∧ ∃ ε₀ : ℝ, 0 < ε₀ ∧ ∀ ε : ℝ, 0 < ε → ε ≤ ε₀ →
      ∀ Γ : Set (Matrix.specialUnitaryGroup (Fin 2) ℂ),
        IsNet Γ (su2Ball ε) (ε ^ 2) → IsNet (commutatorSet Γ) (su2Ball (ε ^ 2)) (C * ε ^ 3) := by
  sorry

end QAlgorithms.Childs

Source

Andrew Childs, Lecture Notes on Quantum Algorithms, 17 April 2025, PDF p. 16, Lemma 2.3. https://www.cs.umd.edu/~amchilds/qa/qa.pdf

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Notation.

$\mathrm{SU}(2)$ denotes the group of $2 \times 2$ complex unitary matrices with determinant $1$ .
$\|\cdot\|$ is the spectral norm.
For $r \in \mathbb{R}$ , the ball around the identity is

\mathrm{Ball}(r) = \{U \in \mathrm{SU}(2) : \|I - U\| \le r\}.

For sets $\Gamma, S \subseteq \mathrm{SU}(2)$ and $\delta \in \mathbb{R}$ , say " $\Gamma$ is a $\delta$ -net for $S$ " if every $A \in S$ has some $U \in \Gamma$ with $\|A - U\| \le \delta$ . The set $\Gamma$ is not required to lie inside $S$ .
The commutator set of $\Gamma$ is

[\Gamma, \Gamma] = \{U V U^{-1} V^{-1} : U, V \in \Gamma\}.

Group inverses in $\mathrm{SU}(2)$ are conjugate transposes.

Statement. There exist real constants $C > 0$ and $\varepsilon_0 > 0$ such that the following holds. For every real $\varepsilon$ with $0 < \varepsilon \le \varepsilon_0$ and every set $\Gamma \subseteq \mathrm{SU}(2)$ :

\text{if } \Gamma \text{ is an } \varepsilon^2\text{-net for } \mathrm{Ball}(\varepsilon), \text{ then } [\Gamma, \Gamma] \text{ is a } C\varepsilon^3\text{-net for } \mathrm{Ball}(\varepsilon^2).

The constants $C$ and $\varepsilon_0$ are asserted only to exist; they are universal, independent of $\varepsilon$ and $\Gamma$ .

Human review

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

View graph