LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A Quantitative Balanced Commutator in SU(2)

Statement

For a matrix $M$ , write $e^{M} = \sum_{j \geq 0} M^{j} / j!$ . Here $S U (2) : = {M \in M_{2} (C) : M^{*} M = I_{2}, \det M = 1}$ . If $D \in S U (2)$ and $0 \leq ∥ D - I ∥ \leq η \leq 1 / 16$ , there are $V, W \in S U (2)$ such that $∥ V - I ∥, ∥ W - I ∥ \leq \sqrt{η}, ∥ D - V W V^{*} W^{*} ∥ \leq 40 η^{3 / 2} .$

Facts & Assumptions

Given: $D \in S U (2)$ and $0 \leq ∥ D - I ∥ \leq η \leq 1 / 16$ .

[F1]

The near-identity logarithm is traceless and skew-Hermitian and has norm at most $2 η$ (A Quantitative Logarithm Near the Identity in SU(2)).

[F2]

For real vectors $a, b$ , Pauli multiplication gives $[i a \cdot σ, i b \cdot σ] = - 2 i (a \times b) \cdot σ$ (Pauli Vector Multiplication and Commutator Formula).

[F3]

The operator norm is submultiplicative (The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2).

[F4]

Euler's formula and the Pythagorean identity give $e^{i t} = \cos t + i \sin t$ and $\cos^{2} t + \sin^{2} t = 1$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[F5]

Sine is differentiable with derivative cosine and $\sin 0 = 0$ (The derivatives of sine and cosine are cosine and minus sine); the mean value theorem applies to a continuous function on a closed interval that is differentiable in its interior (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[F6]

The operator-norm triangle inequality follows from its definition by applying the vector triangle inequality to each unit input and taking the maximum (The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||).

Proof

1.1F1F2givenconstruct

Write $X = \log D = i v \cdot σ$ with $v \in R^{3}$ ; the Pauli matrices form a real basis of the traceless skew-Hermitian $2 \times 2$ matrices, and [F2] gives $∥ X ∥ = ∣ v ∣$ . If $v = 0$ , take $a = b = 0$ and $V = W = I$ . Otherwise set $u = v / ∣ v ∣$ , choose the smallest index $k \in {1, 2, 3}$ attaining $\min_{i} ∣ u_{i} ∣$ , and let $e_{k}$ be the corresponding coordinate vector. Then $w = u \times e_{k}$ has norm at least $\sqrt{2 / 3} > 1 / 2$ ; put $e = w / ∣ w ∣$ . This is a deterministic choice with $e ⊥ u$ . Set $a = \sqrt{∣ v ∣ / 2} e$ and $b = - \sqrt{∣ v ∣ / 2} (u \times e)$ . Then $a \times b = - v / 2$ and $∣ a ∣ = ∣ b ∣ = \sqrt{∣ v ∣ / 2} \leq \sqrt{η}$ .

2.1F2F4F5step 1.1algebra

For every real $t$ , $∣ \sin t ∣ \leq ∣ t ∣$ : it is immediate at $t = 0$ , and otherwise [F5] and the mean value theorem give $\sin t - \sin 0 = \cos (c) t$ for some $c$ between $0$ and $t$ ; [F4] implies $∣ \cos c ∣ \leq 1$ . Put $A = i a \cdot σ$ , $B = i b \cdot σ$ , $V = e^{A}$ and $W = e^{B}$ . For $a \neq 0$ , $P = a \cdot σ / ∣ a ∣$ is Hermitian, traceless and satisfies $P^{2} = I$ by [F2]; its eigenvalues are $1, - 1$ . Thus $e^{A} = I \cos ∣ a ∣ + i P \sin ∣ a ∣$ by the power series and [F4], so it is unitary with determinant $1$ and $∥ e^{A} - I ∥ = 2 ∣ \sin (∣ a ∣ / 2) ∣ \leq ∣ a ∣$ . If $a = 0$ , $e^{A} = I$ ; the same argument applies to $B$ . By [F2], $[A, B] = X$ , and both distances are at most $\sqrt{η}$ .

3.1F3F6step 2.1algebra

Expand $e^{A} e^{B} e^{- A} e^{- B}$ as a sum of homogeneous terms in $A, B$ . Its degree-one terms cancel, and direct multiplication of the degree-two terms gives $A B - B A = [A, B]$ . By [F3], products have norm at most the product of their norms; the triangle inequality [F6] therefore bounds the sum of norms of all terms of total degree $n$ by $(4 s)^{n} / n!$ , where $s = \max (∥ A ∥, ∥ B ∥) \leq 1 / 4$ . Hence the degree-at-least-three remainder has norm at most $(4 s)^{3} e^{4 s} / 6 < 32 s^{3}$ .

4.1F1F3F6step 2.1step 3.1algebra∎

The exponential series and [F3] give $∥ e^{X} - I - X ∥ \leq ∥ X ∥^{2} e^{∥ X ∥} / 2 \leq 2 s^{4} e^{2 s^{2}} \leq s^{3}$ , since $∥ X ∥ = ∥ [A, B] ∥ \leq 2 s^{2}$ and $s \leq 1 / 4$ . By the triangle inequality [F6], $∥ e^{X} - e^{A} e^{B} e^{- A} e^{- B} ∥ \leq 33 s^{3} \leq 40 η^{3 / 2}$ . By [F1], $e^{X} = D$ ; step 2.1 gives $[A, B] = X$ , and step 3.1 controls the commutator expansion. These facts prove the claim.

Depends on

Used by

Solovay–Kitaev Unitary Compiler for SU(2) Algorithm
Error Cancellation in an SU(2) Commutator Lemma
Finite-Precision Bit Complexity of the SU(2) Solovay–Kitaev Compiler Theorem
Solovay–Kitaev Error and Resource Bound Theorem

Dependency tree · two levels

41 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Christopher M. Dawson and Michael A. Nielsen, The Solovay–Kitaev Algorithm, arXiv:quant-ph/0505030v2 (standard reference, not scraped)
Dieter van Melkebeek and Thomas Watson, Time-Space Efficient Simulations of Quantum Computations (standard reference, not scraped)