A validated rational residual-tube certificate encloses an exact ODE solution

A certified return means each interval operation was finite and every listed inclusion and strict inequality passed. By [F2], all exact rational-DAG values and their derivative-DAG values lie in the checked intervals. Thus on each panel $f$ is defined on $[t_j,t_{j+1}]\times X_j$. The residual interval tests bound each component's absolute value by its checked supremum, whose squared sum is at most ${\rho }_j^2$; [F12] and [F13] give $\mathrm{\parallel }{U}_j^{\mathrm{\prime }}-f(t,U_j){\mathrm{\parallel }}_2\le {\rho }_j$. Define $\mathrm{\parallel }A{\mathrm{\parallel }}_F:=({\sum }_{i,k}{A}_{ik}^2{)}^{1\mathrm{/}2}$; the Jacobian interval tests bound this sum by $L_j^2$, so [F13] gives $\mathrm{\parallel }{D}_{y}f{\mathrm{\parallel }}_F\le L_j$. The checker also proves $U_j(t)+[-R_j(t),R_j(t){]}^d\subseteq X_j$. Its exact initial squared comparison and [F12]–[F13] give $\mathrm{\parallel }{U}_0(a)-y_0{\mathrm{\parallel }}_2\le d_0<R_0(a)$. For each coordinate, $\mathrm{\mid }{U}_0(a{)}_i-(y_0{)}_i{\mathrm{\mid }}^2\le {\sum }_k\mathrm{\mid }{U}_0(a{)}_k-(y_0{)}_k{\mathrm{\mid }}^2=\mathrm{\parallel }{U}_0(a)-y_0{\mathrm{\parallel }}_2^2$, so [F13] places $y_0$ in $U_0(a)+[-R_0(a),R_0(a){]}^d\subseteq X_0$. Hence $(a,y_0)$ lies in the checked open ODE domain.

Fix $w=u-v$ and define $\varphi (s)=⟨w,f(t,v+sw)⟩$ for $0\le s\le 1$. The segment stays in $X_j$ by convexity. By [F3] and bilinearity in [F12], ${\varphi }^{\mathrm{\prime }}(s)=⟨w,D_{y}f(t,v+sw)w⟩$. The bound in step 1.1 and rowwise Cauchy–Schwarz give $\mathrm{\parallel }{D}_{y}fw{\mathrm{\parallel }}_2\le \mathrm{\parallel }{D}_{y}f{\mathrm{\parallel }}_F\mathrm{\parallel }w{\mathrm{\parallel }}_2\le L_j\mathrm{\parallel }w{\mathrm{\parallel }}_2$, and [F7] then gives $\mathrm{\mid }\varphi \mathrm{\prime }(s)\mathrm{\mid }\le L_j\mathrm{\parallel }w{\mathrm{\parallel }}_2^2$. [F6] on $[0,1]$ yields $\varphi (1)-\varphi (0)=⟨u-v,f(t,u)-f(t,v)⟩\le L_j\mathrm{\parallel }u-v{\mathrm{\parallel }}_2^2$. Thus the one-sided Lipschitz hypothesis in [F4] holds with $\mathrm{\ell }=L_j$ whenever the exact and reconstructed states lie in the certified box.

Picard–Lindelöf applies locally by [F3], and [F8] gives a unique maximal solution through $(a,y_0)$. On any interval where it exists and lies in the checked panel boxes, apply [F4] panel by panel. Write ${\delta }_j(t):=R_j^{\mathrm{\prime }}(t)-L_j{R}_j(t)-{\rho }_j$, which is strictly positive by the checker. Integrating the scalar identity $R_j^{\mathrm{\prime }}=L_j{R}_j+{\rho }_j+{\delta }_j$ with the same integrating factor shows that the radius dominates the error bound strictly: the initial gap is positive because $d_0<R_0(a)$, and each panel adds the positive integral of $e^{{\int }_s^t{L}_j}{\delta }_j(s)$, using positivity of the exponential [F11] and the fundamental theorem [F10]. For $e=y-U_j$, each coordinate satisfies $\mathrm{\mid }{e}_i{\mathrm{\mid }}^2\le {\sum }_k\mathrm{\mid }{e}_k{\mathrm{\mid }}^2=\mathrm{\parallel }e{\mathrm{\parallel }}_2^2$, so [F13] gives $\mathrm{\mid }{e}_i\mathrm{\mid }\le \mathrm{\parallel }e{\mathrm{\parallel }}_2$; hence $\mathrm{\parallel }e{\mathrm{\parallel }}_2<R_j(t)$ implies $y(t)\in U_j(t)+[-R_j(t),R_j(t){]}^d\subseteq X_j$. The comparison therefore applies up to any first exit and gives a strict radius bound there, ruling out that exit. At each panel endpoint the stored reconstructions and radii agree, so the strict inequality continues across the finite partition.

If the maximal solution ended before or at $T$, the no-first-exit conclusion in step 3.1 would keep its graph inside the finite union of the closed bounded boxes $[t_j,t_{j+1}]\times X_j$, which is compact by [F9] and lies in the rational field's open domain. All divisions stay away from zero there by step 1.1. This contradicts [F5], so the maximal solution reaches $T$. Applying the panelwise error estimate on the whole interval gives $\mathrm{\parallel }y(t)-U_j(t){\mathrm{\parallel }}_2<R_j(t)$ and hence $y(t)\in X_j$ for every panel time. Uniqueness follows from local Lipschitz continuity in [F3] and the local uniqueness clause of Picard–Lindelöf.