Multiplication and division through Lean's floating-point model #
Lean's roundWithAccuracy requires an exponent that needs no left shift. That holds exactly when
the exponent is at or below the format's minimum exponent or the mantissa has at least as many
bits as the precision. Finite nonzero values unpacked from format words satisfy it, their products
keep it, and divCore satisfies it for all nonzero mantissas. When the provisional quotient is
zero, the sign, the selected exponent, and the remainder accuracy still determine the rounding.
toReal_ofModel_mul_toModel_eq_roundAt and toReal_ofModel_div_toModel_eq_roundAt therefore
need only a conventional IEEE descriptor and a finite result, plus a finite divisor for division.
Arbitrary unpacked operands need not satisfy the precondition, so
toReal_ofModel_mul_finite_eq_roundAt keeps its exponent hypothesis. These bridges are checked
against the logical floating-point model shipped with Lean.
Lean's roundWithAccuracy precondition holds exactly when the exponent is at or below the
format's minimum exponent or the mantissa has at least as many bits as the precision.
If two nonzero mantissas and their exponents satisfy Lean's roundWithAccuracy precondition, so
do the product of the mantissas and the sum of the exponents.
A finite nonzero value unpacked from a format word satisfies Lean's roundWithAccuracy
precondition: a subnormal has the minimum exponent and a normal has its leading bit set.
For nonzero mantissas, the provisional quotient and exponent returned by Lean's divCore satisfy
the roundWithAccuracy precondition. Above the minimum exponent, the numerator is shifted far
enough for the provisional quotient to have at least as many bits as the precision, so a zero
provisional quotient occurs only at or below the minimum exponent.
For a conventional IEEE descriptor and an accuracy that represents value at a zero mantissa,
Lean's signed roundWithAccuracy result has the same real value as independent nearest-even
rounding of the represented signed real. This is the case excluded by the nonzero-mantissa premise
of toReal_ofModel_roundWithAccuracy_eq_roundAt, under the same exponent premise. The result is
a signed zero or a signed least subnormal, so no finiteness premise is needed.
For a conventional IEEE descriptor, finite nonzero operands, and a finite result, Lean core's
unpacked division has the same independent nearest-even real semantics as Model.div.
This is toReal_ofModel_div_finite_eq_roundAt without its divCore premises. A zero provisional
quotient is rounded from its sign, selected exponent, and remainder accuracy by
toReal_ofModel_roundWithAccuracy_zero_eq_roundAt.
For a conventional IEEE descriptor, Lean core's finiteness test on the unpacked value agrees with
isFinite on the format word.
The word packed from Lean's NaN is not finite under a conventional IEEE descriptor.
For a conventional IEEE descriptor and a finite result, Lean core's unpacked multiplication of the
values unpacked from two format words has the same independent nearest-even real semantics as
Model.mul.
The finite result already excludes NaN and infinite factors; signed zeros are allowed. Unlike
toReal_ofModel_mul_finite_eq_roundAt, there is no exponent premise: values unpacked from format
words satisfy the roundWithAccuracy precondition, while arbitrary unpacked operands need not.
For a conventional IEEE descriptor, a finite divisor, and a finite result, Lean core's unpacked
division of the values unpacked from two format words has the same independent nearest-even real
semantics as Model.div.
The finite result already excludes a NaN or infinite dividend and a zero divisor. It does not
exclude an infinite divisor: a finite dividend over an infinite divisor is a signed zero. Unlike
toReal_ofModel_div_finite_eq_roundAt, there is no divCore premise: a quotient below the least
positive subnormal in magnitude rounds to a signed zero or a signed least subnormal.