Error Bounds for General Rounding Modes

A valid rounding mode selects one of the two adjacent representable values. Consequently its absolute error is at most one ULP. Nearest rounding sharpens this to half an ULP; this file records the one-ULP result needed for directed and toward-zero modes.

theorem TorchLean.Floats.neural_round_abs_error_le_ulp {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) : |neuralRound rnd x - x| ≤ neuralUlp β fexp x

Every valid generic rounding mode has absolute error at most one ULP.

theorem TorchLean.Floats.neural_round_abs_error_lt_ulp_of_inexact {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) [NeuralValidRnd rnd] {x : ℝ} (hinexact : neuralRound rnd x ≠ x) : |neuralRound rnd x - x| < neuralUlp β fexp x

A non-exact valid rounding has error strictly smaller than one ULP.

theorem TorchLean.Floats.relative_error_round_FLX_of_valid {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) (hx : x ≠ 0) : ErrorBounds.relativeError x (neuralRound rnd x) hx ≤ neuralBpow β (1 - prec)

Every valid FLX rounding mode has relative error at most β^(1-prec).

theorem TorchLean.Floats.neural_round_relative_error_FLX_of_valid {β : NeuralRadix} (prec : ℤ) (hprec : 0 < prec) (rnd : ℝ → ℤ) [NeuralValidRnd rnd] (x : ℝ) (hx : x ≠ 0) : ∃ (δ : ℝ), |δ| ≤ neuralBpow β (1 - prec) ∧ neuralRound rnd x = x * (1 + δ)

General FLX rounding admits a multiplicative error model with a one-ULP relative bound.