IEEE32Exec and FP32: Arithmetic Operation Refinement

Op-level refinement theorems (finite/no-overflow)

These are the results that the rest of TorchLean typically consumes: statements that each arithmetic operation in IEEE32Exec refines its FP32 real-rounded counterpart.

If you are coming from PyTorch: this is the “float32 math model” that underlies many informal numerical arguments (“the kernel computes the exact real result, then rounds to float32”), but made explicit and proved for our executable kernel.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_add_eq_fp32Round (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hfin : (x.add y).isFinite = true) : (x.add y).toReal = fp32Round (x.toReal + y.toReal)

Finite refinement for addition: IEEE32Exec.add = exact real add + float32 rounding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sub_eq_fp32Round (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hfin : (x.sub y).isFinite = true) : (x.sub y).toReal = fp32Round (x.toReal - y.toReal)

Finite refinement for subtraction, reduced to addition + negation.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_mul_eq_fp32Round (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hfin : (x.mul y).isFinite = true) : (x.mul y).toReal = fp32Round (x.toReal * y.toReal)

Finite refinement for multiplication: IEEE32Exec.mul = exact real mul + float32 rounding.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_fma_eq_fp32Round (x y z : IEEE32Exec) {dx dy dz : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hz : z.toDyadic? = some dz) (hfin : (x.fma y z).isFinite = true) : (x.fma y z).toReal = fp32Round (x.toReal * y.toReal + z.toReal)

Finite refinement for fused multiply-add: fma x y z rounds x*y + z once at the end.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_div_eq_fp32Round (x y : IEEE32Exec) {dx dy : Dyadic} (hx : x.toDyadic? = some dx) (hy : y.toDyadic? = some dy) (hy0 : dy.mant ≠ 0) (hfin : (x.div y).isFinite = true) : (x.div y).toReal = fp32Round (x.toReal / y.toReal)

Finite refinement for division.

At the executable level, division is implemented by forming an exact rational quotient num/den (after aligning dyadic exponents) and then rounding that rational to float32. This theorem states that the overall real meaning is FP32 rounding of real division.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sqrt_eq_fp32Round (x : IEEE32Exec) {dx : Dyadic} (hx : x.toDyadic? = some dx) (hfin : x.sqrt.isFinite = true) : x.sqrt.toReal = fp32Round √x.toReal

Finite refinement for square root.

IEEE32Exec.sqrt computes an executable approximation and then rounds it to float32. This bridge theorem states that, on the finite path, the real meaning agrees with FP32 rounding of Real.sqrt.