Directed multiplication soundness for conventional IEEE formats

For finite operands, mulDown and mulUp round the same exact dyadic product in opposite directions. The extended-real statements remain valid when outward rounding overflows.

The bounds hold for every descriptor satisfying fmt.isIEEE = true, with no restriction to named widths. Both operands must be finite; the rounded product may be infinite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toEReal_mulDown_le {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.mulDown y).toEReal ≤ ↑(x.toReal * y.toReal)

Downward-rounded multiplication is a lower bound on the exact real product.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_toEReal_mulUp {fmt : FloatFormat} (x y : Model fmt) (hfmt : fmt.isIEEE = true) (hx : x.isFinite = true) (hy : y.isFinite = true) : ↑(x.toReal * y.toReal) ≤ (x.mulUp y).toEReal

The exact real product is bounded above by upward-rounded multiplication.