Exact meaning of conversion range comparisons

The scalable rational/dyadic comparator first tests signs and leading exponents. Its answer is the ordinary rational order, including zero significands and negative values. This connects the executable conversion range indicator with the mathematical finite interval.

theorem FloatLib.Floats.Formats.P3109.compareDyadic_eq_compare (negative : Bool) (numerator denominator : ℕ) (value : Numerics.Dyadic) (hd : denominator ≠ 0) : Numerics.RationalBinary.compareDyadic? negative numerator denominator value = some (compare (RationalRounding.signed negative (↑numerator / ↑denominator)) value.toRat)

The scalable comparison with an arbitrary dyadic is its exact signed rational order.

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.exceedsFiniteRange_eq_decide (format : Formats.P3109.Format) (exact : ℚ) : exceedsFiniteRange format exact = decide (exact < format.minFinite.toRat ∨ format.maxFinite.toRat < exact)

The executable exact-range test is precisely strict exclusion from the finite interval.

theorem FloatLib.Floats.ExecFloat.P3109.Conversion.roundedExceedsFiniteRange_eq_decide (format : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (exact : ℚ) : roundedExceedsFiniteRange format mode exact = decide ((format.roundFiniteRatToPrecision mode exact).toRat < format.minFinite.toRat ∨ format.maxFinite.toRat < (format.roundFiniteRatToPrecision mode exact).toRat)

The pre-saturation overflow indicator is strict exclusion of the rounded rational value.