Sterbenz's Lemma for Gradual Underflow

This file extends the exact-subtraction result for the unbounded-exponent family FLX to the gradual-underflow family FLT. The latter is the format used by the rounded-real binary32 model.

The proof separates two regimes. Below the normal threshold, FLT values lie on a fixed-exponent grid that is closed under subtraction. Above that threshold, the existing FLX Sterbenz theorem applies, and the resulting normal value can be transported back to FLT.

Reference

• P. H. Sterbenz, Floating-Point Computation, Prentice-Hall, 1974.

theorem TorchLean.Floats.neural_generic_format_FLX_to_FLT_of_normal {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) {x : ℝ} (hxFLX : neuralGenericFormat β (FLXExp prec) x) (hnorm : neuralBpow β (emin + prec - 1) ≤ |x|) : neuralGenericFormat β (FLTExp emin prec) x

An FLX value in the normal range is representable in the corresponding FLT format.

This is the normal-range converse of neural_generic_format_FLT_to_FLX.

theorem TorchLean.Floats.neural_generic_format_FLT_sub_of_le_two_mul {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) {x y : ℝ} (hy : 0 < y) (hyx : y ≤ x) (hx2y : x ≤ 2 * y) (hxFmt : neuralGenericFormat β (FLTExp emin prec) x) (hyFmt : neuralGenericFormat β (FLTExp emin prec) y) : neuralGenericFormat β (FLTExp emin prec) (x - y)

Directed Sterbenz lemma for FLT: if 0 < y ≤ x ≤ 2y and both operands are representable, then their exact difference is representable.

theorem TorchLean.Floats.neural_generic_format_FLT_sterbenz {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) {x y : ℝ} (hx : 0 < x) (hy : 0 < y) (hx2y : x ≤ 2 * y) (hy2x : y ≤ 2 * x) (hxFmt : neuralGenericFormat β (FLTExp emin prec) x) (hyFmt : neuralGenericFormat β (FLTExp emin prec) y) : neuralGenericFormat β (FLTExp emin prec) (x - y)

Sterbenz's lemma for FLT: if two positive representable values are within a factor of two, then their exact difference is representable, including across the subnormal boundary.