Finite-budget certified evaluation of Boys function tables

Input a nonnegative integer $M$, a finite dyadic interval $\mathcal{T}=[T_{-},T_{+}]\subset [0,\mathrm{\infty })$, absolute tolerance ${\epsilon }_a>0$, optional relative tolerance ${\epsilon }_r>0$, a finite integer work cap $W$, a finite integer precision cap $P\ge 2$, and a dyadic format with precision $2\le p\le P$, exponent bounds and elementary truncation index $K\ge 1$. These are the backend parameters of Certified special-function enclosure result. The output is a table of real dyadic intervals $I_m$ for $0\le m\le M$, with status success, inconclusive, domain, or range.

All arithmetic uses Outward-rounded interval, rectangle and ball operations. Every real elementary call means a typed DAG call to Certified range evaluation for elementary real and complex functions at the supplied format and fixed $K$. Embed an exact rational argument by outward rounding; check the domain of the entire rounded argument before calling. Square roots use the outward square-root operation. No machine elementary value is an endpoint certificate. Maintain a shared work counter: charge each arithmetic operation, conversion, comparison, loop update, summand and primitive child operation before executing it. Interrupt a child when the remaining counter reaches zero. A cap exhaustion, unresolved enclosure test, intermediate overflow, or child non-success on otherwise valid data makes the affected seed or directional candidate unavailable; if no candidate succeeds, return inconclusive. Return range only when a certified bound proves that an exact requested table value lies outside the largest finite magnitude of the supplied format. Invalid original inputs give domain; a domain test obscured only by intermediate rounding gives inconclusive.

1. Validate the stated input conditions and supported format. Process the distinct endpoints in increasing order; process the distinct seed orders $m\in \{0,M\}$ in increasing order. At an endpoint $\tau =0$, form the exact rationals $1\mathrm{/}(2m+1)$ for every $0\le m\le M$. If any exact value exceeds the largest finite magnitude of the format, return range; otherwise round the rationals outward to the output format. Use this table without a recurrence. A rational is retained exactly internally, but a non-dyadic rational is not returned as a singleton dyadic interval.

2. For each positive endpoint $\tau$, perform refinements $k=0,1,\dots ,W-1$, subject to the shared work counter. At refinement $k$, try the two seed orders separately using their own $m$ and $s=m+\frac{1}{2}$:

   • If $0<\tau \le 1$, evaluate the Taylor polynomial through $N=k$ from Boys integral, power series, recurrence, and incomplete-gamma representation, then enlarge by the outward upper bound for ${\tau }^{N+1}\mathrm{/}((N+1)!(2m+2N+3))$ from A monotone-range Taylor remainder for small Boys arguments. The condition $N+2\ge \tau$ holds throughout this branch.
   • If $1<\tau \le 2m+1$, use $N=2^k$ panels of A positive midpoint enclosure for Boys functions on bounded arguments, in increasing node order $j=1,\dots ,N$, and enlarge the positive midpoint sum by $(m+\tau )\mathrm{/}(2N)$. Its dyadic nodes are formed exactly before storage; evaluate their exponentials by the finite real elementary call.
   • If $\tau >2m+1$, request the Gamma target from Finite certified evaluation of Gamma and a continued log-Gamma branch on the exact rectangle $[s,s]+i[0,0]$, with positive exact rational child absolute tolerance $q\mathrm{/}{2}^{k+2}$, where $q$ is constructed by starting at $q=1$ and repeatedly replacing $q$ by $q\mathrm{/}2$ until $q\le {\epsilon }_a$. Charge every comparison and halving to the shared counter; exhaustion returns inconclusive. Thus $0<q\le {\epsilon }_a$ without restricting the parent tolerance to rational values. Supply no relative request, base format precision $p_0=p$, the same exponent bounds and fixed elementary truncation $K$, child precision cap $P$, and child work cap $w=\lfloor R\mathrm{/}4\rfloor$, where $R$ is the remaining parent work at call entry. If $w<1$, stop inconclusive. Debit its actual work, including unsuccessful work, to the parent counter. A successful child rectangle has real projection containing the real number $\mathrm{\Gamma }(s)$: its reality follows from the positive-real Euler integral, also evaluated by the half-integer identity in Boys integral, power series, recurrence, and incomplete-gamma representation. Use this projection as the real Gamma enclosure. Evaluate $e^{-\tau }$ by the real elementary call, and use A scaled incomplete-gamma tail bound for large Boys arguments to form the enclosing interval for $F_m(\tau )$. Compute ${\tau }^s={\tau }^m\sqrt{\tau }$ and ${\tau }^{s-1}={\tau }^s\mathrm{/}\tau$ by outward operations; the exact denominator $1-\max (s-1,0)\mathrm{/}\tau$ is positive. Replace a negative lower endpoint by zero, retaining the upper endpoint. A child range, a child domain on this valid positive argument, or a child inconclusive invalidates that seed attempt and permits the next bounded refinement; no child status is propagated as a range claim for the Boys output.

   A finite seed interval is available to its direction only when its radius is at most ${\epsilon }_a$. A failed attempt does not invalidate a successfully enclosed seed for the other direction. Every panel and child loop is subject to the counter, even when its formal index bound is very large.

3. At each refinement obtain one finite real interval $J$ for $e^{-\tau }$. From an available order-zero seed form the upward candidate for orders $0,\dots ,M$; from an available order-$M$ seed form the downward candidate for orders $M,\dots ,0$. Use the exact affine recurrence maps in Upward and downward Boys recurrence error amplification bounds: compute each affine image's endpoints by exact rational endpoint arithmetic, then convert those two endpoints outward once. If either conversion overflows, discard that directional candidate at this refinement. Otherwise record the two conversion errors and propagate the lemma's radius bounds, including half their sum at each step. This prescription avoids omitting rounding at intermediate nodes. A table is admissible only if every entry satisfies the propagated bound and the requested absolute and, if requested, zero-excluding relative-radius test. Keep the admissible candidate with smaller maximum radius, ties upward. If neither direction is admissible, continue to the next refinement. Once an endpoint table is chosen, proceed to the next endpoint. No upward division is attempted at zero.

4. With both endpoint tables, form $I_m=\mathrm{hull}(I_m(T_{+}),I_m(T_{-}))$ for every requested order, using endpoint minima and maxima. By $F_m^{\mathrm{\prime }}(T)=-F_{m+1}(T)<0$ from Boys integral, power series, recurrence, and incomplete-gamma representation, this encloses the full range over $\mathcal{T}$. Return success only after every output radius is at most ${\epsilon }_a$ and, when relative tolerance is requested, the interval excludes zero and satisfies the relative-radius test in Certified special-function enclosure result. Otherwise return inconclusive. Exhausting the finite refinement list or shared work counter also returns inconclusive. At a positive endpoint, return range only if a certified lower bound for some requested exact Boys value exceeds the largest finite magnitude of the format; a merely overflowing enclosure endpoint gives inconclusive. No branch promises success for every valid box or finite cap.