Directed addition soundness for conventional IEEE formats

Finite operands decode to exact dyadics. Their executable directed sum is the exact dyadic sum rounded outward, except that exact cancellation selects the IEEE rounding-mode-specific signed zero. Both signed zeros denote zero, so the same enclosure theorem covers cancellation and overflow for conventional IEEE descriptors.

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

Downward-rounded addition is a lower bound on exact real addition for finite operands.

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

Exact real addition is bounded above by upward-rounded addition for finite operands.