Outward-bounded floating determinant filter

Input: a finite exact dyadic square matrix $M$ of size $s\ge 2$, a selected floating-point system with known dyadic unit-roundoff bound $u$, and a finite range certificate listing each exact product or sum in the fixed left-to-right Leibniz schedule. Verify by exact dyadic comparison that every entry of $M$ is representable and each listed operation result is either zero or normal-range. The system must satisfy the standard relative model in The standard relative floating-point model and unit roundoff. Set $q=s+s!-2$ and ${\gamma }_q=qu\mathrm{/}(1-qu)$; if $qu\ge 1$, or if the certificate or model hypotheses are unavailable, return inconclusive without using a floating result.

1. Enumerate permutations in lexicographic tuple order. Form each signed product left-to-right, applying its sign by exact sign change. Initialize the sum with the first term; add each later term left-to-right using the selected floating-point system. Call the result $\widehat{D}$.
2. Enumerate permutations in the same lexicographic tuple order. For each permutation, start with $[1,1]$ and multiply the singleton intervals $[\mathrm{\mid }{M}_{i,\pi (i)}\mathrm{\mid },\mathrm{\mid }{M}_{i,\pi (i)}\mathrm{\mid }]$ from row $0$ through row $s-1$, from left to right, using the real absolute value Absolute value in an ordered field and the outward interval operations of Outward-rounded interval, rectangle and ball operations. Add these nonnegative terms from left to right, starting with the first term, to obtain the interval enclosure of the Leibniz absolute-term sum. Its expression DAG is finite; let $U$ be the upper endpoint of the resulting finite interval. If any operation is nonfinite, return inconclusive.
3. Compute $E=\mathrm{ru}({\gamma }_{q}U)$ by the directed rounding of Dyadic floating-point format and directed rounding. If this overflows, return inconclusive.
4. Compare exact dyadic rationals. Return positive if $\widehat{D}-E>0$; return negative if $\widehat{D}+E<0$; otherwise return inconclusive.

The computation of $U$ uses outward arithmetic, so the exact nonnegative sum $S$ in A left-to-right Leibniz determinant has an explicit forward error bound satisfies $S\le U$ whenever a finite $U$ is returned, by Outward-rounded operations are inclusion-isotone and enclose DAG evaluations.