TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Solovay–Kitaev Error and Resource Bound

Statement

For a fixed inverse-closed dense $G \subset S U (2)$ and a certified base net of radius $0 < η_{0} < 64^{- 2}$ and a target $U \in S U (2)$ , the level recursion $Compile (U, J)$ of Solovay–Kitaev Unitary Compiler for SU(2) returns, for every real $0 < ε \leq η_{0}$ , a word $W$ with $∥ U - W ∥ \leq ε$ , where $J$ is the least nonnegative integer with $η_{J} \leq ε$ . For a real tolerance this means selecting $J$ by ideal exact-real comparisons and calling the level subroutine directly; the algorithm's top-level tolerance input is rational. The level errors may be chosen as $η_{j} = 64^{- 2} (64^{2} η_{0})^{(3 / 2)^{j}} .$ The word length is at most $L_{0} 5^{j}$ at level $j$ , hence $O (\log^{\log_{3 / 2} 5} (1 / ε)) = O (\log^{3.97} (1 / ε))$ . With shared recursive words, the exact-real arithmetic count is $O (\log^{\log_{3 / 2} 3} (1 / ε)) = O (\log^{2.71} (1 / ε))$ ; printing the expanded word takes $O (\log^{3.97} (1 / ε))$ time. The latter are exact-real arithmetic bounds, not bit-complexity bounds.

Facts & Assumptions

Given: The fixed gate package and base-net certificate, a target $U \in S U (2)$ , and a real $0 < ε \leq η_{0} < 64^{- 2}$ , with ideal exact-real comparisons for selecting the level.

[F1]

The compiler uses a level-zero word within $η_{0}$ and at each later level uses one lower-level approximation to $U$ and two to the balanced commutator factors (Solovay–Kitaev Unitary Compiler for SU(2)).

[F2]

If $∥ D - I ∥ \leq η \leq 1 / 16$ , there are $V, W$ within $\sqrt{η}$ of $I$ whose commutator is within $40 η^{3 / 2}$ of $D$ (A Quantitative Balanced Commutator in SU(2)).

[F3]

Approximating each of $V, W$ within $η$ changes their commutator by at most $5 η^{3 / 2}$ when both are within $\sqrt{η}$ of $I$ (Error Cancellation in an SU(2) Commutator).

[F4]

Every compiled gate word is unitary because its letters lie in $G \subset S U (2)$ (Inverse-Closed Dense SU(2) Gate Set). From the operator-norm definition (The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||), left multiplication by a unitary preserves norm because it preserves vector norms, and right multiplication preserves norm because it maps the unit sphere bijectively to itself.

[F5]

$\log$ denotes the natural logarithm, the inverse of the positive real exponential; it is strictly increasing, $\log 1 = 0$ , and it obeys the product and reciprocal laws. For $b > 0$ , $b \neq 1$ , set $\log_{b} x : = \log x / \log b$ . For $x > 0$ and real $t$ , use $x^{t} : = \exp (t \log x)$ ; the logarithm product law and inverse relation imply $(x y)^{t} = x^{t} y^{t}$ and $(x^{s})^{t} = x^{s t}$ for positive $x, y$ and real $s, t$ . Also $⌈ y ⌉ : = - ⌊ - y ⌋$ , where $⌊ \cdot ⌋$ is the integer part (The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

Proof

1.1F1F4givenalgebra

We prove by induction that level $j$ has error at most $η_{j}$ . The base net gives error at most $η_{0}$ at level zero. Suppose the lower-level word $A$ has error at most $η_{j - 1}$ . Since $A$ is unitary, right multiplication by $A^{*}$ maps the unit sphere bijectively to itself; the operator-norm definition in [F4] therefore gives $∥ D - I ∥ = ∥ (U - A) A^{*} ∥ = ∥ U - A ∥ \leq η_{j - 1}$ .

2.1F1F2F3F4step 1.1algebra

By [F2] choose $V, W$ within $\sqrt{η_{j - 1}}$ of $I$ whose exact commutator differs from $D$ by at most $40 η_{j - 1}^{3 / 2}$ . The level- $(j - 1)$ words $B, C$ approximate $V, W$ within $η_{j - 1}$ , so [F3] bounds the additional commutator error by $5 η_{j - 1}^{3 / 2}$ . The combined bound follows from the operator-norm triangle inequality, which follows from [F4] and the vector triangle inequality. If $C_{0} = B C B^{*} C^{*} A$ , then $U - C_{0} = (D - B C B^{*} C^{*}) A$ ; right multiplication by the unitary $A$ preserves norm by [F4]. Thus the returned word approximates $U$ to at most $45 η_{j - 1}^{3 / 2} \leq 64 η_{j - 1}^{3 / 2} = η_{j}$ .

3.1F5step 2.1algebra

Set $q_{j} = 64^{2} η_{j}$ and $q_{0} = 64^{2} η_{0} \in (0, 1)$ . The recurrence gives $q_{j + 1} = q_{j}^{3 / 2}$ ; with the positive-real-power convention in [F5], induction yields $q_{j} = q_{0}^{(3 / 2)^{j}}$ and hence the displayed error formula. Put $q_{ε} = 64^{2} ε \in (0, q_{0}]$ . Since $\log$ is strictly increasing and obeys the reciprocal law [F5], $η_{j} \leq ε$ is equivalent to ${(\frac{3}{2})}^{j} \geq \frac{\log (1 / q_{ε})}{\log (1 / q_{0})} .$ The ratio is at least $1$ , and $\log_{3 / 2}$ is increasing because $3 / 2 > 1$ and $\log$ is strictly increasing. Thus the least nonnegative integer level is $J = ⌈ \log_{3 / 2} \frac{\log (1 / (64^{2} ε))}{\log (1 / (64^{2} η_{0}))} ⌉,$ with the ceiling convention in [F5].

4.1F1step 3.1algebra∎

The recursive word contains two copies each of the level- $(j - 1)$ words $B, C$ and one copy of $A$ , so its length is at most $5 L_{j - 1}$ and hence at most $L_{0} 5^{j}$ . The recursion tree has three recursive calls per node, so its shared-DAG arithmetic count is $O (3^{j})$ ; expanding and printing the word takes at most $O (5^{j})$ . Since $j = O (\log \log (1 / ε))$ , these are respectively $O (\log^{\log_{3 / 2} 3} (1 / ε))$ and $O (\log^{\log_{3 / 2} 5} (1 / ε))$ .

Depends on

Used by

Classical output, quantum-state output, and access costs Definition
A Three-Factor Solovay–Kitaev Error Budget Example
Fibonacci SU(2) compiler error, length, and bit cost Theorem
Finite universal-gate compilation cost for the truncated QFT Theorem
Finite-Precision Bit Complexity of the SU(2) Solovay–Kitaev Compiler Theorem
Fixed-Arity Unitary Error Budget Theorem

Cited to discharge well-definedness by Solovay–Kitaev Unitary Compiler for SU(2).

Dependency tree · two levels

37 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)
Ronald de Wolf, Quantum Computing: Lecture Notes, arXiv:1907.09415v6 (standard reference, not scraped)