TorchLean's rounded-real binary32 specialization

FP32 specializes FloatLib's NF to binary32 precision and gradual underflow, with no upper exponent bound. Each arithmetic operation rounds its real result to this grid. The underlying type stores a real value without a representability invariant; use NF.ofReal to round an input.

FloatLib supplies the rounding theorems directly: Model.abs_roundAt_sub_le fmt bounds one rounding step, and round_nearestEven_computed gives its mantissa/exponent representation. Encoded values and exceptional arithmetic use ExecFloat.Binary 8 23.

@[reducible, inline]

abbrev TorchLean.Floats.FP32 : Type

Rounded-real binary32 arithmetic, without an upper exponent bound.

@[reducible, inline]

abbrev TorchLean.Floats.FP32.toReal (x : FP32) : ℝ

Interpret a rounded-real scalar as a real number.