Soundness of binary enclosure acceptance

Finite rational rounding agrees with roundAt. Monotonicity extends agreement of rounded endpoints to every real target in the enclosure, including subnormal results and underflow to zero. The binary scale of roundScaled? multiplies every target by the same power of two.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Enclosure.toReal_roundEndpoint (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) (value : ℚ) (scale : ℤ) (hfinite : (roundEndpoint fmt value scale).isFinite = true) : (roundEndpoint fmt value scale).toReal = roundAt fmt (↑value * 2 ^ scale)

Finite endpoint rounding agrees with nearest-even rounding on the independent real grid.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Enclosure.accepted {fmt : FloatFormat} {interval : Numerics.RationalInterval} {scale : ℤ} {result : Model fmt} (hresult : roundScaled? fmt interval scale = some result) : fmt.isIEEE = true ∧ result.isFinite = true ∧ roundEndpoint fmt interval.lo scale = result ∧ roundEndpoint fmt interval.hi scale = result

Acceptance proves both the descriptor restriction and endpoint finiteness and agreement.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Enclosure.isFinite_of_roundScaled?_eq_some {fmt : FloatFormat} {interval : Numerics.RationalInterval} {scale : ℤ} {result : Model fmt} (hresult : roundScaled? fmt interval scale = some result) : result.isFinite = true

A scaled accepted encoding is finite, because overflow can never pass the endpoint check.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Enclosure.toReal_eq_roundAt_of_roundScaled?_eq_some {fmt : FloatFormat} {interval : Numerics.RationalInterval} {scale : ℤ} {target : ℝ} {result : Model fmt} (htarget : interval.Contains target) (hresult : roundScaled? fmt interval scale = some result) : result.toReal = roundAt fmt (target * 2 ^ scale)

Every scaled accepted result is the correctly rounded value of every real target in the enclosure times the binary scale.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Enclosure.isFinite_of_round?_eq_some {fmt : FloatFormat} {interval : Numerics.RationalInterval} {result : Model fmt} (hresult : round? fmt interval = some result) : result.isFinite = true

An accepted encoding is finite, because overflow can never pass the endpoint check.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.Enclosure.toReal_eq_roundAt_of_round?_eq_some {fmt : FloatFormat} {interval : Numerics.RationalInterval} {target : ℝ} {result : Model fmt} (htarget : interval.Contains target) (hresult : round? fmt interval = some result) : result.toReal = roundAt fmt target

Every accepted result is the correctly rounded value of every real target in the enclosure.