Nearest-even lies between directed roundings (op-level corollaries) #
NN.Floats.IEEEExec.Rounding.RoundDyadicToIEEE32Bounds proves the core theorem:
$$ \operatorname{roundDyadicDown}(d) \le \operatorname{roundDyadicToIEEE32}(d) \le \operatorname{roundDyadicUp}(d) $$
in EReal.
This file packages small op-level corollaries for IEEE32Exec.add / mul / sub on the
finite path:
$$ \operatorname{addDown}(x,y) \le \operatorname{add}(x,y) \le \operatorname{addUp}(x,y), $$
and similarly for multiplication and subtraction.
These are useful for “checked boundary => enclosure” statements in downstream code (e.g. RL shadow interval diagnostics).
Small helpers #
Addition sandwich #
On the finite path, add/addDown/addUp all reduce to rounding the same exact dyadic sum with
different rounding modes.
Multiplication sandwich #
On finite inputs, mul/mulDown/mulUp reduce to rounding the same exact dyadic product with
different rounding modes.
Subtraction sandwich #
This is a direct corollary of the addition sandwich, since:
$\operatorname{sub}(x,y)=\operatorname{add}(x,\operatorname{neg}(y))$, and similarly for directed endpoints.