MkBitsToDyadic

Exec32.lean defines the bit-level encoding/decoding functions for IEEE-754 binary32, including mkBits and toDyadic?.

This module provides the finite-path decoding lemma for bit patterns constructed as ofBits (mkBits sign exp frac). Keeping the lemma in a dedicated module avoids import cycles and gives the bridge, interval, and runtime-approximation proofs a shared decoding interface.

toDyadic? (ofBits (mkBits …)) on the finite path

theorem TorchLean.Floats.IEEE754.IEEE32Exec.toDyadic?_ofBits_mkBits_fin (sign : Bool) (exp frac : ℕ) (hexp : exp < 255) (hfrac : frac < 2 ^ 23) : (ofBits (mkBits sign exp frac)).toDyadic? = if exp = 0 then if frac = 0 then some { sign := sign, mant := 0, exp := 0 } else some { sign := sign, mant := frac, exp := -149 } else some { sign := sign, mant := pow2 23 + frac, exp := Int.ofNat exp - 150 }

Decode ofBits (mkBits sign exp frac) to a dyadic in the finite range (exp < 255).

This is the exact decoding rule used throughout IEEEExec proofs that construct floats from their fields and then want to reason about their real meaning via toDyadic?.