Directed division soundness for conventional IEEE formats #
For finite operands and a nonzero divisor, div x y (mode := .down) and div x y (mode := .up)
round the exact rational quotient in opposite directions. The extended-real statements hold even
when outward rounding overflows.
The bounds hold for every descriptor satisfying fmt.isIEEE = true, with no restriction to named
widths.
theorem
FloatLib.Floats.Formats.BinaryInterchange.Model.signedScaledRatToReal_of_toDyadic?_some
{fmt : FloatFormat}
{x y : Model fmt}
{dx dy : Numerics.Dyadic}
(hdx : x.toDyadic? = some dx)
(hdy : y.toDyadic? = some dy)
:
signedScaledRatToReal (dx.negative ^^ dy.negative) dx.significand dy.significand (dx.exponent - dy.exponent) = x.toReal / y.toReal
The exact scaled rational quotient of two finite values denotes their real quotient.