Exactness of Addition Errors

For nearest rounding, the error of adding two representable values is itself representable. The proof aligns both operands on the smaller canonical grid, represents the rounded result on that same grid, and uses nearestness to control the canonical exponent of the error.

theorem TorchLean.Floats.neural_add_round_error_generic {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] [NeuralMonotoneExp fexp] {x y : ℝ} (hx : neuralGenericFormat β fexp x) (hy : neuralGenericFormat β fexp y) : neuralGenericFormat β fexp (neuralRound neuralNearestEven (x + y) - (x + y))

The nearest-rounded addition error of two representable values is representable.

theorem TorchLean.Floats.neural_generic_format_FLT_to_FIX {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) {x : ℝ} (hx : neuralGenericFormat β (FLTExp emin prec) x) : neuralGenericFormat β (FIXExp emin) x

Every FLT value lies on its minimum-exponent FIX grid.

theorem TorchLean.Floats.neural_generic_format_FIX_to_FLT_of_abs_le {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) {x : ℝ} (hx : neuralGenericFormat β (FIXExp emin) x) (hbound : |x| ≤ neuralBpow β (prec + emin)) : neuralGenericFormat β (FLTExp emin prec) x

A bounded FIX value is FLT-representable, including the radix-power boundary.

theorem TorchLean.Floats.neural_generic_format_FLT_add_small {β : NeuralRadix} (emin prec : ℤ) (hprec : 0 < prec) {x y : ℝ} (hx : neuralGenericFormat β (FLTExp emin prec) x) (hy : neuralGenericFormat β (FLTExp emin prec) y) (hbound : |x + y| ≤ neuralBpow β (prec + emin)) : neuralGenericFormat β (FLTExp emin prec) (x + y)

A sufficiently small sum of two FLT values is exactly FLT-representable.