Finite-bit Box–Muller with certified elementary-function evaluators

Input an integer bit budget $b\ge 1$, two disjoint ideal fair-bit subsequences as in Disjoint streams of independent fair bits produce independent uniform variables, and a fixed deterministic configuration consisting of finite dyadic format parameters, positive integer series truncation indices $N\ge 1$ and nonnegative integer total split budgets $B\ge 0$ for the log/root interval evaluators, positive dyadic log/root width targets, and phase parameters with exact rational $0<\tau \le 1\mathrm{/}4$, integer exponent limits $e_{\min }\le e_{\max }$, integer precisions $2\le p_0\le p_{\max }$, and a positive integer elementary-series cap $J\ge 1$. Every call uses these fixed parameters; a failed call returns inconclusive with its supplier status. No success at a requested width is promised for arbitrary fixed budgets. The midpoint convention is Midpoint bit discretization has bounded coupling and CDF error, and the exact reference transform is Box–Muller has a product Gaussian density and Rayleigh second moment.

1. Take the first $b$ bits from each subsequence and form the exact dyadics $u_j=(K_j+1\mathrm{/}2)2^{-b}$. Enclose $u_1$ by directed dyadic endpoints in the selected format. If this is non-finite or its lower endpoint is not positive, return inconclusive; underflow may not turn a log argument into an accepted interval containing zero.

2. Apply Finite-budget validated range evaluation to the logarithm DAG on that interval with the configured finite parameters and log width target. On certified(L,X), write $L=[L_{-},L_{+}]$ and set $\widehat{\mathrm{\ell }}=L_{-}$, ${\eta }_{\mathrm{\ell }}=L_{+}-L_{-}$. The natural logarithm equals the integral logarithm by The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, so $L_{-}\le \log u_1<0$. Compute the exact dyadic $q=-2\widehat{\mathrm{\ell }}\ge 0$.

3. Enclose $q$ by directed endpoints in the configured format; reject non-finite endpoints or a negative lower endpoint. Apply the same budgeted procedure to its square-root DAG with the root width target. On a certified interval $S=[S_{-},S_{+}]$, set $\widehat{r}=S_{-}$ and ${\eta }_s=S_{+}-S_{-}$. The range guarantee of Budgeted range evaluation terminates and certifies only sound enclosures gives $\mathrm{\mid }\widehat{\mathrm{\ell }}-\log u_1\mathrm{\mid }\le {\eta }_{\mathrm{\ell }}$ and $\mathrm{\mid }\widehat{r}-\sqrt{q}\mathrm{\mid }\le {\eta }_s$. Width differences and the products in these instructions are exact dyadic arithmetic.

4. Call Certified dyadic enclosures for unit-circle phases on the exact rational $q_{\mathrm{p}\mathrm{h}\mathrm{a}\mathrm{s}\mathrm{e}}=2u_2$ and configured phase parameters. On its certified return $(\widehat{w},ϵ)$, set $\widehat{t}=(\mathrm{\Re }\widehat{w},\mathrm{\Im }\widehat{w})$ and ${\eta }_t=ϵ$. By Certified phase output encloses the exact unit-circle value, $\mathrm{\parallel }\widehat{t}-(\cos (2\pi u_2),\sin (2\pi u_2)){\mathrm{\parallel }}_2\le {\eta }_t$, including pi, angle, truncation and directed-endpoint errors. This is the existing phase routine, with its existing canonical-pi bridge.

5. Return the exact dyadic vector $\widehat{Z}=\widehat{r}\widehat{t}$ and the dyadic certificates ${\eta }_{\mathrm{\ell }},{\eta }_s,{\eta }_t$. If any preceding supplier call has a non-finite status, propagate it as inconclusive. Final vector multiplication is exact dyadic multiplication; rounding it further requires a separate added error certificate.

The output is the dyadic vector together with the reported evaluator certificates. Its arithmetic suppliers provide neither an IID source nor exact normal output.