Finite certified evaluation of the scaled complementary error function

Input an exact dyadic real $x$, positive rational absolute tolerance ${\epsilon }_a$, optional positive rational relative tolerance ${\epsilon }_r$, a fixed exponent range $(e_{\min },e_{\max })$, and finite positive integer caps $S_{\max },D_{\max },N_{\max },p_{\max },W$, with $p_{\max }\ge 2$. Here $S_{\max }$ bounds stages, $D_{\max }$ the continued-fraction depth, $N_{\max }$ the asymptotic truncation, $p_{\max }$ the dyadic precision, and $W$ the exact interval operations, terms, and subroutine calls performed by this procedure. Reject nonpositive tolerances, invalid caps, $e_{\min }>e_{\max }$, or $x\le 0$ with domain. At stage $q$, use $D=\min (q,D_{\max })$, $N=\min (q,N_{\max })$, precision $p=\max (2,\min (q,p_{\max }))$, and truncation index $q$ for elementary-range calls. Outputs and status meanings are those of Certified special-function enclosure result.

All rational and interval arithmetic uses Outward-rounded interval, rectangle and ball operations. Charge every exact arithmetic operation, range-evaluator node operation, term, rounding, and loop update to the shared counter $W$. Interrupt any nested elementary-range call with inconclusive before its next operation would exceed the remaining budget. Return inconclusive before any local operation would exceed $W$. A final endpoint overflow returns range. A non-finite required arithmetic operation or elementary-range subcall makes its candidate unavailable; if neither candidate can be formed, the current stage is inconclusive and later stages may still be tried.

For each stage $q=1,\dots ,S_{\max }$, compute $P_q$, a finite dyadic interval containing $\pi$, as follows. For $r\in \{1\mathrm{/}5,1\mathrm{/}239\}$, form $A_q(r)={\sum }_{j=0}^{q-1}(-1{)}^j{r}^{2j+1}\mathrm{/}(2j+1)$ and $E_q(r)=r^{2q+1}\mathrm{/}((2q+1)(1-r^2))$ exactly; the arctangent-tail lemma gives $\arctan r\in [A_q(r)-E_q(r),A_q(r)+E_q(r)]$. Combine these intervals by $\pi =16\arctan (1\mathrm{/}5)-4\arctan (1\mathrm{/}239)$ and round outward to the selected format at precision $p$. The Machin identity is supplied by Trigonometric identities, Machin's formula and reduced Taylor tails; the arctangent series and its geometric-tail argument are in Range-reduced exponential, logarithm and arctangent series have certified tails. If the interval conversion is non-finite, skip the stage. Call Certified range evaluation for elementary real and complex functions on the real one-node DAG $\sqrt{P_q}$, using exponent range $(e_{\min },e_{\max })$, precision $p$, and truncation $q$. If this call is not finite or its output $R_q$ does not have positive lower endpoint, skip this stage. Otherwise $R_q$ encloses $\sqrt{\pi }$ by Certified real elementary-function evaluations enclose their ranges.

Form the continued-fraction candidate as follows. Set $I_D=[0,(D+1)\mathrm{/}(2x)]$. For $k=D-1,\dots ,0$, set $I_k=[\frac{k+1}{2(x+\sup I_{k+1})},\frac{k+1}{2(x+\inf I_{k+1})}]$ by outward interval operations. Apply the decreasing map $r\mapsto 1\mathrm{/}(\sqrt{\pi }(x+r))$ to $I_0$, evaluating $\sqrt{\pi }$ with $R_q$, to obtain a candidate interval $C_q$. The finite-depth containment lemma Finite continued-fraction enclosure for erfcx makes $C_q$ a valid enclosure for every $D\ge 0$.

If $N\ge 1$, also form the asymptotic candidate. Evaluate $S_N(x)=\frac{1}{x\sqrt{\pi }}{\sum }_{k=0}^{N-1}(-1{)}^k\frac{(1\mathrm{/}2{)}_k}{x^{2k}},B_N(x)=\frac{1}{x\sqrt{\pi }}\frac{(2N)!}{4^{N}N!x^{2N}}$ with $R_q$ and exact factorial/rational interval arithmetic. Write the computed sum interval as $[s_{-},s_{+}]$ and take a nonnegative outward upper endpoint $b_N$ for the remainder bound $B_N$. Set $A_q=[s_{-},s_{+}+b_N]$ when $N$ is even and $A_q=[s_{-}-b_N,s_{+}]$ when $N$ is odd, rounding the final endpoints outward. The signed remainder lemma Signed finite remainder for the erfcx asymptotic expansion makes $A_q$ a valid enclosure.

If both candidates are finite, intersect them when the intersection is nonempty; if it is empty, discard the stage. If only one is finite, use that candidate. Round the selected final endpoints outward to precision $p$. Return success at the first stage whose radius is at most ${\epsilon }_a$. Set relative_certified to true exactly when relative tolerance was requested, the interval excludes zero, and the contract's relative-radius test passes; a failed relative test does not prevent absolute success. If no stage passes before the finite caps, return inconclusive.