Total FP32 Bridge: Arithmetic #

This module lifts the finite FP32 refinement results for addition, subtraction, multiplication, division, and square root to the total IEEE32Exec domain. A theorem either recovers the rounded real equation from a finite executable result or leaves the NaN/infinity branch visible through toReal?.

See FP32Total.Core for the finite/special-value split and references.

Arithmetic Refinement #

source

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_eq_fp32Round_of_isFinite (x y : IEEE32Exec) (hfin : (x.add y).isFinite = true) :

(x.add y).toReal = fp32Round (x.toReal + y.toReal)

Addition refinement packaged for total reasoning.

source

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_eq_computed_of_isFinite (x y : IEEE32Exec) (hfin : (x.add y).isFinite = true) :

(x.add y).toReal = neuralToReal { mantissa := neuralNearestEvenMantissa (neuralScaledMantissa binaryRadix fexp32 (x.toReal + y.toReal)), exponent := neuralCexp binaryRadix fexp32 (x.toReal + y.toReal) }

Finite executable addition also agrees with the canonical mantissa/exponent produced by the effective nearest-even calculation layer.

source

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sub_eq_fp32Round_of_isFinite (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) (hfin : (x.sub y).isFinite = true) :

(x.sub y).toReal = fp32Round (x.toReal - y.toReal)

Subtraction refinement packaged for total reasoning (hide dyadic witnesses).

This is the finite-path wrapper around toReal_sub_eq_fp32Round, replacing explicit toDyadic? witnesses with the more user-facing finiteness hypotheses.

source