Directed division soundness for conventional IEEE formats #
For finite operands and a nonzero divisor, divDown and divUp round the exact rational quotient
in opposite directions. The extended-real statements remain valid when outward rounding
overflows.
The bounds hold for every descriptor satisfying fmt.isIEEE = true, with no restriction to named
widths. The operands must be finite and the divisor nonzero; the result may be infinite.
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.