Order Theory for Generic Rounding

Monotonicity is subtle because two inputs may be scaled with different canonical exponents. The proof separates equal-grid inputs from inputs in different magnitude bins and uses the bounds from Rounding.Generic in the latter case.

theorem FloatLib.Floats.Formats.Flocq.round_le_of_cexp_eq {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] {x y : ℝ} (hxy : x ≤ y) (he : cexp β fexp x = cexp β fexp y) : round rnd x ≤ round rnd y

Rounding is monotone when both inputs use the same canonical exponent.

theorem FloatLib.Floats.Formats.Flocq.round_mono_pos {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] {x y : ℝ} (hx : 0 < x) (hxy : x ≤ y) : round rnd x ≤ round rnd y

Positive generic rounding is monotone.

theorem FloatLib.Floats.Formats.Flocq.round_nonneg {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] {x : ℝ} (hx : 0 ≤ x) : 0 ≤ round rnd x

Rounding a nonnegative value with a valid mode produces a nonnegative value.

theorem FloatLib.Floats.Formats.Flocq.round_nonpos {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] {x : ℝ} (hx : x ≤ 0) : round rnd x ≤ 0

Rounding a nonpositive value with a valid mode produces a nonpositive value.

theorem FloatLib.Floats.Formats.Flocq.round_mono {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] {x y : ℝ} (hxy : x ≤ y) : round rnd x ≤ round rnd y

Generic rounding is monotone on all real inputs.

theorem FloatLib.Floats.Formats.Flocq.generic_le_round {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] {x y : ℝ} (hx : genericFormat β fexp x) (hxy : x ≤ y) : x ≤ round rnd y

A representable lower value remains below rounding of any larger input.

theorem FloatLib.Floats.Formats.Flocq.round_le_generic {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] {x y : ℝ} (hy : genericFormat β fexp y) (hxy : x ≤ y) : round rnd x ≤ y

Rounding of a smaller input remains below a representable upper value.

theorem FloatLib.Floats.Formats.Flocq.round_floor_point {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : RoundDownPoint (genericFormat β fexp) x (round floorRound x)

Directed-down generic rounding selects the greatest representable value below its input.

theorem FloatLib.Floats.Formats.Flocq.round_ceil_point {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : RoundUpPoint (genericFormat β fexp) x (round ceilRound x)

Directed-up generic rounding selects the least representable value above its input.

theorem FloatLib.Floats.Formats.Flocq.round_trunc_point {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : RoundTowardZeroPoint (genericFormat β fexp) x (round truncRound x)

Generic truncation satisfies the toward-zero rounding specification.

theorem FloatLib.Floats.Formats.Flocq.toNearest_is_nearest_integer (rnd : ℝ → ℤ) [ValidRndToNearest rnd] (x : ℝ) (n : ℤ) : |↑(rnd x) - x| ≤ |↑n - x|

A nearest rounding rule selects an integer at least as close to the input as every other integer.

Only the half-unit bound of ValidRndToNearest is used: any other integer is at distance at least one from the selected integer, hence at least one half from the input.

theorem FloatLib.Floats.Formats.Flocq.round_toNearest_error_le {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRndToNearest rnd] (other : ℝ → ℤ) (x : ℝ) : |round rnd x - x| ≤ |round other x - x|

Nearest generic rounding is no farther from the input than any other integer rounding.

theorem FloatLib.Floats.Formats.Flocq.round_nearestEven_error_le {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (x : ℝ) : |round nearestEven x - x| ≤ |round rnd x - x|

Nearest-even generic rounding is no farther from the input than any other integer rounding.

theorem FloatLib.Floats.Formats.Flocq.round_toNearest_point {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRndToNearest rnd] (x : ℝ) : RoundNearestPoint (genericFormat β fexp) x (round rnd x)

Every nearest rounding rule selects a globally nearest representable value.

theorem FloatLib.Floats.Formats.Flocq.round_nearestEven_point {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : RoundNearestPoint (genericFormat β fexp) x (round nearestEven x)

Nearest-even rounding selects a globally nearest representable value.