Executable Binary32 ULPs and Absorption

ulp32 specifies the unit in the last place as a real number. This file supplies the executable counterpart for IEEE32Exec: ulpExp? reads a finite binary32 payload and returns the exponent k for which the ULP is 2^k. It returns none for NaNs and infinities rather than assigning them an artificial spacing.

The absorption test checks whether adding one executable value to another leaves the first value unchanged. Its soundness theorem transports that observation through the finite-operation bridge to the rounded-real binary32 model.

def TorchLean.Floats.IEEE754.IEEE32Exec.ulpExp? (x : IEEE32Exec) : Option ℤ

Compute the binary32 ULP exponent from an executable bit pattern.

Finite zero has exponent -149. A finite nonzero value with dyadic mantissa m and exponent e has magnitude ⌊log₂ m⌋ + e + 1; applying fexp32 gives its ULP exponent. NaNs and infinities return none.

@[simp]

theorem TorchLean.Floats.IEEE754.IEEE32Exec.ulpExp?_isSome (x : IEEE32Exec) : x.ulpExp?.isSome = x.isFinite

ulpExp? succeeds exactly on finite executable binary32 values.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.ulpExp?_eq_none_iff (x : IEEE32Exec) : x.ulpExp? = none ↔ x.isFinite = false

NaNs and infinities are precisely the values for which ulpExp? returns none.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neuralBpow_ulpExp?_eq_ulp32 (x : IEEE32Exec) {d : Dyadic} (hx : x.toDyadic? = some d) : Option.map (neuralBpow binaryRadix) x.ulpExp? = some (ulp₃₂ x.toReal)

For every finite executable binary32 value, exponentiating the result of ulpExp? gives its rounded-real ULP exactly.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.neuralBpow_eq_ulp32_of_ulpExp?_eq_some {x : IEEE32Exec} {k : ℤ} (hx : x.ulpExp? = some k) : neuralBpow binaryRadix k = ulp₃₂ x.toReal

Direct soundness theorem for the executable query: if ulpExp? x returns k, then 2^k is exactly the rounded-real binary32 ULP at x.

def TorchLean.Floats.IEEE754.IEEE32Exec.absorbs (a b : IEEE32Exec) : Bool

Whether executable binary32 addition leaves its left operand unchanged.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.round32_add_eq_left_of_absorbs {a b : IEEE32Exec} {da db : Dyadic} (ha : a.toDyadic? = some da) (hb : b.toDyadic? = some db) (hfin : (a.add b).isFinite = true) (habs : a.absorbs b = true) : round₃₂ (a.toReal + b.toReal) = a.toReal

If the executable absorption test succeeds on a finite addition, the rounded-real model agrees: rounding the exact real sum returns the left operand.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.round32_add_eq_left_of_absorbs_of_isFinite {a b : IEEE32Exec} (ha : a.isFinite = true) (hb : b.isFinite = true) (hadd : (a.add b).isFinite = true) (habs : a.absorbs b = true) : round₃₂ (a.toReal + b.toReal) = a.toReal

Public finite-value form of absorption soundness. Dyadic decoding witnesses are recovered from the three executable finiteness checks.