Finite checker for rational residual-tube certificates

Input a finite rational certificate of Finite rational residual-tube certificate for an ODE trajectory, an outward-rounded real interval format, and the matching operation evaluator of Outward-rounded interval, rectangle and ball operations. Return either certified or inconclusive by this finite procedure:

1. Parse and structurally check the rational field DAG, finite mesh, panel polynomials, state boxes, radius polynomials, rational bounds, and subdivisions. Reject malformed syntax, noncanonical/nonfinite numbers, gaps, nontrivial interior overlaps, endpoint mismatches, or a non-acyclic graph as inconclusive.
2. In topological order, construct the formal time/state derivative DAG for each field output by Symbolic derivative recursion for a rational expression DAG is correct. If any recursion node is unsupported, return inconclusive.
3. Convert each exact rational cell endpoint and constant to a directed outward dyadic interval. On each supplied time cell and panel box, evaluate the field, derivative DAG, reconstruction, its derivative, radius and strict-margin expressions using only outward-rounded real interval addition, subtraction, multiplication, division, and rational constants. If any operation returns split-domain, entire, domain-error, overflow, or inconclusive, return inconclusive.
4. Check exactly that the time cells cover each panel and that neighboring reconstruction/radius endpoints agree; verify the initial squared-error inequality separately. From interval endpoints check: each radius and each strict supersolution margin has strictly positive lower endpoint; the componentwise reconstruction-plus-radius boxes lie inside $X_j$; the residual component intervals satisfy the displayed squared-norm bound by ${\rho }_j^2$; all field and derivative denominator intervals exclude zero; and the squared Frobenius bound on the state Jacobian is at most $L_j^2$. Check the initial squared error bound and strict comparison $d_0<R_0(a)$ by exact rational arithmetic.
5. Return certified only when every check passes. Any failed inclusion or comparison returns inconclusive with the first failed check identifier. No automatic subdivision, transcendental evaluation, complex rectangle operation, or ball operation is performed.

The finite interval evaluator and its DAG interpretation are those of Outward-rounded interval, rectangle and ball operations and Outward-rounded operations are inclusion-isotone and enclose DAG evaluations. A separate theorem proves soundness of every certified result.