FP32: TorchLean's proof-oriented float32 semantics

FP32 is a proof-oriented float32 semantics: it models float computations as real-number operations over $\mathbb{R}$ 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 $\beta=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 the gradual-underflow part of IEEE-754 binary32, 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 $\mathbb{R}$” model.

FLTExp has no upper exponent bound. Overflow and the transition to infinity belong to IEEE32Exec, not this exponent function.

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 real 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.

theorem TorchLean.Floats.FP32.round_eq_computed (x : ℝ) : neuralRound rnd32 x = neuralToReal { mantissa := neuralNearestEvenMantissa (neuralScaledMantissa binaryRadix fexp32 x), exponent := neuralCexp binaryRadix fexp32 x }

Canonical effective mantissa/exponent representation of binary32 rounded-real rounding.

theorem TorchLean.Floats.FP32.add_toReal_eq_computed (a b : FP32) : (a + b).toReal = neuralToReal { mantissa := neuralNearestEvenMantissa (neuralScaledMantissa binaryRadix fexp32 (a.val + b.val)), exponent := neuralCexp binaryRadix fexp32 (a.val + b.val) }

The result of FP32 addition has the canonical mantissa/exponent representation computed by the effective nearest-even rounding layer.

theorem TorchLean.Floats.FP32.sub_toReal_eq_computed (a b : FP32) : (a - b).toReal = neuralToReal { mantissa := neuralNearestEvenMantissa (neuralScaledMantissa binaryRadix fexp32 (a.val - b.val)), exponent := neuralCexp binaryRadix fexp32 (a.val - b.val) }

Effective representation of FP32 subtraction.

theorem TorchLean.Floats.FP32.mul_toReal_eq_computed (a b : FP32) : (a * b).toReal = neuralToReal { mantissa := neuralNearestEvenMantissa (neuralScaledMantissa binaryRadix fexp32 (a.val * b.val)), exponent := neuralCexp binaryRadix fexp32 (a.val * b.val) }

Effective representation of FP32 multiplication.

theorem TorchLean.Floats.FP32.div_toReal_eq_computed (a b : FP32) : (a / b).toReal = neuralToReal { mantissa := neuralNearestEvenMantissa (neuralScaledMantissa binaryRadix fexp32 (a.val / b.val)), exponent := neuralCexp binaryRadix fexp32 (a.val / b.val) }

Effective representation of FP32 division.

noncomputable def TorchLean.Floats.FP32.ieeeMaxFinite : ℝ

The largest finite IEEE-754 binary32 magnitude, $(2-2^{-23})2^{127}$.

This is a bridge guard, not a maximum of FP32: the proof-oriented FLTExp (-149) 24 model has gradual underflow but no upper exponent bound. Executable IEEE binary32 operations must establish this bound before transferring a finite result into the rounded-real model.

theorem TorchLean.Floats.FP32.ieeeMaxFinite_eq : ieeeMaxFinite = ↑(2 ^ 24 - 1) * neuralBpow binaryRadix 104

Mantissa/exponent form of the largest finite binary32 magnitude.

theorem TorchLean.Floats.FP32.ieeeMaxFinite_lt_bpow_128 : ieeeMaxFinite < neuralBpow binaryRadix 128

The largest finite binary32 value lies strictly below 2^128.

noncomputable def TorchLean.Floats.FP32.minNormal : ℝ

Convenience constant: the smallest positive normal binary32 number (approximately $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.

@[simp]

theorem TorchLean.Floats.FP32.minNormal_eq_bpow : minNormal = neuralBpow binaryRadix (-126)

The binary32 minimum normal value is $2^{-126}$.