Symbolic finiteness conditions

The executable arithmetic refinement theorems are stated over real values, but IEEE overflow is observable only on the encoded result. This module connects those views: an exact dyadic whose magnitude is at most the largest finite value of the destination format cannot round to infinity.

The result is uniform in the exponent and fraction widths and is intended as the common foundation for operation-specific no-overflow theorems.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_roundDyadic_of_isIEEE_of_abs_toReal_le_posMaxFinite (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (d : Numerics.Dyadic) (hbound : |d.toReal| ≤ (posMaxFinite fmt).toReal) : (roundDyadic fmt d).isFinite = true

Nearest-even rounding cannot overflow when the exact dyadic magnitude is at most the largest finite value of the destination format.