Solovay–Kitaev Unitary Compiler for SU(2)

Inputs: A fixed inverse-closed dense gate package $G$ with the finite base-net certificate $({\mathcal{N}}_0,{\eta }_0,L_0)$ from Inverse-Closed Dense SU(2) Gate Set, an exact-real target $U\in SU(2)$, and a rational $0<\epsilon \le {\eta }_0$. This is an ideal exact-real procedure: fixed-dimensional exact matrix arithmetic, matrix logarithm/exponential, and exact comparisons are unit-cost operations. It is not, by this definition alone, a finite Turing algorithm.

Set ${\eta }_{j+1}=64{\eta }_j^{3\mathrm{/}2}$ for $j\ge 0$. Choose the least integer $J\ge 0$ with ${\eta }_J\le \epsilon$. Define $\mathrm{Compile}(U,j)$ recursively:

1. If $j=0$, return the first word $A\in {\mathcal{N}}_0$ with $\mathrm{\parallel }U-A\mathrm{\parallel }\le {\eta }_0$.
2. If $j>0$, set $A=\mathrm{Compile}(U,j-1)$ and $D=U{A}^{\ast }$. If $D=I$, set $V=W=I$. Otherwise apply the Pauli-coordinate construction in A Quantitative Balanced Commutator in SU(2) to $D$ and ${\eta }_{j-1}$, obtaining $V,W\in SU(2)$ with $D$ approximated by $VW{V}^{\ast }{W}^{\ast }$.
3. Set $B=\mathrm{Compile}(V,j-1)$ and $C=\mathrm{Compile}(W,j-1)$. Return the word $BC{B}^{\ast }{C}^{\ast }A$. Store concatenations and inverses as a shared expression DAG; an inverse word is formed by reversing its label order and replacing each label by its listed inverse. Expanding the DAG writes the ordinary gate word.

Return $\mathrm{Compile}(U,J)$. The recursion depth is finite because each call decreases the nonnegative integer $j$.

Solovay–Kitaev Error and Resource Bound ↗ establishes this procedure's level existence and recursive admissibility: its step 3.1 gives the least finite $J$, while steps 1.1–2.1 give the inductive bound $\mathrm{\parallel }D-I\mathrm{\parallel }\le {\eta }_{j-1}$ for every balanced-commutator call. The displayed level formula has $0<{\eta }_j\le {\eta }_0<{64}^{-2}<1\mathrm{/}16$, so each such call satisfies the lemma's norm and radius hypotheses. The base-net certificate supplies the level-zero choice. This is the well-definedness justification for the instructions above; the error and resource conclusions are stated and proved in that theorem.