FP32: TorchLean's proof-oriented float32 semantics

FP32 is a proof-oriented float32 semantics: it models float computations as real-number operations (ℝ) followed by rounding to a fixed binary32 grid after each primitive operation. This abstraction is designed to support compositional rounding-error bounds over long computations.

What this model does cover:

• binary radix (β = 2)
• IEEE-754-like binary32 exponent/precision parameters, including gradual underflow
• rounding to nearest with ties-to-even

What this model does not cover:

• NaN/Inf payload rules, signed-zero corner cases, and other IEEE “special values”

Special-value semantics live in the executable IEEE32Exec model. Bridge lemmas relate IEEE32Exec back to FP32 on the finite/no-overflow fragment.

Canonical IEEE-754 binary32 configuration

def TorchLean.Floats.fexp32 : ℤ → ℤ

Exponent function for IEEE-754 binary32 (gradual underflow), expressed in Flocq style.

Two numbers here matter:

• prec = 24: binary32 has 23 stored fraction bits, but 24 bits of precision for normal numbers once you include the implicit leading 1.
• emin = -149: the smallest positive subnormal is 2^-149. Using emin = -149 is the usual way to encode gradual underflow in this “rounding-on-ℝ” model.

instance TorchLean.Floats.instNeuralValidExpFexp32 : NeuralValidExp fexp32

fexp32 is the binary32-compatible exponent function used by FP32.

noncomputable def TorchLean.Floats.rnd32 : ℝ → ℤ

Round-to-nearest, ties-to-even (binary32-style default rounding).

This is the rounding mode people typically assume when they say “IEEE float32 rounding”.

instance TorchLean.Floats.instNeuralValidRndRnd32 : NeuralValidRnd rnd32

rnd32 is a valid monotone rounding mode in the generic neural-float sense.

instance TorchLean.Floats.instNeuralValidRndToNearestRnd32 : NeuralValidRndToNearest rnd32

rnd32 is round-to-nearest in the NeuralValidRndToNearest sense.

@[reducible, inline]

abbrev TorchLean.Floats.FP32 : Type

FP32: finite float32 rounding model, as a rounded-ℝ value.

This is the type you want if you are proving numerical stability/error bounds without dealing with NaN/Inf behavior.

@[reducible, inline]

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

Forgetful projection: treat an FP32 value as a real number.

noncomputable def TorchLean.Floats.FP32.maxFinite : ℝ

Convenience constant: the largest finite magnitude representable by the binary32 parameters used by this model (i.e. roughly (2 - 2^-23) * 2^127).

We keep this in FP32 because it is a useful proof-level guard when you want to state “no overflow” side-conditions in a readable way.

noncomputable def TorchLean.Floats.FP32.minNormal : ℝ

Convenience constant: the smallest positive normal binary32 number (roughly 2^-126).

Subnormals exist below this; this constant is mainly useful when you want to distinguish “normal-range” arguments from “subnormal-range” arguments in proofs.