Outward rounded interval and ball arithmetic — Examples

For any $M>0$, choose a real $t>M+1$, set $x=1$ and $y=1\mathrm{/}t$. Then $x\in [1,2]$, $y\in (0,1]\subset Y$, and $x\mathrm{/}y=t>M$. Replacing $y$ by $-1\mathrm{/}t$ gives a quotient $-t<-M$. Thus the quotient set is unbounded in both directions.

A finite interval has finite lower and upper endpoints, so choose $M$ larger than their absolute values in step 1.1; the resulting exact quotient lies outside that interval, contradicting the required inclusion [L2]. The branch in [L1] avoids that contradiction by declining a finite hull.

Substituting $a=c=1$ and $b=d=2$ into [L1] gives $[1,2]-[1,2]=[1-2,2-1]=[-1,1]$.

For every real $x\in [1,2]$, the two DAG nodes have the same input value, so $f(x)=x-x=0$, and at $x=1$ this value is attained. Thus the exact range is $\{0\}$, which is contained in the computed interval by [L2].

Apply [L1] at $1\mathrm{/}5$ and $1\mathrm{/}239$ with $N=12$. The arctangent interval widths are at most twice the displayed tails; multiplying by $16$ and $4$ gives the two rational terms in the bound. By [L4], the integral gives $13\mathrm{/}20\le \arctan 1\le 9\mathrm{/}10<1$: its integrand is at least $4\mathrm{/}5$ on $[0,1\mathrm{/}2]$ and at least $1\mathrm{/}2$ on $[1\mathrm{/}2,1]$, while it is at most $1$ on the first half and at most $4\mathrm{/}5$ on the second. Thus $13\mathrm{/}5\le \pi \le 18\mathrm{/}5<4$. Before rounding, the Machin interval has width less than $2\cdot {10}^{-19}+{10}^{-30}$ by the tail estimates below, so its exact endpoints lie in $[5\mathrm{/}2,37\mathrm{/}10]$ using $13\mathrm{/}5\le \pi \le 18\mathrm{/}5$. The directed conversions stay in that interval and therefore each add at most $2^{-126}$ to the width. For the first tail, $32(1\mathrm{/}5{)}^{27}\mathrm{/}(27(1-1\mathrm{/}25))=800\mathrm{/}(648\cdot 5^{27})<2\cdot {10}^{-19}$, using $4000\cdot {10}^{18}<648\cdot 5^{27}$. The second tail is less than ${239}^{-27}<{16}^{-27}=2^{-108}<{10}^{-30}$. Therefore exact rational comparison gives $W:=\mathrm{width}(P)<{10}^{-18}$ and $\pi \in P$.

Each $x\in X$ has form $x=2p$ with $p\in P$, so $\mathrm{\mid }x-2\pi \mathrm{\mid }=2\mathrm{\mid }p-\pi \mathrm{\mid }\le 2W<2\cdot {10}^{-18}<\inf (P)\mathrm{/}4\le \pi \mathrm{/}4$; $\inf (P)\ge 5\mathrm{/}2$ by step 1.1. Thus $X$ lies inside the canonical $k=4$ cell. If $P=[p_{-},p_{+}]$, the actual cell formula $C_k=kP\mathrm{/}2+[-1\mathrm{/}4,1\mathrm{/}4]P$ gives $\sup C_3=7p_{+}\mathrm{/}4$ and $\inf C_5=5p_{-}\mathrm{/}2-p_{+}\mathrm{/}4=9p_{-}\mathrm{/}4-W\mathrm{/}4$. Since $p_{-}>2$ and $W<{10}^{-18}$, both $p_{-}>7W$ and $p_{-}>9W$ hold. Consequently $2p_{-}-\sup C_3=(p_{-}-7W)\mathrm{/}4>0$ and $\inf C_5-2p_{+}=(p_{-}-9W)\mathrm{/}4>0$. Thus $X=2P$ meets neither neighboring enclosure. All farther cells are separated as well by monotonicity of their endpoints in the integer cell index, while $C_4$ contains $X$. Hence the only included candidate is $k=4$. The interval residual computed by the evaluator is $R=X-4(P\mathrm{/}2)=[-2W,2W]$, which contains each exact reduced argument and lies inside the certified Taylor range.

Put $r_0=2W<2\cdot {10}^{-18}$. Bound each odd Taylor term on $R=[-r_0,r_0]$ by the symmetric exact rational interval $[-r_0^{2k+1}\mathrm{/}(2k+1)!,r_0^{2k+1}\mathrm{/}(2k+1)!]$, sum these intervals exactly, and add the geometric tail before outward conversion. The polynomial interval has total width at most $2{\sum }_{k=0}^{12}{r}_0^{2k+1}\mathrm{/}(2k+1)!\le 2r_0\mathrm{/}(1-r_0^2)<6\cdot {10}^{-18}$, since $r_0^2<1\mathrm{/}3$ gives $(1-r_0^2{)}^{-1}<3\mathrm{/}2$. Since $r_0<1\mathrm{/}2$, the displayed tail formula gives $T_s<2r_0^{27}\mathrm{/}27!<2r_0^2<{10}^{-18}$, so the symmetric tail width is below $2\cdot {10}^{-18}$. Only four directed endpoint conversions occur in this exact-rational path (two for $P$ and two for the sine enclosure); their total width increase is at most $4\cdot 2^{-126}$, below the conservative allowance $200\cdot 2^{-126}$. The total width is therefore below $1$. With $B=0$, the budgeted evaluator checks this finite enclosure and returns certified; [L3] confirms the exact range and width claim. No system sine routine is used.