Outward-rounded operations are inclusion-isotone and enclose DAG evaluations

For real addition and subtraction, every exact pair value lies between the endpoint formulas. For multiplication, fixing one variable makes the product affine in the other, so a minimum or maximum over a rectangle is attained at a corner. Reciprocal is monotone on either interval avoiding zero, and square root is monotone on $[0,\mathrm{\infty })$. Thus the exact ranges lie in the displayed pre-rounding intervals. Each computed lower endpoint is no greater than the exact lower endpoint and each upper endpoint is no smaller than the exact upper endpoint by [L2]; square-root endpoint bounds follow from [L3]. For complex rectangles, component addition and multiplication preserve the exact component formulas. If a rectangle excludes zero, at least one coordinate interval omits zero, so its exact squared interval has positive lower endpoint. The reciprocal rule retains the exact rational denominator and component quotient endpoints until final outward conversion, so underflow cannot introduce a zero divisor. Those converted components and subsequent multiplication enclose the reciprocal and quotient.

For a ball $B(c,r)$, the coordinate projection intervals in [L1] contain each real and imaginary component. By [L5]–[L6], $\mathrm{\mid }i\mathrm{\Im }z\mathrm{\mid }=\mathrm{\mid }\mathrm{\Im }z\mathrm{\mid }$; the complex triangle inequality [L4] therefore gives $\mathrm{\mid }z\mathrm{\mid }=\mathrm{\mid }\mathrm{\Re }z+i\mathrm{\Im }z\mathrm{\mid }\le \mathrm{\mid }\mathrm{\Re }z\mathrm{\mid }+\mathrm{\mid }\mathrm{\Im }z\mathrm{\mid }\le M_B$. Also $\mathrm{\mid }z{\mathrm{\mid }}^2=(\mathrm{\Re }z{)}^2+(\mathrm{\Im }z{)}^2\ge (\mathrm{\Re }z{)}^2=\mathrm{\mid }\mathrm{\Re }z{\mathrm{\mid }}^2$ by [L7]. If $\mathrm{\mid }z\mathrm{\mid }<\mathrm{\mid }\mathrm{\Re }z\mathrm{\mid }$, nonnegativity would imply $\mathrm{\mid }z{\mathrm{\mid }}^2<\mathrm{\mid }\mathrm{\Re }z{\mathrm{\mid }}^2$, a contradiction. Hence $\mathrm{\mid }z\mathrm{\mid }\ge \mathrm{\mid }\mathrm{\Re }z\mathrm{\mid }$; the same argument gives $\mathrm{\mid }z\mathrm{\mid }\ge \mathrm{\mid }\mathrm{\Im }z\mathrm{\mid }$. Every point of $X_B$ and $Y_B$ has absolute value at least its corresponding $d$ value, so $\mathrm{\mid }z\mathrm{\mid }\ge m_B$. For $z\in B_1,w\in B_2$, [L4] gives $\mathrm{\mid }z\pm w\mathrm{\mid }\le M_{B_1}+M_{B_2}$ and $\mathrm{\mid }zw\mathrm{\mid }\le M_{B_1}{M}_{B_2}$. If $m_{B_2}>0$, then $\mathrm{\mid }w\mathrm{\mid }\ge m_{B_2}$ and $\mathrm{\mid }z\mathrm{/}w\mathrm{\mid }\le M_{B_1}\mathrm{/}{m}_{B_2}$. Upward radius rounding in [L1] preserves these bounds, proving soundness of all finite ball results.

Inclusion of balls implies inclusion of each coordinate projection interval. Therefore $M_B$ cannot decrease and $m_B$ cannot increase as an input ball enlarges. The ball addition, subtraction and multiplication radii in [L1] are consequently nondecreasing. If both divisor results are finite, the larger divisor ball has positive $m_B$ and the smaller one has at least as large an $m_B$; the quotient radius therefore cannot decrease when either ball is enlarged. For intervals and rectangles, the exact endpoint hulls and their downward/upward roundings preserve inclusion, so their finite extensions are isotone as well; for square root, [L3] gives monotonicity of the computed endpoint maps. If a domain restriction is lost, the operation returns its stated non-finite status.

In any nonempty finite acyclic graph, some node has no predecessor: otherwise, repeatedly following predecessors would revisit a node by finiteness and create a directed cycle. Remove such a node and repeat to construct a finite topological order. By [L1], input nodes contain their assigned values and constants have certified enclosures. Induct along this order: if each predecessor of an operation node contains its exact value, steps 1.1, 1.2, and 2.1 show that the operation enclosure contains the node's exact value. The induction covers every node, including the root, for every admissible assignment.