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 the rounding modes toward $-\infty$ and toward $+\infty$. FloatLib represents these directions with Flocq-style rounding on $\mathbb{R}$ via round together with the floor/ceil rounding functions from FloatLib/Floats/Formats/Flocq/Theory/Rounding/Core.lean.

The rounders work for any radix $\beta$ and exponent selection function fexp satisfying ValidExp.

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 FloatLib.Floats.Interval.roundDown {β : Numerics.Radix} {fexp : ℤ → ℤ} [Formats.Flocq.ValidExp fexp] (x : ℝ) : ℝ

Round down to the $(\beta,\mathtt{fexp})$ grid by taking the floor of the scaled mantissa.

noncomputable def FloatLib.Floats.Interval.roundUp {β : Numerics.Radix} {fexp : ℤ → ℤ} [Formats.Flocq.ValidExp fexp] (x : ℝ) : ℝ

Round up to the $(\beta,\mathtt{fexp})$ grid by taking the ceiling of the scaled mantissa.

theorem FloatLib.Floats.Interval.roundDown_le {β : Numerics.Radix} {fexp : ℤ → ℤ} [Formats.Flocq.ValidExp 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 FloatLib.Floats.Interval.le_roundUp {β : Numerics.Radix} {fexp : ℤ → ℤ} [Formats.Flocq.ValidExp 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 FloatLib.Floats.Interval.Rounder : Type

A pair of real maps bracketing every real number from below and above.

This is the only interface the enclosure proofs need: they use $\operatorname{down}(x)\le x\le\operatorname{up}(x)$ and nothing else. In particular the structure does not require down x or up x to lie on any representable grid, nor does it require monotonicity; the identity maps satisfy both bounds. Representability is a property of a particular instance such as formatRounder, whose outputs lie on the $(\beta,\mathtt{fexp})$ grid by construction.

• down : ℝ → ℝ

  A lower bound for an exact real value.

• up : ℝ → ℝ

  An upper bound for an exact real value.

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

  Rounding down never exceeds the exact value.

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

  Rounding up never falls below the exact value.

noncomputable def FloatLib.Floats.Interval.formatRounder (β : Numerics.Radix) (fexp : ℤ → ℤ) [Formats.Flocq.ValidExp fexp] : Rounder

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

The outputs are values of the Flocq generic format, which has an unbounded exponent range: there is no overflow to infinity and no largest finite value, so this rounder models a binary format's finite grid extended past its exponent limits rather than the encoded format itself.