Finite binary32 refinement for proof consumers

These lemmas transfer FloatLib's real rounding theorems through the configured binary32 codec. The executable operations remain FloatLib operations. The total refinement theorems assume only a finite result and discharge exceptional inputs internally. In particular, division of a finite value by infinity produces signed zero, agreeing with the totalized real interpretation.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_eq_true_of_toDyadic?_some {x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4} {d : FloatLib.Numerics.Dyadic} (h : x.toModel.toDyadic? = some d) : x.isFinite = true

A decoded dyadic witnesses that the IEEE value is finite.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toModel_sub (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4) : FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.sub x y) = x.toModel.sub y.toModel

Configured subtraction decodes to FloatLib's model subtraction.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toModel_div (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4) : FloatLib.Floats.ExecFloat.Binary.toModel (FloatLib.Floats.ExecFloat.div x y) = x.toModel.div y.toModel

Configured division decodes to FloatLib's model division.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toModel_fma (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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4) : FloatLib.Floats.ExecFloat.Binary.toModel ((fun (left right addend : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4) (1 + 8 + 23) ⋯))) => left.fma right addend) x y z) = x.toModel.fma y.toModel z.toModel

Configured nearest-even FMA decodes to the model's single-rounding FMA.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toModel_sqrt (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4) : FloatLib.Floats.ExecFloat.Binary.toModel ((fun (value : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4) (1 + 8 + 23) ⋯))) => value.sqrt) x) = x.toModel.sqrt

Configured nearest-even square root decodes to the model square root.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_zero : (FloatLib.Floats.ExecFloat.Binary.toModel 0).toReal = 0

The binary32 zero literal denotes real 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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4} (hx : x.isFinite = true) (hy : y.isFinite = true) : (x ⊓ y).toModel.toReal = min x.toModel.toReal y.toModel.toReal

IEEE minimum agrees with real minimum on finite operands, including signed zeros.

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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4} (hx : x.isFinite = true) (hy : y.isFinite = true) : (x ⊔ y).toModel.toReal = max x.toModel.toReal y.toModel.toReal

IEEE maximum agrees with real maximum on finite operands, including signed zeros.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sub_eq_round_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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal - y.toModel.toReal)

Finite subtraction refines one nearest-even rounding of the real difference.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_roundDyadic_eq_round {d : FloatLib.Numerics.Dyadic} (hfin : (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 d)).isFinite = true) : (FloatLib.Floats.ExecFloat.Binary.ofModel (FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadic FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 d)).toModel.toReal = FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 d.toReal

Finite dyadic rounding refines binary32 rounding of the exact dyadic real value.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sqrt_eq_round {x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4} {dx : FloatLib.Numerics.Dyadic} (hx : x.toModel.toDyadic? = some dx) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite ((fun (value : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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 := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4) (1 + 8 + 23) ⋯))) => value.sqrt) x)).toReal = FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 √x.toModel.toReal

Finite square-root evaluation excludes negative nonzero inputs and refines real rounding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_fma_eq_round_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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite ((fun (left right addend : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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 := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4) (1 + 8 + 23) ⋯))) => left.fma right addend) x y z)).toReal = FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal * y.toModel.toReal + z.toModel.toReal)

Fused multiply-add refinement packaged for total reasoning.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sqrt_eq_round_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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4) (hfin : FloatLib.Floats.ExecFloat.Binary.isFinite ((fun (value : FloatLib.Floats.ExecFloat.Binary { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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 := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.expWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.fracWidth { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._proof_4 }.encoding { expWidth := 8, expWidth_ge_two := isFinite_eq_true_of_toDyadic?_some._proof_1, fracWidth := 23, fracWidth_pos := isFinite_eq_true_of_toDyadic?_some._proof_2, exponentBias := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8, encoding := FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee, exponentBias_pos := isFinite_eq_true_of_toDyadic?_some._proof_3, exponentBias_le_maxFinite := isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._proof_4) (1 + 8 + 23) ⋯))) => value.sqrt) x)).toReal = FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 √x.toModel.toReal

Square-root refinement packaged for total reasoning.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_div_eq_round_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) isFinite_eq_true_of_toDyadic?_some._proof_1 isFinite_eq_true_of_toDyadic?_some._proof_2 isFinite_eq_true_of_toDyadic?_some._proof_3 isFinite_eq_true_of_toDyadic?_some._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.BinaryInterchange.Model.roundAt FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.binary32 (x.toModel.toReal / y.toModel.toReal)

Division refinement packaged for total reasoning.