Range-limited finite-only interval enclosures

Finite-only formats saturate instead of producing infinity. Their outward interval operations are therefore sound only when the exact endpoint expressions remain inside the finite range. This module states those range premises explicitly.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.add_sound_of_encoding_finite {fmt : FloatFormat} (A B : Interval fmt) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (hloRange : |A.lo.toReal + B.lo.toReal| ≤ (posMaxFinite fmt).toReal) (hhiRange : |A.hi.toReal + B.hi.toReal| ≤ (posMaxFinite fmt).toReal) {x y : ℝ} (hx : A.RealMem x) (hy : B.RealMem y) : (A.add B).RealMem (x + y)

Finite-only interval addition encloses every selected sum when both exact endpoint sums fit in the format's symmetric finite range.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.sub_sound_of_encoding_finite {fmt : FloatFormat} (A B : Interval fmt) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (hloRange : |A.lo.toReal - B.hi.toReal| ≤ (posMaxFinite fmt).toReal) (hhiRange : |A.hi.toReal - B.lo.toReal| ≤ (posMaxFinite fmt).toReal) {x y : ℝ} (hx : A.RealMem x) (hy : B.RealMem y) : (A.sub B).RealMem (x - y)

Finite-only interval subtraction is sound when its two exact endpoint differences fit in range.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Interval.mul_sound_of_encoding_finite {fmt : FloatFormat} (A B : Interval fmt) (hfmt : fmt.encoding = FloatFormat.Encoding.finite) (h00 : |A.lo.toReal * B.lo.toReal| ≤ (posMaxFinite fmt).toReal) (h01 : |A.lo.toReal * B.hi.toReal| ≤ (posMaxFinite fmt).toReal) (h10 : |A.hi.toReal * B.lo.toReal| ≤ (posMaxFinite fmt).toReal) (h11 : |A.hi.toReal * B.hi.toReal| ≤ (posMaxFinite fmt).toReal) {x y : ℝ} (hx : A.RealMem x) (hy : B.RealMem y) : (A.mul B).RealMem (x * y)

Finite-only interval multiplication is sound when all four exact corner products fit in range.