Binary models as numerical systems

The NumericalSystem interface gives Model fmt a representation-independent semantic view. Its ordinary semantic domain is ℝ; supported infinities retain their signs, and NaNs retain the stored fraction as a payload.

Model.toDyadic? supplies the executable exact dyadic decoder. This real-valued view lets generic refinement results compose with other numerical families.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.toNumericalValue {fmt : FloatFormat} (x : Model fmt) : Numerics.NumericalValue ℝ

Complete real-valued interpretation of an executable float.

@[reducible, inline]

noncomputable abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.numericalSystem (fmt : FloatFormat) : Numerics.NumericalSystem

Real-valued numerical-system semantics of a binary format.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.Represents {fmt : FloatFormat} (x : Model fmt) (r : ℝ) : Prop

Proof-facing real interpretation of an executable float.

This is a relation on the existing Model fmt carrier, not a second floating-point type. Represents x r says that the exact bits stored by x have the ordinary finite meaning r.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.numericalSystem_represents_iff {fmt : FloatFormat} (x : Model fmt) (r : ℝ) : (numericalSystem fmt).Represents x r ↔ x.Represents r

The generic numerical-system relation is the direct Model representation relation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toNumericalValue_of_isFinite {fmt : FloatFormat} (x : Model fmt) (hx : x.isFinite = true) : x.toNumericalValue = Numerics.NumericalValue.finite x.toReal

Every finite executable float has its exact real interpretation as its total value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.numericalSystem_denote_of_isFinite {fmt : FloatFormat} (x : Model fmt) (hx : x.isFinite = true) : (numericalSystem fmt).denote x = Numerics.NumericalValue.finite x.toReal

Every finite executable float denotes its real interpretation in the general interface.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.numericalSystem_represents_of_isFinite {fmt : FloatFormat} (x : Model fmt) (hx : x.isFinite = true) : (numericalSystem fmt).Represents x x.toReal

The general interface represents exactly the real value used by finite arithmetic theorems.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.represents_iff {fmt : FloatFormat} (x : Model fmt) (r : ℝ) : x.Represents r ↔ x.isFinite = true ∧ x.toReal = r

An executable float represents a real exactly when it is finite and its exact decoding is that real. This is the main bridge from the single executable carrier to proof-oriented real reasoning.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.represents_toReal_iff {fmt : FloatFormat} (x : Model fmt) : x.Represents x.toReal ↔ x.isFinite = true

The real decoding of x is represented exactly when x is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_of_represents {fmt : FloatFormat} {x : Model fmt} {r : ℝ} (hx : x.Represents r) : x.isFinite = true

A represented executable float is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_eq_of_represents {fmt : FloatFormat} {x : Model fmt} {r : ℝ} (hx : x.Represents r) : x.toReal = r

The exact real decoding of a represented executable float is its represented value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.represents_unique {fmt : FloatFormat} {x : Model fmt} {r s : ℝ} (hr : x.Represents r) (hs : x.Represents s) : r = s

The finite real value represented by an executable bit pattern is unique.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.neg_refines (fmt : FloatFormat) : Numerics.Operation.Finite1 (numericalSystem fmt) (numericalSystem fmt) neg fun (x : ℝ) => -x

Executable negation represents the exact negative of every represented finite real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.add_refines (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : Numerics.Operation.Finite2If (numericalSystem fmt) (numericalSystem fmt) (numericalSystem fmt) add (fun (x y : ℝ) => roundAt fmt (x + y)) fun (x x_1 result : (numericalSystem fmt).Code) => isFinite result = true

Executable addition refines one nearest-even rounding for a conventional IEEE format, provided the result is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.sub_refines (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : Numerics.Operation.Finite2If (numericalSystem fmt) (numericalSystem fmt) (numericalSystem fmt) sub (fun (x y : ℝ) => roundAt fmt (x - y)) fun (x x_1 result : (numericalSystem fmt).Code) => isFinite result = true

Executable subtraction refines one nearest-even rounding for a conventional IEEE format, provided the result is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.mul_refines (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : Numerics.Operation.Finite2If (numericalSystem fmt) (numericalSystem fmt) (numericalSystem fmt) mul (fun (x y : ℝ) => roundAt fmt (x * y)) fun (x x_1 result : (numericalSystem fmt).Code) => isFinite result = true

Executable multiplication refines one nearest-even rounding for a conventional IEEE format, provided the result is finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.fma_refines (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : Numerics.Operation.Finite3If (numericalSystem fmt) (numericalSystem fmt) (numericalSystem fmt) (numericalSystem fmt) fma (fun (x y z : ℝ) => roundAt fmt (x * y + z)) fun (x x_1 x_2 result : (numericalSystem fmt).Code) => isFinite result = true

For a conventional IEEE format, executable fused multiply-add refines one nearest-even rounding when the result remains finite.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.cast_refines (src dst : FloatFormat) (hsrc : src.isIEEE = true) (hdst : dst.isIEEE = true) : Numerics.Operation.Finite1If (numericalSystem src) (numericalSystem dst) (cast src dst) (fun (x : ℝ) => roundAt dst x) fun (x : (numericalSystem src).Code) (result : (numericalSystem dst).Code) => isFinite result = true

A finite cross-format cast refines nearest-even rounding in its destination format.