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.isFinite_sub_of_isFinite_of_nonneg (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) (hx0 : 0 ≤ x.toReal) (hy0 : 0 ≤ y.toReal) : (x.sub y).isFinite = true

Subtraction of two finite, nonnegative binary32 values cannot overflow.

Both operands lie between zero and the largest finite binary32 value, so their exact difference lies in the symmetric interval bounded by that value. The executable dyadic rounder therefore returns a finite result.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_sub_eq_sub_of_sterbenz (x y : IEEE32Exec) (hx : x.isFinite = true) (hy : y.isFinite = true) (hxpos : 0 < x.toReal) (hypos : 0 < y.toReal) (hxy : x.toReal ≤ 2 * y.toReal) (hyx : y.toReal ≤ 2 * x.toReal) : (x.sub y).toReal = x.toReal - y.toReal

Executable Sterbenz theorem for finite binary32 values.

If two positive operands are within a factor of two, then bit-level subtraction is finite and denotes the exact real difference. The result combines executable-operation refinement, representability of finite bit patterns, and the rounded-real Sterbenz theorem.

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.