Executable packing semantics

For a descriptor with fmt.isIEEE = true and a nonzero denominator, a finite result produced by roundRatScaled denotes roundAt applied to the corresponding real value.

The positive proof covers underflow, subnormal and normal results, including a carry into the next exponent. Finiteness excludes the overflow branches. The signed theorem restores the sign through the symmetry proved in RoundedReal.

Executable packing semantics

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundRatScaled_false_eq_roundAt (fmt : FloatFormat) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hfinite : (roundRatScaled fmt false numerator denominator exponent).isFinite = true) : (roundRatScaled fmt false numerator denominator exponent).toReal = roundAt fmt (signedScaledRatToReal false numerator denominator exponent)

Positive scaled-rational rounding denotes the independent nearest-even rounded-real value whenever the executable result is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundRatScaled_eq_roundAt (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) (hfinite : (roundRatScaled fmt sign numerator denominator exponent).isFinite = true) : (roundRatScaled fmt sign numerator denominator exponent).toReal = roundAt fmt (signedScaledRatToReal sign numerator denominator exponent)

Finite scaled rational rounding is exact signed rational evaluation followed by one nearest-even rounding in the destination format.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundRatScaled_eq_roundAt_of_isFinite (fmt : FloatFormat) (sign : Bool) (numerator denominator : ℕ) (exponent : ℤ) (hfmt : fmt.isIEEE = true) (hdenominator : denominator ≠ 0) (hfinite : (roundRatScaled fmt sign numerator denominator exponent).isFinite = true) : (roundRatScaled fmt sign numerator denominator exponent).toReal = roundAt fmt (signedScaledRatToReal sign numerator denominator exponent)

Finite scaled-rational rounding agrees with nearest-even real rounding, including a zero numerator. A nonzero denominator is still required, because zero denominators produce an invalid result.