Finite rational residual-tube certificate for an ODE trajectory

Fix a dimension $d\ge 1$, rational times $a<T$, a rational initial vector $y_0$, and an ODE field $f$ represented by a finite acyclic expression DAG with rational constants, time/state inputs, and only $+,-,\times ,÷$ nodes. Its domain consists of points where every division is defined. Write $D_{y}f$ for the matrix of partial derivatives with respect to the state coordinates. A finite rational residual-tube certificate consists of the following exact rational data:

1. A finite partition $a=t_0<t_1<\cdots <t_m=T$. On each panel $[t_j,t_{j+1}]$, a vector polynomial $U_j(t)$ with dyadic (hence rational) coefficients, whose neighboring endpoint values agree exactly. These stored coefficients define the actual reconstruction, including any endpoint correction or rounded stage value used by an implementation.
2. For each panel, a closed rational state box $X_j\subset {\mathbb{R}}^d$, rational bounds $L_j\ge 0$, ${\rho }_j\ge 0$, a rational $d_j\ge 0$, and a polynomial radius $R_j(t)$ with rational coefficients. The radius polynomials agree at neighboring endpoints. For a panel's finite rational subdivision, the intended inequalities are $R_j(t)>0$, $R_j^{\mathrm{\prime }}(t)-L_j{R}_j(t)-{\rho }_j>0$, and $U_j(t)+[-R_j(t),R_j(t){]}^d\subseteq X_j$.
3. A finite rational subdivision of every panel, with exact endpoint coverage, no gaps, and pairwise-disjoint interiors. It supplies cells on which each required range test below is performed. Rational cell endpoints and constants are enclosed by directed outward rounding to finite dyadic endpoints before interval evaluation; an unrepresentable or overflowing conversion cannot validate.
4. An initial check target $d_0\ge 0$ with ${\sum }_i(U_0(a{)}_i-(y_0{)}_i{)}^2\le d_0^2$ and $d_0<R_0(a)$.

The certificate is validated only if outward-rounded real-interval evaluation on every supplied cell proves all three radius/tube inequalities, the range inclusion in $X_j$, that every division denominator in the field and its state derivatives excludes zero on the time-state box $[t_j,t_{j+1}]\times X_j$, and ${\sum }_{i=1}^d\sup \mathrm{\mid }{U}_{j,i}^{\mathrm{\prime }}-f_i(t,U_j(t)){\mathrm{\mid }}^2\le {\rho }_j^2,{\sum }_{i,k=1}^d\sup \mathrm{\mid }{\mathrm{\partial }}_{y_k}{f}_i(t,y){\mathrm{\mid }}^2\le L_j^2$ there. Here each supremum is replaced in the check by the maximum absolute endpoint of a finite outward interval enclosure; the residual expression is evaluated at the actual polynomial $U_j$, so interpolation, stage, and storage errors already present in that reconstruction are included. Strict inequalities must have a certified positive interval lower endpoint; an inconclusive, nonfinite, unsupported, or failed test is not validation.

This format certifies only rational expression fields and polynomial reconstructions using the stated finite checks. It uses real intervals, not complex rectangles or balls, and does not claim an evaluator for transcendental functions or general library floating-point operations. The page proves the soundness of a validated certificate separately.

The finite DAG and real-interval conventions are those of Real intervals, complex rectangles and ball enclosures and Outward-rounded interval, rectangle and ball operations.