Total FP32 Bridge: Effective Finite Results

The arithmetic bridge states refinement under a finiteness hypothesis. This module packages the same facts as executable implications: when toReal? returns some r, the theorem identifies r with the corresponding FP32 rounded-real operation. It also derives useful finite-result facts for operations whose IEEE rules rule out exceptional results.

See FP32Total.Core for the total bridge convention and bibliography.

Effective finite results

theorem TorchLean.Floats.IEEE754.IEEE32Exec.fp32Round_eq_computed (z : ℝ) : fp32Round z = neuralToReal { mantissa := neuralNearestEvenMantissa (neuralScaledMantissa binaryRadix fexp32 z), exponent := neuralCexp binaryRadix fexp32 z }

fp32Round agrees with the canonical output of the effective nearest-even calculation.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sub_eq_computed_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) (hfin : (x.sub y).isFinite = true) : (x.sub y).toReal = neuralToReal { mantissa := neuralNearestEvenMantissa (neuralScaledMantissa binaryRadix fexp32 (x.toReal - y.toReal)), exponent := neuralCexp binaryRadix fexp32 (x.toReal - y.toReal) }

Effective representation of finite executable subtraction.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_mul_eq_computed_of_isFinite (x y : IEEE32Exec) (hfin : (x.mul y).isFinite = true) : (x.mul y).toReal = neuralToReal { mantissa := neuralNearestEvenMantissa (neuralScaledMantissa binaryRadix fexp32 (x.toReal * y.toReal)), exponent := neuralCexp binaryRadix fexp32 (x.toReal * y.toReal) }

Effective representation of finite executable multiplication.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_div_eq_computed_of_isFinite (x y : IEEE32Exec) (hfin : (x.div y).isFinite = true) : (x.div y).toReal = neuralToReal { mantissa := neuralNearestEvenMantissa (neuralScaledMantissa binaryRadix fexp32 (x.toReal / y.toReal)), exponent := neuralCexp binaryRadix fexp32 (x.toReal / y.toReal) }

Effective representation of finite executable division.

“Both” view: toReal? semantics as an ite

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_add_eq_ite (x y : IEEE32Exec) : (x.add y).toReal? = if (x.add y).isFinite = true then some (fp32Round (x.toReal + y.toReal)) else none

toReal? (add x y) as an ite over finiteness.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_mul_eq_ite (x y : IEEE32Exec) : (x.mul y).toReal? = if (x.mul y).isFinite = true then some (fp32Round (x.toReal * y.toReal)) else none

toReal? (mul x y) as an ite over finiteness.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_fma_eq_ite (x y z : IEEE32Exec) : (x.fma y z).toReal? = if (x.fma y z).isFinite = true then some (fp32Round (x.toReal * y.toReal + z.toReal)) else none

toReal? (fma x y z) as an ite over finiteness.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_sqrt_eq_ite (x : IEEE32Exec) : x.sqrt.toReal? = if x.sqrt.isFinite = true then some (fp32Round √x.toReal) else none

toReal? (sqrt x) as an ite over finiteness.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_div_eq_ite (x y : IEEE32Exec) : (x.div y).toReal? = if (x.div y).isFinite = true then some (fp32Round (x.toReal / y.toReal)) else none

toReal? (div x y) as an ite over finiteness.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_minimum_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.minimum y).isFinite = true

minimum of two finite values is finite.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_minimum_eq_min_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.minimum y).toReal? = some (min x.toReal y.toReal)

On finite inputs, toReal? (minimum x y) returns some (min (toReal x) (toReal y)).

theorem TorchLean.Floats.IEEE754.IEEE32Exec.isFinite_maximum_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.maximum y).isFinite = true

maximum of two finite values is finite.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal?_maximum_eq_max_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) : (x.maximum y).toReal? = some (max x.toReal y.toReal)

On finite inputs, toReal? (maximum x y) returns some (max (toReal x) (toReal y)).