Rational boxes admit dyadic enclosure boundaries and exact affine root charts

For addition and subtraction, the scalar order inequalities give the displayed endpoint bounds. For multiplication with one argument fixed, the product is affine in the other argument and lies between its two endpoint values; repeating this for the first argument bounds every product by the minimum and maximum of the four corners. On an interval not containing zero, the reciprocal function reverses order, so its values lie in $[1\mathrm{/}d,1\mathrm{/}c]$; multiplication then gives division bounds. Each endpoint is rational by [F1]. Induction over a finite expression applies these bounds to every actual predecessor value, so every exact expression value lies in the computed rational enclosure. A domain failure or unavailable operation ends this assertion.

An enclosed vector differs from its midpoint by coordinate errors of magnitude at most $r_i$, so [F5] bounds its Euclidean error by ${\sum }_i{r}_i$. If a matrix error $E$ has $\mathrm{\mid }{E}_{ij}\mathrm{\mid }\le s_{ij}$ and $\mathrm{\parallel }x{\mathrm{\parallel }}_2=1$, then $\mathrm{\mid }{x}_j\mathrm{\mid }\le 1$ and $\mathrm{\parallel }Ex{\mathrm{\parallel }}_2\le {\sum }_i\mathrm{\mid }(Ex{)}_i\mathrm{\mid }\le {\sum }_{i,j}{s}_{ij}$. Taking the supremum over unit vectors proves the matrix-error bound. The same calculation for the exact inverse matrix $V$ gives $\mathrm{\parallel }V{\mathrm{\parallel }}_{\mathrm{o}\mathrm{p}}\le {\sum }_{i,j}\mathrm{\mid }{V}_{ij}\mathrm{\mid }$; its two checked inverse identities identify it with ${\widehat{A}}^{-1}$. These estimates are conservative and finite, not relative-error assertions.

Each $d_j=b_j-a_j$ is positive. The inverse $T^{-1}(z{)}_j=(z_j-a_j)\mathrm{/}{d}_j$ is well-defined and sends $[a_j,b_j]$ bijectively onto $[0,1]$. Hence $T(B)=Z$ bijectively. For a subbox $A={\prod }_j[l_j,u_j]$, positivity gives $T(A)={\prod }_j[a_j+d_j{l}_j,a_j+d_j{u}_j]$; its endpoints are rational when those of $A$ are dyadic or rational. Affineness gives $T((l+u)\mathrm{/}2)=(T(l)+T(u))\mathrm{/}2$. Images commute with unions and preserve intersections under a bijection, so finite coverage and disjoint interiors of partitions transfer, including shared bisection faces.

If the rational result is $[l,u]$ and both directed endpoints are finite, [F2] and [F3] give $\mathrm{rd}(l)\le l\le u\le \mathrm{ru}(u)$. Thus its dyadic replacement contains the full rational enclosure and every exact value established in step 1.1. Apply this separately to each coordinate or matrix entry. An overflow sentinel is not a finite interval and cannot supply the finite-return assertion.

The affine maps $T$ and its displayed inverse are continuously differentiable with constant derivatives $D$ and $D^{-1}$. Thus $T^{-1}(V)$ is open, is convex because affine maps preserve segments, and contains $B$. By [F4], $D\widehat{F}(u)=DF(T(u))D$. A point residual enclosure therefore applies unchanged to $\widehat{F}(m)$. On $A$, every physical derivative lies entrywise in $J(T(A))$ and right multiplication by $D$ multiplies column $j$ by the positive scalar $d_j$; steps 1.1 and 2.1 give the stated finite dyadic enclosure. No transformed point is queried outside the original physical box.

The identity $\widehat{F}(u)=F(T(u))$ and the bijection in step 1.3 identify each zero in $A$ with exactly one zero in $T(A)$. Empty-root, at-least-one-root and at-most-one-root statements therefore transfer in both directions, and finite partition coverage transfers as well. Finally write $J=DF(T(u))$ and $A=CJD$. If $A$ and $C$ are nonsingular, then $D{A}^{-1}C$ is a two-sided inverse for $J$: $JD{A}^{-1}C=C^{-1}A{A}^{-1}C=I$ and $D{A}^{-1}CJ=D{A}^{-1}A{D}^{-1}=I$. This proves the last assertion using the explicit invertibility of $D$, without a norm comparison between physical and normalized coordinates.