The Rz approximation procedure is correct when it returns

If $\epsilon \ge c$, the direct branch returns the zero-T Clifford word whose error bound is proved in [F11]. Suppose instead $0<\epsilon <c$. If the procedure returns, its successful candidate satisfies the scaled-grid real-part inequality by construction and [A2] gives the exact norm equation. Thus $\mathrm{\mid }u{\mathrm{\mid }}^2+\mathrm{\mid }t{\mathrm{\mid }}^2=1$; multiplying the displayed matrix by its conjugate transpose gives $U^{\ast }U=I$ and $\det U=\mathrm{\mid }u{\mathrm{\mid }}^2+\mathrm{\mid }t{\mathrm{\mid }}^2=1$. Therefore $U$ is in the form required by [F2], which gives $\mathrm{\parallel }{R}_z(\theta )-U{\mathrm{\parallel }}_{\mathrm{o}\mathrm{p}}\le \epsilon$.

Since $T$ and $R_z(\theta )$ are diagonal, they commute. By [F7], unitary left and right multiplication preserve the operator norm: the left factor preserves every vector norm, and the right factor bijects the unit sphere to itself. Thus $\mathrm{\parallel }{R}_z(\theta )-TU{T}^{†}{\mathrm{\parallel }}_{\mathrm{o}\mathrm{p}}=\mathrm{\parallel }{T}^{†}{R}_z(\theta )T-U{\mathrm{\parallel }}_{\mathrm{o}\mathrm{p}}=\mathrm{\parallel }{R}_z(\theta )-U{\mathrm{\parallel }}_{\mathrm{o}\mathrm{p}}$. Thus both compiler inputs meet the same error bound.

If $\epsilon \ge c$, [A1] makes the direct integer-part operation terminate, so the zero-T word is returned. Suppose $0<\epsilon <c$. Then $\epsilon <1\mathrm{/}2$, and [F3] gives a solvable grid candidate with some finite exponent $k$. By [F4], each layer from $0$ through $k$ has finitely many coefficient vectors. The finite-search alternative checks them all; the default iterator enumerates precisely the candidates and finishes each preceding layer by [F9]. By [F8], each norm call terminates and it succeeds when that candidate is reached; the finitely many comparison and oracle calls terminate by [A1]. Therefore the unbounded loop terminates after finitely many earlier layers and candidates. A finite candidate limit may instead cause TIMEOUT before this point.

The exact compiler conclusion [F5] makes each returned word's matrix equal its selected input. Since the procedure chooses between $U$ and $U^{\mathrm{\prime }}$, step 2.1 proves the returned word satisfies the required bound.

For efficient factored mode, take a fixed exponent $k$ for one solvable candidate from [F3]. There are only finitely many candidates in layers through $k$, independent of their within-layer order. The iterator finishes each preceding layer for every random-bit sequence by [F9]. On each of these finitely many algebraic inputs, the norm call terminates with probability one by [F10]. With fresh independent solver bits this remains true conditional on the history, so the finite union of nontermination events has probability zero. On its complement the same candidate argument as in step 2.2 gives successful return.