Certified rounding from rational enclosures

Monotonicity places the rounded real target between the rounded endpoints. If those endpoints agree, they also equal the target's rounded code. In particular, the exponential enclosure algorithm supplies an entirely internal analytic justification for an accepted result.

These are acceptance theorems, not a claim that any fixed Taylor degree resolves every input.

theorem FloatLib.Floats.Formats.Posit.Model.Enclosure.roundPositiveCode_eq_of_contains (format : Format) {interval : Numerics.RationalInterval} {x : ℝ} (hx : interval.Contains x) (hequal : roundPositiveCode format interval.lo = roundPositiveCode format interval.hi) : RealRounding.roundPositiveCode format x = roundPositiveCode format interval.lo

Equal endpoint codes determine the rounded code of every enclosed real value.

theorem FloatLib.Floats.Formats.Posit.Model.Enclosure.eq_roundPositive_of_roundPositive?_eq_some (format : Format) {interval : Numerics.RationalInterval} {x : ℝ} {result : Model format} (hx : interval.Contains x) (hresult : roundPositive? format interval = some result) : result = RealRounding.roundPositive format x

Every accepted enclosure result equals rounding the enclosed real target.

theorem FloatLib.Floats.Formats.Posit.Model.Enclosure.eq_roundPositive_exp_of_roundPositive?_eq_some (format : Format) (x : ℚ) (degree : ℕ) {result : Model format} (hresult : roundPositive? format (Numerics.Enclosure.exp x degree) = some result) : result = RealRounding.roundPositive format (Real.exp ↑x)

An accepted rational exponential enclosure is correctly rounded to the posit format.