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 x.isFinite = true then some x.toModel.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 : x.isFinite = true) : toReal? x = some x.toModel.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 : x.isFinite = 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 = x.isFinite

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 ↔ x.isFinite = false

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

theorem TorchLean.Floats.IEEE754.IEEE32Exec.bpow_ulpExp?_eq_ulp (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 : x.toModel.toDyadic? = some d) : Option.map (FloatLib.Floats.Formats.Flocq.bpow FloatLib.Numerics.binaryRadix) (ulpExp? x) = some (FloatLib.Floats.Formats.BinaryInterchange.Model.ulpAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 x.toModel.toReal)

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

theorem TorchLean.Floats.IEEE754.IEEE32Exec.bpow_eq_ulp_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 = FloatLib.Floats.Formats.BinaryInterchange.Model.ulpAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 x.toModel.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 encoded value unchanged, including its zero sign. The real-valued absorption theorem below additionally requires a finite result.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.round_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} (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite (FloatLib.Floats.ExecFloat.add a b) = true) (habs : absorbs a b = true) : FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (a.toModel.toReal + b.toModel.toReal) = a.toModel.toReal

An observed absorption agrees with the rounded-real addition. Only finiteness of the sum is required: a finite executable sum already forces finite operands.

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 : x.isFinite = true) (hy : y.isFinite = 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 (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32) (x.toModel.toReal - y.toModel.toReal)), exponent := FloatLib.Floats.Formats.Flocq.cexp FloatLib.Numerics.binaryRadix (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32) (x.toModel.toReal - y.toModel.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 (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32) (x.toModel.toReal / y.toModel.toReal)), exponent := FloatLib.Floats.Formats.Flocq.cexp FloatLib.Numerics.binaryRadix (FloatLib.Floats.Formats.BinaryInterchange.Model.fexpOf FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32) (x.toModel.toReal / y.toModel.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 (FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal + y.toModel.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 (FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal * y.toModel.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.Binary { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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) ⋯))) => left.fma right addend) x y z) = if FloatLib.Floats.ExecFloat.Binary.isFinite ((fun (left right addend : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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) ⋯))) => left.fma right addend) x y z) = true then some (FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal * y.toModel.toReal + z.toModel.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.Binary { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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) ⋯))) => value.sqrt) x) = if FloatLib.Floats.ExecFloat.Binary.isFinite ((fun (value : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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) ⋯))) => value.sqrt) x) = true then some (FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 √x.toModel.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 (FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal / y.toModel.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 : x.isFinite = true) (hy : y.isFinite = true) : (x ⊓ y).isFinite = 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 : x.isFinite = true) (hy : y.isFinite = true) : (x ⊔ y).isFinite = 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 : x.isFinite = true) (hy : y.isFinite = true) : toReal? (x ⊓ y) = some (min x.toModel.toReal y.toModel.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 : x.isFinite = true) (hy : y.isFinite = true) : toReal? (x ⊔ y) = some (max x.toModel.toReal y.toModel.toReal)

Optional maximum agrees with real maximum on finite inputs.

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 - (x.toModel.toReal + y.toModel.toReal)| ≤ FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal + y.toModel.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 : x.isFinite = true) (hy : y.isFinite = 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 - (x.toModel.toReal - y.toModel.toReal)| ≤ FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal - y.toModel.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 - x.toModel.toReal * y.toModel.toReal| ≤ FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal * y.toModel.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 - x.toModel.toReal / y.toModel.toReal| ≤ FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal / y.toModel.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.Binary { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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) ⋯))) => left.fma right addend) x y z) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel ((fun (left right addend : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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) ⋯))) => left.fma right addend) x y z)).toReal - (x.toModel.toReal * y.toModel.toReal + z.toModel.toReal)| ≤ FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal * y.toModel.toReal + z.toModel.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.Binary { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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) ⋯))) => value.sqrt) x) = true) : |(FloatLib.Floats.ExecFloat.Binary.toModel ((fun (value : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := toReal?._proof_1, fracWidth := 23, fracWidth_pos := toReal?._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := toReal?._proof_3, exponentBias_le_maxFinite := toReal?._proof_4 }.exponentBias ⋯ ⋯ ⋯ ⋯ (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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.Code (FloatLib.Floats.Formats.BinaryInterchange.Configured.StoragePlan.forKnownWidth (FloatLib.Floats.ExecFloat.Binary.descriptor 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) ⋯))) => value.sqrt) x)).toReal - √x.toModel.toReal| ≤ FloatLib.Floats.Formats.BinaryInterchange.Model.epsilonAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 √x.toModel.toReal

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