Interval Krawczyk linear system certifier with explicit statuses

Input $n\ge 1$, a nonempty family of square matrices $\mathcal{A}$ and right-hand sides $\mathcal{b}$ enclosed by finite complex rectangles, a closed complex rectangle box $X\subset {\mathbb{C}}^n$, a point $x_0\in X$, and dyadic point matrices $R,S\in {\mathbb{C}}^{n\times n}$ with exact identities $RS=SR=I$. The witness $S$ establishes that $R$ is nonsingular. No independence assumption on the actual family is required beyond its inclusion in the input boxes.

1. Outward-evaluate, over the full family boxes and $x\in X$, the Krawczyk expression

$$K=x_0-R(A{x}_0-b)+(I-RA)(X-x_0)\mathrm{.}$$

If any interval operation is not finite and defined, return inconclusive.

2. Compare the resulting enclosing rectangle box with $X$ by exact endpoint comparisons. If it is not contained in $X$, return inconclusive. Otherwise outward-bound the maximum row sum of $\mathrm{\mid }I-RA\mathrm{\mid }$ uniformly over the family by a number $q$. If this norm bound cannot be enclosed finitely, return existence-certified with uniqueness-inconclusive and no defect bound. If it is finite, return existence-certified; attach unique-certified for each fixed pair if the outward comparison certifies $q<1$, and otherwise attach uniqueness-inconclusive.

The enclosure in step 1 may be wider than the exact set of Krawczyk values; only successful inclusion produces a claim. A failed inclusion or a failed norm bound does not imply singularity.