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 down x ≤ x,
• up x is a representable value with x ≤ up x.

In IEEE-754 hardware this corresponds to rounding modes “toward -∞” and “toward +∞”. In TorchLean’s proof-oriented stack we model this with Flocq-style rounding on ℝ via neural_round together with the floor/ceil rounding functions from NN/Floats/NeuralFloat/Rounding.lean.

This file is format-generic: it works for any radix β 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 (β,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 (β,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 -∞” 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 +∞” 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 down x ≤ x ≤ 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 (β,fexp) format via roundDown/roundUp.