Generic rounding properties

Rounding in the generic format scales to an integer, applies a valid integer rounding rule, and scales back by a positive radix power. This construction gives the basic order sandwich: directed down is below every valid rounding, and directed up is above it.

These results do not assume a concrete precision family. They form the reusable real-valued layer used when proving executable binary and rational rounding algorithms.

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

Rounding toward negative infinity never exceeds the exact value.

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

Rounding toward positive infinity never falls below the exact value.

theorem FloatLib.Floats.Formats.Flocq.floor_le_valid_round (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) : floorRound x ≤ rnd x

Every valid integer rounding rule returns a value at least as large as the floor.

theorem FloatLib.Floats.Formats.Flocq.valid_round_le_ceil (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) : rnd x ≤ ceilRound x

Every valid integer rounding rule returns a value at most as large as the ceiling.

theorem FloatLib.Floats.Formats.Flocq.valid_round_eq_floor_or_ceil (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) : rnd x = floorRound x ∨ rnd x = ceilRound x

Every valid integer rounding chooses either floor or ceiling.

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

Every valid format rounding lies above directed-down rounding.

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

Every valid format rounding lies below directed-up rounding.

theorem FloatLib.Floats.Formats.Flocq.round_eq_floor_or_ceil {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) : round rnd x = round floorRound x ∨ round rnd x = round ceilRound x

Every valid generic rounding chooses either directed-down or directed-up rounding.