Finite proof-indexed binary-interchange arithmetic

The finite Model.At view supports constructors, decoding theorems, directed rounding bounds, and arithmetic operations. Each arithmetic wrapper contains the corresponding executable result together with an erased proof of its real index. Rounded arithmetic requires conventional IEEE descriptors and a finite result.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.At.toValue {fmt : FloatFormat} {r : ℝ} (x : At fmt r) : AtValue fmt (Numerics.NumericalValue.finite r)

Regard a finite refinement through the total numerical-value interface.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.At.ofFinite {fmt : FloatFormat} (x : Model fmt) (hfinite : x.isFinite = true) : At fmt x.toReal

Construct the proof-indexed view of a finite executable float.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.At.zero (fmt : FloatFormat) (sign : Bool) : At fmt 0

The format's policy-aware zero with its exact real interpretation.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.At.one (fmt : FloatFormat) : At fmt 1

Positive one with its exact real interpretation.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.At.negOne (fmt : FloatFormat) : At fmt (-1)

Negative one with its exact real interpretation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.represents {fmt : FloatFormat} {r : ℝ} (x : At fmt r) : Represents (↑x) r

The bundled executable value represents its real index.

@[simp]

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

Every proof-indexed executable float is finite.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.toReal {fmt : FloatFormat} {r : ℝ} (x : At fmt r) : Model.toReal ↑x = r

Decoding a proof-indexed executable float recovers its real index.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.toEReal {fmt : FloatFormat} {r : ℝ} (x : At fmt r) : Model.toEReal ↑x = ↑r

The extended-real interpretation of a proof-indexed executable float is its real index.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.toEReal_addDown_le {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) : (addDown ↑x ↑y).toEReal ≤ ↑(r + s)

Downward-rounded addition of represented inputs is a lower bound on their exact sum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.le_toEReal_addUp {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) : ↑(r + s) ≤ (addUp ↑x ↑y).toEReal

Upward-rounded addition of represented inputs is an upper bound on their exact sum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.toEReal_subDown_le {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) : (subDown ↑x ↑y).toEReal ≤ ↑(r - s)

Downward-rounded subtraction of represented inputs is a lower bound on their exact difference.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.le_toEReal_subUp {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) : ↑(r - s) ≤ (subUp ↑x ↑y).toEReal

Upward-rounded subtraction of represented inputs is an upper bound on their exact difference.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.toEReal_mulDown_le {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) : (mulDown ↑x ↑y).toEReal ≤ ↑(r * s)

Downward-rounded multiplication of represented inputs is a lower bound on their exact product.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.le_toEReal_mulUp {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) : ↑(r * s) ≤ (mulUp ↑x ↑y).toEReal

Upward-rounded multiplication of represented inputs is an upper bound on their exact product.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.toEReal_divDown_le {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) (hy0 : isZero ↑y = false) : (divDown ↑x ↑y).toEReal ≤ ↑(r / s)

Downward-rounded division bounds the exact quotient when the represented divisor is nonzero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.le_toEReal_divUp {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) (hy0 : isZero ↑y = false) : ↑(r / s) ≤ (divUp ↑x ↑y).toEReal

Upward-rounded division bounds the exact quotient when the represented divisor is nonzero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.toEReal_sqrtDown_le {fmt : FloatFormat} {r : ℝ} (x : At fmt r) (hfmt : fmt.isIEEE = true) (hr : 0 ≤ r) : (sqrtDown ↑x).toEReal ≤ ↑√r

Downward-rounded square root bounds the exact square root of a nonnegative represented value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.le_toEReal_sqrtUp {fmt : FloatFormat} {r : ℝ} (x : At fmt r) (hfmt : fmt.isIEEE = true) (hr : 0 ≤ r) : ↑√r ≤ (sqrtUp ↑x).toEReal

Upward-rounded square root bounds the exact square root of a nonnegative represented value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.At.neg {fmt : FloatFormat} {r : ℝ} (x : At fmt r) : At fmt (-r)

Negation transports the real index exactly.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.At.add {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) (hfinite : (Model.add ↑x ↑y).isFinite = true) : At fmt (roundAt fmt (r + s))

Addition transports real indices through one nearest-even rounding step.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.At.sub {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) (hfinite : (Model.sub ↑x ↑y).isFinite = true) : At fmt (roundAt fmt (r - s))

Subtraction transports real indices through one nearest-even rounding step.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.At.mul {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) (hfinite : (Model.mul ↑x ↑y).isFinite = true) : At fmt (roundAt fmt (r * s))

Multiplication transports real indices through one nearest-even rounding step.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.At.fma {fmt : FloatFormat} {r s t : ℝ} (x : At fmt r) (y : At fmt s) (z : At fmt t) (hfmt : fmt.isIEEE = true) (hfinite : (Model.fma ↑x ↑y ↑z).isFinite = true) : At fmt (roundAt fmt (r * s + t))

Fused multiply-add transports real indices through one nearest-even rounding step.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.At.cast {src dst : FloatFormat} {r : ℝ} (x : At src r) (hsrc : src.isIEEE = true) (hdst : dst.isIEEE = true) (hfinite : (Model.cast src dst ↑x).isFinite = true) : At dst (roundAt dst r)

A cross-format cast transports its real index through destination rounding.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.value_ofFinite {fmt : FloatFormat} (x : Model fmt) (hfinite : x.isFinite = true) : ↑(ofFinite x hfinite) = x

Lifting a finite model value records that value as the carrier.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.value_neg {fmt : FloatFormat} {r : ℝ} (x : At fmt r) : ↑x.neg = Model.neg ↑x

The carrier of a negated witness is the model negation.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.value_add {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) (hfinite : (Model.add ↑x ↑y).isFinite = true) : ↑(x.add y hfmt hfinite) = Model.add ↑x ↑y

The carrier of a finite sum witness is the model sum.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.value_sub {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) (hfinite : (Model.sub ↑x ↑y).isFinite = true) : ↑(x.sub y hfmt hfinite) = Model.sub ↑x ↑y

The carrier of a finite difference witness is the model difference.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.value_mul {fmt : FloatFormat} {r s : ℝ} (x : At fmt r) (y : At fmt s) (hfmt : fmt.isIEEE = true) (hfinite : (Model.mul ↑x ↑y).isFinite = true) : ↑(x.mul y hfmt hfinite) = Model.mul ↑x ↑y

The carrier of a finite product witness is the model product.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.value_fma {fmt : FloatFormat} {r s t : ℝ} (x : At fmt r) (y : At fmt s) (z : At fmt t) (hfmt : fmt.isIEEE = true) (hfinite : (Model.fma ↑x ↑y ↑z).isFinite = true) : ↑(x.fma y z hfmt hfinite) = Model.fma ↑x ↑y ↑z

The carrier of a finite fused multiply-add witness is the model fused multiply-add.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.At.value_cast {src dst : FloatFormat} {r : ℝ} (x : At src r) (hsrc : src.isIEEE = true) (hdst : dst.isIEEE = true) (hfinite : (Model.cast src dst ↑x).isFinite = true) : ↑(x.cast hsrc hdst hfinite) = Model.cast src dst ↑x

The carrier of a finite cast witness is the model cast.