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.

@[reducible, inline]

noncomputable abbrev TorchLean.Floats.IEEE754.IEEE32Exec.dyadicToReal (d : FloatLib.Numerics.Dyadic) : ℝ

Real denotation of FloatLib's signed dyadic representation.

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 : (FloatLib.Floats.ExecFloat.Binary.toModel x).toDyadic? = some d) : FloatLib.Floats.ExecFloat.Binary.isFinite x = 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) = (FloatLib.Floats.ExecFloat.Binary.toModel x).sub (FloatLib.Floats.ExecFloat.Binary.toModel y)

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) = (FloatLib.Floats.ExecFloat.Binary.toModel x).div (FloatLib.Floats.ExecFloat.Binary.toModel y)

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 (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) 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.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) 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.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) 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.ExecFloat.Binary.fma left right addend FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x y z) = (FloatLib.Floats.ExecFloat.Binary.toModel x).fma (FloatLib.Floats.ExecFloat.Binary.toModel y) (FloatLib.Floats.ExecFloat.Binary.toModel z)

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 (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) 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.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) 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.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) 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.ExecFloat.Binary.sqrt value FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x) = (FloatLib.Floats.ExecFloat.Binary.toModel x).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_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 : FloatLib.Floats.ExecFloat.Binary.isFinite x = true) (hy : FloatLib.Floats.ExecFloat.Binary.isFinite y = true) : (FloatLib.Floats.ExecFloat.Binary.toModel (x ⊔ y)).toReal = max (FloatLib.Floats.ExecFloat.Binary.toModel x).toReal (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal

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

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sub_eq_fp32Round_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 : 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 = fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal - (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

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

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

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

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_div_eq_fp32Round {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} {dx dy : FloatLib.Numerics.Dyadic} (hx : (FloatLib.Floats.ExecFloat.Binary.toModel x).toDyadic? = some dx) (hy : (FloatLib.Floats.ExecFloat.Binary.toModel y).toDyadic? = some dy) (hden : dy.significand ≠ 0) (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 = fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal / (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

Finite division by a decoded nonzero dyadic refines one real rounding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_fma_eq_fp32Round {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} {dx dy dz : FloatLib.Numerics.Dyadic} (hx : (FloatLib.Floats.ExecFloat.Binary.toModel x).toDyadic? = some dx) (hy : (FloatLib.Floats.ExecFloat.Binary.toModel y).toDyadic? = some dy) (hz : (FloatLib.Floats.ExecFloat.Binary.toModel z).toDyadic? = some dz) (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) 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.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) 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.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) 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.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) 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.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) 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.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) 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.ExecFloat.Binary.fma left right addend FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x y z)).toReal = fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel z).toReal)

Finite FMA refines one rounding of the exact product-plus-addend expression.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sqrt_eq_fp32Round {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 : (FloatLib.Floats.ExecFloat.Binary.toModel x).toDyadic? = some dx) (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) 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.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) 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.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) 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.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) 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.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) 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.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) 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.ExecFloat.Binary.sqrt value FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x)).toReal = fp32Round √(FloatLib.Floats.ExecFloat.Binary.toModel x).toReal

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

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_fma_eq_fp32Round_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 (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) 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.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) 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.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) 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.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) 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.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) 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.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) 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.ExecFloat.Binary.fma left right addend FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x y z)).toReal = fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal * (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal + (FloatLib.Floats.ExecFloat.Binary.toModel z).toReal)

Fused multiply-add refinement packaged for total reasoning.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sqrt_eq_fp32Round_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 (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) 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.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) 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.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) 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.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) 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.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) 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.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) 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.ExecFloat.Binary.sqrt value FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearestEven) x)).toReal = fp32Round √(FloatLib.Floats.ExecFloat.Binary.toModel x).toReal

Square-root refinement packaged for total reasoning.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_div_eq_fp32Round_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 = fp32Round ((FloatLib.Floats.ExecFloat.Binary.toModel x).toReal / (FloatLib.Floats.ExecFloat.Binary.toModel y).toReal)

Division refinement packaged for total reasoning.