Binary32 observation and error contracts

These interfaces connect TorchLean's binary32 observations to FloatLib's real semantics. Optional observations distinguish finite values from infinities and NaNs. ULP queries return the exponent of the spacing at a finite value, and each arithmetic error bound follows from FloatLib's rounding theorem with the original finiteness hypotheses.

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.IEEE754.IEEE32Exec.toReal? (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) : Option ℝ

Real observation of a finite word; infinities and NaNs have no real observation.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_eq_ite (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) : toReal? x = if FloatLib.Floats.ExecFloat.Binary.isFinite x = true then some (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal else none

Optional real observation succeeds exactly when the word is finite.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_eq_some_toReal_of_isFinite_eq_true {x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4} (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) : toReal? x = some (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal

A finite word has the same optional and total real observations.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_eq_none_of_isFinite_eq_false {x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4} (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = false) : toReal? x = none

A nonfinite word has no optional real observation.

def TorchLean.Floats.IEEE754.IEEE32Exec.ulpExp? (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) : Option ℤ

ULP exponent of a finite word, including the subnormal spacing at zero.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.ulpExp?_isSome (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) : (ulpExp? x).isSome = FloatLib.Floats.ExecFloat.Binary.isFinite x

ULP queries succeed precisely on finite words.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.ulpExp?_eq_none_iff (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) : ulpExp? x = none ↔ FloatLib.Floats.ExecFloat.Binary.isFinite x = false

Infinities and NaNs are exactly the words without a finite ULP exponent.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.bpow_ulpExp?_eq_ulp32 (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) {d : FloatLib.Numerics.Dyadic} (hx : (FloatLib.Floats.ExecFloat.Binary.toModel x).toDyadic? = some d) : Option.map (FloatLib.Floats.Formats.Flocq.bpow FloatLib.Numerics.binaryRadix) (ulpExp? x) = some (ulp32 (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal)

The executable ULP exponent gives the exact real spacing at a decoded value.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.bpow_eq_ulp32_of_ulpExp?_eq_some {x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4} {k : ℤ} (hx : ulpExp? x = some k) : FloatLib.Floats.Formats.Flocq.bpow FloatLib.Numerics.binaryRadix k = ulp32 (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal

A successful ULP query identifies the real spacing directly.

def TorchLean.Floats.IEEE754.IEEE32Exec.absorbs (a b : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) : Bool

Whether adding the second word leaves the first word unchanged.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.round32_add_eq_left_of_absorbs {a b : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4} {da db : FloatLib.Numerics.Dyadic} (ha : (FloatLib.Floats.ExecFloat.Binary.toModel a).toDyadic? = some da) (hb : (FloatLib.Floats.ExecFloat.Binary.toModel b).toDyadic? = some db) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.add a b) = true) (habs : absorbs a b = true) : round32 ((FloatLib.Floats.ExecFloat.Binary.toModel a).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel b).toReal) = (FloatLib.Floats.ExecFloat.Binary.toModel a).toReal

An observed absorption agrees with the rounded-real addition.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.round32_add_eq_left_of_absorbs_of_isFinite {a b : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4} (ha : FloatLib.Floats.ExecFloat.Binary.isFinite a = true) (hb : FloatLib.Floats.ExecFloat.Binary.isFinite b = true) (hadd : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.add a b) = true) (habs : absorbs a b = true) : round32 ((FloatLib.Floats.ExecFloat.Binary.toModel a).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel b).toReal) = (FloatLib.Floats.ExecFloat.Binary.toModel a).toReal

Finiteness checks suffice to establish rounded-real absorption.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sub_eq_computed_of_isFinite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (hy : FloatLib.Floats.ExecFloat.Binary.isFinite y = true) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.sub x y) = true) : (FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.sub x y)).toReal = FloatLib.Floats.Formats.Flocq.toReal { mantissa := FloatLib.Floats.Formats.Flocq.nearestEvenMantissa (FloatLib.Floats.Formats.Flocq.scaledMantissa FloatLib.Numerics.binaryRadix fexp32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)), exponent := FloatLib.Floats.Formats.Flocq.cexp FloatLib.Numerics.binaryRadix fexp32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal) }

Effective nearest-even representation of a finite subtraction.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_div_eq_computed_of_isFinite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.div x y) = true) : (FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.div x y)).toReal = FloatLib.Floats.Formats.Flocq.toReal { mantissa := FloatLib.Floats.Formats.Flocq.nearestEvenMantissa (FloatLib.Floats.Formats.Flocq.scaledMantissa FloatLib.Numerics.binaryRadix fexp32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal / (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)), exponent := FloatLib.Floats.Formats.Flocq.cexp FloatLib.Numerics.binaryRadix fexp32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal / (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal) }

Effective nearest-even representation of a finite division result.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_add_eq_ite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) : toReal? (FloatLib.Floats.ExecFloat.add x y) = if FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.add x y) = true then some (fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)) else none

Optional addition result characterized by one real rounding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_mul_eq_ite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) : toReal? (FloatLib.Floats.ExecFloat.mul x y) = if FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.mul x y) = true then some (fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)) else none

