Real interpretation of binary models

Finite format-parameterized bit patterns denote exact real values. Arithmetic refinement belongs in later modules, after the executable operation has been related to one exact dyadic intermediate and one rounding step.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.toReal_of_mantissa_zero (sign : Bool) (exponent : ℤ) : { negative := sign, significand := 0, exponent := exponent }.toReal = 0

A dyadic with zero mantissa denotes zero, independently of its sign and exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.toReal_eq_signedSignificand (d : Numerics.Dyadic) : d.toReal = ↑d.signedSignificand * Flocq.bpow Numerics.binaryRadix d.exponent

Numerics.Dyadic real semantics expressed using a signed integer significand.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.signedSignificand_shiftLeft (d : Numerics.Dyadic) (shift : ℕ) : ↑{ negative := d.negative, significand := d.significand.shiftLeft shift, exponent := 0 }.signedSignificand = ↑d.signedSignificand * Flocq.bpow Numerics.binaryRadix (Int.ofNat shift)

Left-shifting a signed significand multiplies its real value by the matching power of two.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.toReal_addDyadic (a b : Numerics.Dyadic) : (addDyadic a b).toReal = a.toReal + b.toReal

Exact dyadic addition agrees with addition in the real semantics.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.toReal_mul (a b : Numerics.Dyadic) : { negative := a.negative ^^ b.negative, significand := a.significand * b.significand, exponent := a.exponent + b.exponent }.toReal = a.toReal * b.toReal

The exact dyadic product used by Model.mul agrees with real multiplication.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.toReal? {fmt : FloatFormat} (x : Model fmt) : Option ℝ

Real interpretation for finite values; returns none for NaN and infinity.

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

Total real interpretation, mapping NaN and infinity to 0. Numerical theorems must therefore establish finiteness or handle exceptional inputs separately.

noncomputable def FloatLib.Floats.Formats.BinaryInterchange.Model.unpackedToReal (x : Float.Model.UnpackedFloat) : ℝ

Real interpretation of Lean's unpacked logical float; NaN and infinity map to zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpackedToReal_zero (sign : Float.Model.UnpackedFloat.Sign) : unpackedToReal (Float.Model.UnpackedFloat.zero sign) = 0

Both signed zeros of Lean's unpacked float model denote the real zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.unpackedToReal_finite (sign : Float.Model.UnpackedFloat.Sign) (mantissa : ℕ) (exponent : ℤ) (hm : 0 < mantissa) : unpackedToReal (Float.Model.UnpackedFloat.finite sign mantissa exponent hm) = (if modelSignBit sign = true then -1 else 1) * ↑mantissa * Flocq.bpow Numerics.binaryRadix exponent

A finite unpacked model value denotes its signed integer mantissa times its dyadic scale.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_eq {fmt : FloatFormat} (x : Model fmt) : x.toReal = match x.toDyadic? with | some d => d.toReal | none => 0

toReal is the dyadic denotation on finite values and zero on NaN and infinities.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_zero (fmt : FloatFormat) (sign : Bool) : (zero fmt sign).toReal = 0

The policy-aware zero constructor denotes zero for every encoding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_eq_unpackedToReal_toModel {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (x : Model fmt) : x.toReal = unpackedToReal x.toModel

Executable and logical decoding agree for formats represented by Lean's IEEE model.