Finite-budget multidimensional Krawczyk root certification

Input $F:U\to {\mathbb{R}}^n$ of class $C^1$ on an open convex $U$, a nonempty initial real box $X_0\subset U$, interval evaluators whose returned $F(x_0)$ and $J(Y)$ enclose the exact values at each processed box $Y$, a dyadic point matrix $C$, a rational matrix $W$, an exactly represented rational minimum side width $\eta >0$, and a nonnegative integer box budget $B\ge 0$. Check the inverse witness exactly by computing $WC$ and testing $WC=I$. If this test fails, return "inconclusive: preconditioner not certified nonsingular". For square matrices, a left inverse implies nonsingularity by rank-nullity (Rank-nullity: ${\dim }_{F}V=\mathrm{nullity}T+\mathrm{rank}T$).

Initialize a queue with $X_0$. Process at most $B$ boxes. For each box $Y$, take its coordinatewise midpoint $x_0$, evaluate a finite interval vector $F_0$ enclosing $F(x_0)$ and a finite interval Jacobian enclosure $J(Y)$, and compute

$$K(Y)=x_0-C{F}_0+(I-CJ(Y))(Y-x_0)$$

by outward real interval operations. If an evaluation or operation is non-finite, record that box as "unresolved" and continue with the remaining queue. If $K(Y)\cap Y=\mathrm{\varnothing }$, record "root-free". If $K(Y)\subset \mathrm{int}Y$, compute $E=I-CJ(Y)$ and

$$\bar{q}=\underset{i}{\max }\sum _j\max (\mathrm{\mid }\inf E_{ij}\mathrm{\mid },\mathrm{\mid }\sup E_{ij}\mathrm{\mid })\mathrm{.}$$

Record "unique-root" if $\bar{q}<1$, and "existence-only" otherwise. In every other case, bisect a longest side at its midpoint and append the two closed halves if the maximum side width exceeds $\eta$; ties use the lowest coordinate index. If no side exceeds $\eta$, record "unresolved". When the budget is exhausted, record every remaining queued box as "unresolved". The overall status is "complete" only if every output box is root-free or unique-root; existence-only and unresolved outputs do not establish an all-roots result.