Decoding mkBits back to reals

Many IEEE32Exec proofs need to reason about floats that are constructed directly from their bitfields:

ofBits (mkBits sign exp frac)

When exp < 255 (i.e. not all-ones) and frac < 2^23, this is a finite float32 value (normal/subnormal/zero) and we can compute its real meaning explicitly.

This module exposes the finite-case decoding lemma as part of the IEEEExec proof interface, so the bridge, interval, and runtime-approximation developments share the same closed-form real expression.

Main decoding lemma

Recall:

• if exp = 0 and frac = 0 we have signed zero (both map to real 0),
• if exp = 0 and frac ≠ 0 we have a subnormal with value frac * 2^-149,
• if exp ≠ 0 we have a normal with value (2^23 + frac) * 2^(exp - 150).

All of this is encoded in toDyadic? and exposed here via toReal.

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toReal_ofBits_mkBits_fin (sign : Bool) (exp frac : ℕ) (hexp : exp < 255) (hfrac : frac < 2 ^ 23) : (ofBits (mkBits sign exp frac)).toReal = if exp = 0 then if frac = 0 then 0 else if sign = true then -(↑frac * neuralBpow binaryRadix (-149)) else ↑frac * neuralBpow binaryRadix (-149) else if sign = true then -(↑(pow2 23 + frac) * neuralBpow binaryRadix (Int.ofNat exp - 150)) else ↑(pow2 23 + frac) * neuralBpow binaryRadix (Int.ofNat exp - 150)

Decode ofBits (mkBits sign exp frac) to a closed-form real expression (finite case).

Assumptions:

• exp < 255 so the exponent field is not all ones (excluding NaN/Inf),
• frac < 2^23 so the fraction fits in the binary32 layout.

Conclusion: toReal returns the standard IEEE-754 normal/subnormal/zero formulas.