Certified finite-bit Box–Muller has explicit BL and W1 error

The all-input-success hypothesis makes the computed output a deterministic function of the two finite bit blocks on the original probability space; no conditioning changes their law. Couple each ideal uniform input $U_j$ to its midpoint $U_{j,b}$ using the same bits. On the event $G=\{U_1\ge \delta +{\delta }_b\}$, both $U_1$ and $U_{1,b}$ are at least $\delta$. The mean-value theorem and logarithm derivative [F6] give $\mathrm{\mid }\log U_1-\log U_{1,b}\mathrm{\mid }\le {\delta }_b\mathrm{/}\delta$. For $x\ge y\ge 0$, [F7] and $(\sqrt{x}-\sqrt{y})(\sqrt{x}+\sqrt{y})=x-y$ give $(\sqrt{x}-\sqrt{y}{)}^2\le x-y$; interchanging $x,y$ proves $\mathrm{\mid }\sqrt{x}-\sqrt{y}\mathrm{\mid }\le \sqrt{\mathrm{\mid }x-y\mathrm{\mid }}$. Thus the radial change before evaluator error is at most $\sqrt{2{\delta }_b\mathrm{/}\delta }$. The angular unit vector changes by at most $2\pi \mathrm{\mid }{U}_2-U_{2,b}\mathrm{\mid }\le 2\pi {\delta }_b$, and the midpoint radius is at most $R_{\delta }$. Thus the exact transform difference on $G$ is at most $\sqrt{2{\delta }_b\mathrm{/}\delta }+2\pi R_{\delta }{\delta }_b$.

Put $r_b=\sqrt{-2\log U_{1,b}}$ and $t_b=(\cos (2\pi U_{2,b}),\sin (2\pi U_{2,b}))$. The certified log interval $[L_{-},L_{+}]$ contains $\log U_{1,b}$, so $q=-2L_{-}\ge 0$ and $\mathrm{\mid }q-r_b^2\mathrm{\mid }=2\mathrm{\mid }{L}_{-}-\log U_{1,b}\mathrm{\mid }\le 2{\eta }_{\mathrm{\ell }}$. The certified root interval contains $\sqrt{q}$ and has width at most ${\eta }_s$, hence $\mathrm{\mid }\widehat{r}-\sqrt{q}\mathrm{\mid }\le {\eta }_s$. The square-root inequality from step 1.1 yields $\mathrm{\mid }\widehat{r}-r_b\mathrm{\mid }\le {\eta }_s+\sqrt{2{\eta }_{\mathrm{\ell }}}={\eta }_r$. The phase certificate gives $\mathrm{\parallel }\widehat{t}-t_b{\mathrm{\parallel }}_2\le {\eta }_t$, so $\mathrm{\parallel }\widehat{t}{\mathrm{\parallel }}_2\le 1+{\eta }_t$. Therefore the evaluator perturbation satisfies $\mathrm{\parallel }\widehat{r}\widehat{t}-r_b{t}_b{\mathrm{\parallel }}_2\le \mathrm{\mid }\widehat{r}-r_b\mathrm{\mid }\mathrm{\parallel }\widehat{t}{\mathrm{\parallel }}_2+r_b\mathrm{\parallel }\widehat{t}-t_b{\mathrm{\parallel }}_2\le {\eta }_r(1+{\eta }_t)+R_{\delta }{\eta }_t$, using [F4] and $\mathrm{\parallel }{t}_b{\mathrm{\parallel }}_2=1$. Combining with step 1.1 gives $\mathrm{\parallel }Z-\widehat{Z}{\mathrm{\parallel }}_2\le e$ on $G$.

Since $U_1$ is uniform by [F1], $\mathbb{P}(G^c)=p$. For every bounded-Lipschitz test function the difference on $G$ is at most $e$, and on $G^c$ it is at most $2$. Taking expectations and then the supremum gives $d_{\mathrm{B}\mathrm{L}}(\mathcal{L}(Z),\mathcal{L}(\widehat{Z}))\le e+2p$.

By [F2], $\mathbb{E}\mathrm{\parallel }Z{\mathrm{\parallel }}_2^2=2$, so [F3] gives $\mathbb{E}[\mathrm{\parallel }Z{\mathrm{\parallel }}_2{\mathbf{1}}_{G^c}]\le \sqrt{2p}$. The smallest midpoint is $2^{-b-1}$, hence every exact midpoint radius is at most $R_b$; [F4] gives $\mathrm{\parallel }\widehat{Z}{\mathrm{\parallel }}_2\le (R_b+{\eta }_r)(1+{\eta }_t)$. Therefore the expected coupled error is at most $e+\sqrt{2p}+(R_b+{\eta }_r)(1+{\eta }_t)$, which bounds $W_1$.

The instructions take exactly $b$ bits from each of two subsequences and, on success, call the log evaluator, root evaluator, and phase evaluator once each; hence the stated bit count and three top-level calls. There are only $2^{2b}$ possible pairs of bit blocks, so $\widehat{Z}$ is supported on a finite set. The exact Gaussian law has a density and assigns that set probability zero; by [F5], the distance is $1$. The radius bound in step 3.2 proves bounded support.