Soundness of every successful finite-budget Boys enclosure

If an endpoint is zero, the internal rational is exactly $F_m(0)$ and its outward-rounded interval contains that value. Each positive-endpoint seed branch uses its own explicitly bound order $m\in \{0,M\}$. If the small-$T$ branch is used, [F3] encloses its Taylor sum by its first omitted term. If the positive midpoint branch is used, each exponential node is enclosed by [F7] and the quadrature remainder in [F4] encloses the integral. Thus every successful direct seed interval contains its Boys value.

In the large branch, [F6] encloses $\mathrm{\Gamma }(m+\frac{1}{2})$ whenever its Gamma call succeeds. This target is real by the positive-real Euler integral and half-integer identity in [F8], so projection onto the real coordinate preserves its enclosure. The prescribed square roots and powers enclose the positive scaling factors by [F7], which also encloses $e^{-T}$, and [F5] bounds the omitted upper incomplete-gamma tail. Outward interval operations therefore produce a containing interval for $F_m(T)$.

For $T>0$, apply the exact recurrence identities [F8] to each previously enclosed order. The outward interval expression encloses the exact affine recurrence image, and [F9] bounds the stored radius, since the procedure forms each affine endpoint exactly rationally and adds both final outward-conversion errors. Induction over the finite order count proves every entry of either accepted candidate table contains its exact Boys value.

For $T_{-}\le T\le T_{+}$, [F8] makes $F_m$ decreasing, so its exact range lies between its endpoint values. The endpoint hull in [F1] therefore contains the entire range. The algorithm returns success only after the interval tests in [F2]; its other statuses make no success claim.

The algorithm visits only two endpoints and $M+1$ requested orders. Its refinement index is bounded by $W$; Taylor sums, midpoint panels and recurrence tables each have finite indices. More strongly, the shared counter is checked before every primitive operation and loop update, including all work inside Gamma and elementary subcalls. Every child receives the specified finite format/truncation inputs and the Gamma child additionally receives a finite work cap no larger than the remaining parent budget. Thus even a child whose complete construction would exceed that budget is interrupted with inconclusive; every branch returns a status after finitely many charged operations. No argument infers success from the size of a finite cap.