p. 3 — d(I, exp(iH)) ≤ ‖H‖ for Hermitian H

Proved

SKAlgorithm.Qudit.dist_one_exp_le

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

matrix-exponentialoperator-normp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1solovay-kitaev

Let $H$ be a $d \times d$ Hermitian matrix. Then, in operator norm,

d(I, \exp(iH)) = \|I - \exp(iH)\| \le \|H\|.

The paper derives it from the identity $d(I, \exp(iH)) = \max_E 2\sin(|E|/2)$ over the eigenvalues $E$ of $H$ . It converts bounds on Hermitian generators into bounds on distances from the identity.

Formalization Note. Only the inequality is stated. The identity $d(I, \exp(iH)) = \max_E 2\sin(|E|/2)$ printed in the same sentence is not formalized: as printed it fails when some $|E| > \pi$ (for $H = 3\pi$ in dimension one the left side is $2$ and the right side is $-2$ ); the correct form has $2|\sin(E/2)|$ . The exponential is NormedSpace.exp on complex matrices and the norm is QAlgorithms.specNorm.

Preamble

import Mathlib
import Definitions.Def_SKAlgorithm_Qudit_Model

open scoped Matrix
open QAlgorithms

Formal statement

namespace SKAlgorithm.Qudit

theorem dist_one_exp_le {d : ℕ} (H : Matrix (Fin d) (Fin d) ℂ) (hH : H.IsHermitian) :
    specNorm (1 - NormedSpace.exp (Complex.I • H)) ≤ specNorm H := by sorry

end SKAlgorithm.Qudit

Source

Dawson and Nielsen, The Solovay-Kitaev algorithm, arXiv:quant-ph/0505030v2, p. 3, §2, 'From this it follows easily that d(I, exp(iH)) ≤ ‖H‖'

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