Positive directed rounding for arbitrary executable float formats

The shift-based directed rounders used by Model are related to the independent Flocq-style real semantics at the scaled-mantissa boundary, before subnormal and normal values are packed into interchange fields.

roundAt fmt x mode is the real rounding of every IEEERoundingMode on the same grid, Flocq's round with nearestEven, ceilRound, and floorRound for nearest-even and the two infinity directions. Nearest-away rounding is Flocq's nearestChoice with the tie choice nearestAwayChoice, and rounding away from zero is awayRound.

All definitions are uniform in FloatFormat.

Real rounding in every direction

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_nearestAway (fmt : FloatFormat) (x : ℝ) : roundAt fmt x IEEERoundingMode.nearestAway = Flocq.round (Flocq.nearestChoice Flocq.nearestAwayChoice) x

Nearest-away rounding rounds the scaled mantissa with ties away from zero.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_towardZero (fmt : FloatFormat) (x : ℝ) : roundAt fmt x IEEERoundingMode.towardZero = Flocq.round Flocq.truncRound x

Rounding toward zero truncates the scaled mantissa.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_away (fmt : FloatFormat) (x : ℝ) : roundAt fmt x IEEERoundingMode.away = Flocq.round Flocq.awayRound x

Rounding away from zero rounds the scaled mantissa away from zero.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.genericFormat_roundAt (fmt : FloatFormat) (x : ℝ) (mode : IEEERoundingMode := IEEERoundingMode.nearest) : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) (roundAt fmt x mode)

Every rounding direction returns a value on the grid of fmt.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_of_genericFormat (fmt : FloatFormat) {x : ℝ} (hx : Flocq.genericFormat Numerics.binaryRadix (fexpOf fmt) x) (mode : IEEERoundingMode := IEEERoundingMode.nearest) : roundAt fmt x mode = x

Every rounding direction fixes a value already on the grid of fmt.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_of_nonneg (fmt : FloatFormat) {mode : IEEERoundingMode} (hnearest : mode ≠ IEEERoundingMode.nearest) (hnearestAway : mode ≠ IEEERoundingMode.nearestAway) {x : ℝ} (hx : 0 ≤ x) : roundAt fmt x mode = if mode.roundsAwayFromZero false = true then roundAt fmt x IEEERoundingMode.up else roundAt fmt x IEEERoundingMode.down

On a nonnegative real a directed mode is upward rounding when it rounds positive results away from zero, and downward rounding otherwise. The two nearest modes are not directed.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundAt_eq_of_scaledBracket (fmt : FloatFormat) (mode : IEEERoundingMode) {x y : ℝ} {m : ℤ} {location : Flocq.Location} (hcexp : Flocq.cexp Numerics.binaryRadix (fexpOf fmt) x = Flocq.cexp Numerics.binaryRadix (fexpOf fmt) y) (hx : Flocq.InbetweenInt m (Flocq.scaledMantissa Numerics.binaryRadix (fexpOf fmt) x) location) (hy : Flocq.InbetweenInt m (Flocq.scaledMantissa Numerics.binaryRadix (fexpOf fmt) y) location) : roundAt fmt x mode = roundAt fmt y mode

Two reals with the same canonical exponent whose scaled mantissas have the same integer bracket and the same location in it round alike in every direction.

Executable scaled-mantissa rounding

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaAtExponentDown (mantissa : ℕ) (exponent targetExponent : ℤ) : ℕ

Floor a natural mantissa after expressing it at targetExponent.

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaAtExponentUp (mantissa : ℕ) (exponent targetExponent : ℤ) : ℕ

Ceil a natural mantissa after expressing it at targetExponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaAtExponentUp_ne_zero (mantissa : ℕ) (exponent targetExponent : ℤ) (hm : mantissa ≠ 0) : roundMantissaAtExponentUp mantissa exponent targetExponent ≠ 0

Ceiling alignment preserves nonzeroness of a positive mantissa.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaAtExponentDown_le_up (mantissa : ℕ) (exponent targetExponent : ℤ) : roundMantissaAtExponentDown mantissa exponent targetExponent ≤ roundMantissaAtExponentUp mantissa exponent targetExponent

Floor alignment never exceeds ceiling alignment at the same exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaAtExponentUp_le_down_add_one (mantissa : ℕ) (exponent targetExponent : ℤ) : roundMantissaAtExponentUp mantissa exponent targetExponent ≤ roundMantissaAtExponentDown mantissa exponent targetExponent + 1

Ceiling alignment is at most one unit above floor alignment.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floor_scaledMagnitude (mantissa : ℕ) (exponent targetExponent : ℤ) : Flocq.floorRound (↑mantissa * Flocq.bpow Numerics.binaryRadix (exponent - targetExponent)) = Int.ofNat (roundMantissaAtExponentDown mantissa exponent targetExponent)

Downward shifting computes the integer floor of a scaled positive dyadic.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.ceil_scaledMagnitude (mantissa : ℕ) (exponent targetExponent : ℤ) : Flocq.ceilRound (↑mantissa * Flocq.bpow Numerics.binaryRadix (exponent - targetExponent)) = Int.ofNat (roundMantissaAtExponentUp mantissa exponent targetExponent)

Upward shifting computes the integer ceiling of a scaled positive dyadic.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundMantissaAtExponentDown_mul_bpow_le (mantissa : ℕ) (exponent targetExponent : ℤ) : ↑(roundMantissaAtExponentDown mantissa exponent targetExponent) * bpow targetExponent ≤ ↑mantissa * bpow exponent

Floor alignment at any target exponent is a lower bound for the exact dyadic magnitude.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.le_roundMantissaAtExponentUp_mul_bpow (mantissa : ℕ) (exponent targetExponent : ℤ) : ↑mantissa * bpow exponent ≤ ↑(roundMantissaAtExponentUp mantissa exponent targetExponent) * bpow targetExponent

Ceiling alignment at any target exponent is an upper bound for the exact dyadic magnitude.