Directed rounding (down/up) for Flocq-style formats

For interval propagation under a discrete numeric grid (float, fixed-point, quantization), one typically wants directed rounding at interval endpoints:

• down x is a representable value with $\operatorname{down}(x)\le x$,
• up x is a representable value with $x\le\operatorname{up}(x)$.

In IEEE-754 hardware this corresponds to rounding modes “toward $-\infty$” and “toward $+\infty$”. In TorchLean’s proof-oriented model we represent this with Flocq-style rounding on $\mathbb{R}$ via neuralRound together with the floor/ceil rounding functions from NN/Floats/NeuralFloat/Rounding/Core.lean.

This file is format-generic: it works for any radix $\beta$ and exponent selection function fexp satisfying NeuralValidExp.

References:

• IEEE 754-2019 (rounding modes; directed rounding).
• Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., SIAM, 2002.
• Flocq (rounded arithmetic on reals).

noncomputable def TorchLean.Floats.Interval.roundDown {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : ℝ

Format-directed rounding down to the $(\beta,\mathtt{fexp})$ grid (via floor rounding of the scaled mantissa).

noncomputable def TorchLean.Floats.Interval.roundUp {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : ℝ

Format-directed rounding up to the $(\beta,\mathtt{fexp})$ grid (via ceil rounding of the scaled mantissa).

theorem TorchLean.Floats.Interval.roundDown_le {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : roundDown x ≤ x

Correctness of directed rounding down: roundDown x is an enclosure lower bound.

This is the format-generic analogue of the IEEE-754 fact that rounding toward $-\infty$ never exceeds the exact real value.

theorem TorchLean.Floats.Interval.le_roundUp {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : x ≤ roundUp x

Correctness of directed rounding up: roundUp x is an enclosure upper bound.

This is the format-generic analogue of the IEEE-754 fact that rounding toward $+\infty$ is never below the exact real value.

structure TorchLean.Floats.Interval.Rounder : Type

A focused “rounder” interface for enclosure-style interval arithmetic.

Monotonicity of down/up is not required: enclosure proofs use only $\operatorname{down}(x)\le x\le\operatorname{up}(x)$.

• down : ℝ → ℝ

  down.

• up : ℝ → ℝ

  up.

• down_le (x : ℝ) : self.down x ≤ x

  down le.

• le_up (x : ℝ) : x ≤ self.up x

  le up.

noncomputable def TorchLean.Floats.Interval.formatRounder (β : NeuralRadix) (fexp : ℤ → ℤ) [NeuralValidExp fexp] : Rounder

Canonical rounder for the $(\beta,\mathtt{fexp})$ format via roundDown/roundUp.