Dyadic orientation and lifted sphere determinants

Use Dyadic floating-point format and directed rounding: each finite binary coordinate is interpreted as its exact dyadic rational $m{2}^e$. Write $\mathbb{D}=\{m{2}^e:m,e\in \mathbb{Z}\}$. All real signs and squared-distance comparisons use the order of Dedekind-complete ordered real field. For a positive integer $s\ge 1$ and a square matrix $M=(M_{ij}{)}_{0\le i,j<s}$ over $\mathbb{D}$, define

$$\det M=\sum _{\pi \in S_s}\mathrm{sgn}(\pi )\prod _{i=0}^{s-1}{M}_{i,\pi (i)},$$

where $S_s$ is the set of permutations of $\{0,\dots ,s-1\}$ and $\mathrm{sgn}(\pi )=(-1{)}^{\mathrm{inv}(\pi )}$ with $\mathrm{inv}(\pi )=\mathrm{\#}\{(i,j):i<j,\pi (i)>\pi (j)\}$.

For $d\in \{2,3\}$ and ordered points $p_0,\dots ,p_d\in {\mathbb{D}}^d$, let $H_d$ have row $i$ equal to $(p_i,1)$ and put $O_d=\det H_d$. The orientation predicate returns $\mathrm{sgn}(O_d)\in \{-1,0,+1\}$, where $\mathrm{sgn}(x)=+1$ for $x>0$, $0$ for $x=0$, and $-1$ for $x<0$. For ordered points $p_0,\dots ,p_{d+1}$, let $K_d$ have row $i$ equal to $(p_i,{\sum }_{j=1}^d{p}_{i,j}^2,1)$ and put $L_d=\det K_d$. The raw incircle predicate ($d=2$) or insphere predicate ($d=3$) returns $\mathrm{sgn}(L_d)$; its zero is an exact determinant zero. The row order is the point order displayed, and the column order is the coordinate columns, then squared norm, then $1$. If $O_d\mathrm{\ne }0$, define the orientation-normalized side sign algebraically to be $\mathrm{sgn}(O_d{L}_d)$. Whenever a sphere through $p_0,\dots ,p_d$ is specified, positive means inside it, zero means on it, and negative means outside. If $O_d=0$, the base simplex is degenerate and only the raw lifted determinant sign is specified.

An uncertain coordinate input is a real interval with finite dyadic endpoints, as defined in Real intervals, complex rectangles and ball enclosures. Its values remain uncertain throughout a certified computation; a midpoint is not substituted. For real $c\in {\mathbb{R}}^d$ and $r\ge 0$, write $S(c,r)=\{x\in {\mathbb{R}}^d:{\sum }_j(x_j-c_j{)}^2=r^2\}$; inside, on, and outside mean that this squared distance is less than, equal to, or greater than $r^2$.