Certified real elementary-function evaluations enclose their ranges

For an exponential input interval, the fixed scale gives the exact interval $U=2^{-s}X\subset (-1\mathrm{/}2,1\mathrm{/}2)$ before any storage rounding. The point bound [L3] with $\mathrm{\mid }u\mathrm{\mid }$ replaced by the interval's largest absolute endpoint gives a uniform tail enclosure. Exact rational interval evaluation of the polynomial and tail encloses every point; final outward conversion preserves that enclosure by [L2]. The tail radius increases with the largest absolute input, and each repeated interval square preserves inclusion by [L2]. To justify the scaling identity, put $d=2^s$. Repeated applications of [L6] to the absolutely convergent series for $\exp u$ show that the coefficient of $u^k$ in $(\exp u{)}^d$ is ${\sum }_{n_1+\cdots +n_d=k}\frac{1}{n_1!\cdots n_d!}=\frac{d^k}{k!},$ where the equality is the multinomial theorem. Thus $(\exp u{)}^d=\exp (du)$; set $u=x\mathrm{/}d$. Each interval squaring preserves the resulting enclosure by [L2].

The outward cell interval built from $P_N$ contains each exact canonical cell, since $\pi \in P_N$; thus its intersection hull $X_k$ contains every input point assigned to that cell, and $X_k-k{P}_N\mathrm{/}2$ contains the exact residual $r=x-k\pi \mathrm{/}2$. The algorithm certifies this residual inside the Taylor range. By [L4], exact sine and cosine values are the stated signed swaps of $\sin r$ and $\cos r$. The polynomial interval evaluation contains each truncated value by [L2], and adding the symmetric tail interval from [L4] contains the omitted remainder. Taking the hull over all intersected cells therefore contains the full range. If the input width is at least $2\sup (P_N)$, it is at least $2\pi$, so [L4] gives the safe range $[-1,1]$. The algorithm rounds the endpoints of this exact interval outward; if the result is finite, [L2] ensures that it contains $[-1,1]$. For nested inputs, each fixed canonical cell intersection enlarges and its fixed-term interval evaluation is isotone by [L2]; the hull is therefore nested on the reduced branch. Exact rational interval polynomial and tail operations are inclusion-isotone, and the final directed endpoint conversions are nondecreasing. Intersecting with $[-1,1]$ preserves containment and nesting. A narrower cell result has endpoints $\mathrm{rd}(a),\mathrm{ru}(b)$ with $a\ge -1$ and $b\le 1$; monotonicity gives $\mathrm{rd}(-1)\le \mathrm{rd}(a)$ and $\mathrm{ru}(b)\le \mathrm{ru}(1)$, so the outward-rounded wide-input result contains it.

On each positive logarithm bin, every $y$ maps to $v=(y-1)\mathrm{/}(y+1)\in [0,1\mathrm{/}3]$. The interval series and uniform tail from [L3] contain $\ln y$; [L3] also proves the exact logarithm scaling identity used by the algorithm. Each interval transform and sum preserves inclusion by [L2]. The fixed bin partition ensures that enlarging the input only enlarges the intersection with each bin, so its interval-series enclosure and the final hull also enlarge. The arctangent transformations follow from [L5]; on each fixed branch the rational interval maps and fixed series are isotone, and the tail radius is nondecreasing in the largest absolute transformed endpoint.

Tangent is defined only where cosine is nonzero. On a piece whose cosine enclosure excludes zero, division is sound by [L2] and contains every $\sin x\mathrm{/}\cos x$. If cosine may vanish, the algorithm returns a split or non-finite status, so no unsound finite value is reported. For a square-root node, the nonnegative-domain guard in [L1] permits the square-root enclosure in [L2], which contains every exact root and preserves inclusion of nonnegative intervals.

Evaluate the finite expression DAG in topological order. Every primitive node encloses its exact value by steps 1.1, 2.1, 1.2, and 2.2; induction over the finite node order then encloses every exact intermediate and every requested output range. Each primitive's canonical partition and fixed truncation are nested on common finite branches, so the same induction preserves inclusion for nested inputs evaluated with the same format and truncation index.