Correctness of IEEE binary division

The exact scaled-rational rounding theorem gives the real-number correctness contract for the public Model.div operation. The refinement sits above the dyadic arithmetic and rational packing layers to keep those dependencies acyclic.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_div_of_abs_div_le_posMaxFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hy0 : y.isZero = false) (hbound : |x.toReal / y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.div y).isFinite = true

Finite division by a nonzero finite operand cannot overflow when the exact real quotient is within the destination's largest finite magnitude.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_div_eq_roundAt {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hy0 : y.isZero = false) (hfin : (x.div y).isFinite = true) : (x.div y).toReal = roundAt fmt (x.toReal / y.toReal)

Finite division by a nonzero finite operand is exact real division followed by one nearest-even format rounding.

The hypothesis hfin excludes overflow by asking that the executable quotient be finite; toReal_div_eq_roundAt_of_abs_div_le_posMaxFinite supplies it from a bound on the operands.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_div_eq_roundAt_of_abs_div_le_posMaxFinite {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) (hy0 : y.isZero = false) (hbound : |x.toReal / y.toReal| ≤ (posMaxFinite fmt).toReal) : (x.div y).toReal = roundAt fmt (x.toReal / y.toReal)

Finite division under a symbolic exact-quotient bound is exact real division followed by one nearest-even format rounding.