Optional multiplication result characterized by one real rounding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_fma_eq_ite (x y z : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) : toReal? ((fun (left right addend : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯)) (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯))) => FloatLib.Floats.ExecFloat.Binary.fma left right addend FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x y z) = if FloatLib.Floats.ExecFloat.Binary.isFinite ((fun (left right addend : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯)) (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯))) => FloatLib.Floats.ExecFloat.Binary.fma left right addend FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x y z) = true then some (fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel z).toReal)) else none

Optional fused multiply-add result characterized by one real rounding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_sqrt_eq_ite (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) : toReal? ((fun (value : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯)) (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯))) => FloatLib.Floats.ExecFloat.Binary.sqrt value FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x) = if FloatLib.Floats.ExecFloat.Binary.isFinite ((fun (value : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯)) (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯))) => FloatLib.Floats.ExecFloat.Binary.sqrt value FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x) = true then some (fp32Round √(FloatLib.Floats.ExecFloat.Binary.toModel x).toReal) else none

Optional square-root result characterized by one real rounding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_div_eq_ite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) : toReal? (FloatLib.Floats.ExecFloat.div x y) = if FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.div x y) = true then some (fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal / (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)) else none

Optional division result, including finite division by infinity.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_minimum_of_isFinite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (hy : FloatLib.Floats.ExecFloat.Binary.isFinite y = true) : FloatLib.Floats.ExecFloat.Binary.isFinite (x ⊓ y) = true

Minimum of two finite words remains finite, including either signed zero.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_maximum_of_isFinite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (hy : FloatLib.Floats.ExecFloat.Binary.isFinite y = true) : FloatLib.Floats.ExecFloat.Binary.isFinite (x ⊔ y) = true

Maximum of two finite words remains finite, including either signed zero.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_minimum_eq_min_of_isFinite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (hy : FloatLib.Floats.ExecFloat.Binary.isFinite y = true) : toReal? (x ⊓ y) = some (min (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

Optional minimum agrees with real minimum on finite inputs.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_maximum_eq_max_of_isFinite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (hy : FloatLib.Floats.ExecFloat.Binary.isFinite y = true) : toReal? (x ⊔ y) = some (max (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

Optional maximum agrees with real maximum on finite inputs.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round_abs_error (x : ℝ) : |fp32Round x - x| ≤ eps32 x

Nearest-even binary32 rounding incurs at most half an ULP of absolute error.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round_relative_error_of_normal (x : ℝ) (hx : x ≠ 0) (hnormal : FP32.minNormal ≤ |x|) : FloatLib.Floats.Formats.Flocq.ErrorBounds.relativeError x (fp32Round x) hx ≤ FloatLib.Floats.Formats.Flocq.bpow FloatLib.Numerics.binaryRadix (-24)

Normal nonzero results have relative error at most binary32 unit roundoff.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_abs_error_of_isFinite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.add x y) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.add x y)).toReal - ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)| ≤ eps32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

Half-ULP absolute error for a finite addition result.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sub_abs_error_of_isFinite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (hx : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (hy : FloatLib.Floats.ExecFloat.Binary.isFinite y = true) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.sub x y) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.sub x y)).toReal - ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)| ≤ eps32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

Half-ULP absolute error for subtraction of finite values with a finite result.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_mul_abs_error_of_isFinite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.mul x y) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.mul x y)).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal| ≤ eps32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

Half-ULP absolute error for a finite multiplication result.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_div_abs_error_of_isFinite (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.div x y) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.div x y)).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal / (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal| ≤ eps32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal / (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

Half-ULP absolute error for a finite division result.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_fma_abs_error_of_isFinite (x y z : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite ((fun (left right addend : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯)) (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯))) => FloatLib.Floats.ExecFloat.Binary.fma left right addend FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x y z) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel ((fun (left right addend : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯)) (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯))) => FloatLib.Floats.ExecFloat.Binary.fma left right addend FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x y z)).toReal - ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel z).toReal)| ≤ eps32 ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel z).toReal)

Half-ULP absolute error for a finite single-rounding fused multiply-add result.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sqrt_abs_error_of_isFinite (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite ((fun (value : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯)) (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯))) => FloatLib.Floats.ExecFloat.Binary.sqrt value FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel ((fun (value : FloatLib.Floats.ExecFloat (FloatLib.Floats.Formats.BinaryInterchange.Configured.Family (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (FloatLib.Floats.Formats.BinaryInterchange.Configured.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯)) (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.format 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) toReal?._proof_1 toReal?._proof_2 toReal?._proof_3 toReal?._proof_4) (1 + 8 + 23) ⋯))) => FloatLib.Floats.ExecFloat.Binary.sqrt value FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x)).toReal - √(FloatLib.Floats.ExecFloat.Binary.toModel x).toReal| ≤ eps32 √(FloatLib.Floats.ExecFloat.Binary.toModel x).toReal

Half-ULP absolute error for a finite square-root result.