Rounding Into A Generic Format

Rounding any real with a valid integer-rounding rule produces a value in the selected generic format. The proof separates inputs whose magnitude is at most the selected exponent from those above it.

Negative inputs reduce to positive ones through round_neg, which conjugates the integer rule by negation. Conjugation exchanges floor and ceiling and fixes truncation.

theorem FloatLib.Floats.Formats.Flocq.validExp_small {fexp : ℤ → ℤ} [ValidExp fexp] {e : ℤ} (h : e ≤ fexp e) : fexp (fexp e + 1) ≤ fexp e

The Valid_exp consequence used when the input magnitude is at most the selected exponent.

theorem FloatLib.Floats.Formats.Flocq.validExp_large {fexp : ℤ → ℤ} [ValidExp fexp] {e : ℤ} (h : fexp e < e) : fexp (e + 1) ≤ e

The Valid_exp consequence used when the selected exponent is below the input magnitude.

theorem FloatLib.Floats.Formats.Flocq.round_pos_small_cases {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) (hx : 0 < x) (hsmall : magnitude β x ≤ fexp (magnitude β x)) : round rnd x = 0 ∨ round rnd x = bpow β (fexp (magnitude β x))

Positive inputs in the small-magnitude regime round either to zero or to one radix power.

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

Rounding in the small-magnitude regime produces a generic-format value.

theorem FloatLib.Floats.Formats.Flocq.round_pos_large_bounds_and_generic {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) (hx : 0 < x) (hlarge : fexp (magnitude β x) < magnitude β x) : (bpow β (magnitude β x - 1) ≤ round rnd x ∧ round rnd x ≤ bpow β (magnitude β x)) ∧ genericFormat β fexp (round rnd x)

In the large-magnitude regime, the rounded value lies between the endpoints of the input magnitude bin, including the upper endpoint, and belongs to the generic format.

theorem FloatLib.Floats.Formats.Flocq.generic_format_round_pos_large {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) [ValidRnd rnd] (x : ℝ) (hx : 0 < x) (hlarge : fexp (magnitude β x) < magnitude β x) : genericFormat β fexp (round rnd x)

Rounding in the large-magnitude regime produces a generic-format value.

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

Every positive real rounds into the selected generic format.

def FloatLib.Floats.Formats.Flocq.negRound (rnd : ℝ → ℤ) : ℝ → ℤ

Conjugate a rounding rule by negation.

instance FloatLib.Floats.Formats.Flocq.negRoundValid (rnd : ℝ → ℤ) [ValidRnd rnd] : ValidRnd (negRound rnd)

theorem FloatLib.Floats.Formats.Flocq.round_neg {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (x : ℝ) : round rnd (-x) = -round (negRound rnd) x

Rounding a negated input is negated rounding with the conjugate integer rule.

theorem FloatLib.Floats.Formats.Flocq.negRound_floorRound : negRound floorRound = ceilRound

Conjugating floor by negation gives ceiling.

theorem FloatLib.Floats.Formats.Flocq.negRound_ceilRound : negRound ceilRound = floorRound

Conjugating ceiling by negation gives floor.

theorem FloatLib.Floats.Formats.Flocq.negRound_truncRound : negRound truncRound = truncRound

Toward-zero integer rounding commutes with negation.

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

Rounding any real produces a value in the selected generic format.