Outward interval and Lipschitz midpoint bounds are sound and consistent under refinement

By the endpoint-rounding rule and [F2], the dyadic input intervals used by the algorithm contain the original box $B$. The DAG enclosure statement [F1] therefore implies $a_{-}\le f(x)\le a_{+}$ for every $x\in B$. Thus $a_{-}$ and $a_{+}$ are valid lower and upper bounds on the entire box, not estimates from a sample point.

For a nested shrinking sequence $B_k\to \{x\}$ with precision $p_k\to \mathrm{\infty }$, outward-rounded input endpoints tend to their exact endpoint values by [F2], and each certified constant enclosure tends to its exact constant by the hypothesis. Induct in topological order through the finite DAG. At each addition, subtraction, or multiplication node the exact endpoint formulas are continuous in the input endpoints; at a division node the denominator is bounded away from zero, so the reciprocal endpoint formulas are continuous for all sufficiently large $k$. The directed-rounding error tends to zero by [F2]. Therefore each node enclosure converges to its exact node value at $x$, and in particular the root endpoints converge to $f(x)$.

For the Lipschitz procedure, every $x\in B$ satisfies ${\max }_j\mathrm{\mid }{x}_j-m_j\mathrm{\mid }\le r\le r^{+}$. By [F4], $f(x)\ge f(m)-Lr\ge q_{-}-L{r}^{+}\ge {\mathrm{\ell }}_B$, so ${\mathrm{\ell }}_B$ is valid on $B$.

Along a shrinking sequence, $m_k\to x$, $r_k^{+}\to 0$, and the singleton enclosure endpoints $q_{k,-},q_{k,+}$ tend to $f(x)$ by step 1.2. Hence $q_{k,-}-L{r}_k^{+}\to f(x)$, and the extra directed-rounding error also tends to zero by [F2]; therefore ${\mathrm{\ell }}_{B_k}\to f(x)$.