Integral-rounding contracts

The unbounded dyadic-to-integer kernel is related to the usual nearest-even, floor, ceiling, and truncation semantics. The floating-point wrapper then records exactly when fractional bits were discarded and exposes the exceptional branches.

For IEEE encodings with fmt.fracWidth ≤ fmt.maxNormalExponent, the selected integer is exactly representable. This condition holds for the IEEE interchange formats. On finite inputs, roundToIntegral then denotes the floor, ceiling, truncation, or nearest-even integer selected by the rounding direction, and roundToIntegralExactWithStatus reports no overflow.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_zero (mode : IEEERoundingMode) : roundDyadicToInt mode Numerics.Dyadic.zero = 0

Exact zero rounds to integer zero in every direction.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_nearestEven (value : Numerics.Dyadic) : roundDyadicToInt IEEERoundingMode.nearestEven value = Flocq.nearestEven value.toReal

Nearest-even integer rounding has its usual mathematical meaning, independently of the stored dyadic exponent or magnitude.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_towardPositiveInfinity (value : Numerics.Dyadic) : roundDyadicToInt IEEERoundingMode.towardPositiveInfinity value = ⌈value.toReal⌉

Rounding toward positive infinity computes the mathematical ceiling.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_towardNegativeInfinity (value : Numerics.Dyadic) : roundDyadicToInt IEEERoundingMode.towardNegativeInfinity value = ⌊value.toReal⌋

Rounding toward negative infinity computes the mathematical floor.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_towardZero (value : Numerics.Dyadic) : roundDyadicToInt IEEERoundingMode.towardZero value = if 0 ≤ value.toReal then ⌊value.toReal⌋ else ⌈value.toReal⌉

Rounding toward zero truncates the exact dyadic: nonnegative values use floor and negative values use ceiling.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsIntegral_ofNat (negative : Bool) (significand exponent : ℕ) : dyadicIsIntegral { negative := negative, significand := significand, exponent := Int.ofNat exponent } = true

A dyadic with a nonnegative exponent is already an integer.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsIntegral_zero (negative : Bool) (exponent : ℤ) : dyadicIsIntegral { negative := negative, significand := 0, exponent := exponent } = true

Dyadic zero is integral independently of its stored sign and exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.dyadicIsIntegral_iff (value : Numerics.Dyadic) : dyadicIsIntegral value = true ↔ match value.exponent with | Int.ofNat a => True | Int.negSucc shift => 2 ^ (shift + 1) ∣ value.significand

An exact dyadic is integral precisely when no negative binary exponent leaves a fractional bit.

For exponent -(shift + 1), this says that 2^(shift + 1) divides the significand. A nonnegative exponent is always integral.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegral_eq_value {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) : value.roundToIntegral mode = (value.roundToIntegralExactWithStatus mode).value

roundToIntegral is exactly the value component of its status-bearing operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegralExactWithStatus_of_finite {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) : value.roundToIntegralExactWithStatus mode = have coefficient := roundDyadicToInt mode exact; have rounded := if (coefficient == 0) = true then zero fmt exact.negative else roundDyadicWithRounding fmt mode (Numerics.Dyadic.ofScaledInt coefficient 0); have encodingStatus := dyadicRoundingStatus fmt mode (Numerics.Dyadic.ofScaledInt coefficient 0) rounded; { value := rounded, status := { overflow := encodingStatus.overflow, inexact := !dyadicIsIntegral exact } }

On finite input, roundToIntegralExactWithStatus rounds the exact dyadic to an unbounded integer, then encodes that integer in the selected direction. The status records discarded fractional bits and the encoder's overflow classification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegralExactWithStatus_inexact_iff {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) : (value.roundToIntegralExactWithStatus mode).status.inexact = true ↔ match exact.exponent with | Int.ofNat a => False | Int.negSucc shift => ¬2 ^ (shift + 1) ∣ exact.significand

On finite input, roundToIntegralExactWithStatus raises inexact exactly when a negative binary exponent leaves at least one fractional bit.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegralExactWithStatus_of_infinity {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) (negative : Bool) (hvalue : value.exactValue = ExactValue.infinity negative) : value.roundToIntegralExactWithStatus mode = { value := value, status := IEEEStatus.clear }

roundToIntegralExactWithStatus preserves either infinity and returns clear status.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegralExactWithStatus_of_nan {fmt : FloatFormat} (value : Model fmt) (mode : IEEERoundingMode) (negative signaling : Bool) (payload : ℕ) (hvalue : value.exactValue = ExactValue.nan negative signaling payload) : value.roundToIntegralExactWithStatus mode = { value := value.quietNaN, status := { invalid := signaling } }

roundToIntegralExactWithStatus quiets a NaN and raises invalid exactly when it was signaling.

Representability of the rounded integer

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.floor_le_roundDyadicToInt (mode : IEEERoundingMode) (value : Numerics.Dyadic) : ⌊value.toReal⌋ ≤ roundDyadicToInt mode value

Every rounding direction lands at or above the floor of the exact value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundDyadicToInt_le_ceil (mode : IEEERoundingMode) (value : Numerics.Dyadic) : roundDyadicToInt mode value ≤ ⌈value.toReal⌉

Every rounding direction lands at or below the ceiling of the exact value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.abs_roundDyadicToInt_le_two_pow_of_exponent_neg (mode : IEEERoundingMode) (value : Numerics.Dyadic) (fracWidth : ℕ) (hsig : value.significand < 2 ^ (fracWidth + 1)) (hexp : value.exponent < 0) : |roundDyadicToInt mode value| ≤ 2 ^ fracWidth

If the significand is below 2^(fracWidth + 1) and the binary exponent is negative, the rounded integer has magnitude at most 2^fracWidth.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Dyadic.toReal_ofScaledInt_zero (c : ℤ) : (Numerics.Dyadic.ofScaledInt c 0).toReal = ↑c

An integer placed at exponent zero denotes itself.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegralExactWithStatus_finite_exact {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (hvalue : value.exactValue = ExactValue.finite exact) : (value.roundToIntegral mode).isFinite = true ∧ (value.roundToIntegral mode).toReal = ↑(roundDyadicToInt mode exact) ∧ (value.roundToIntegralExactWithStatus mode).status.overflow = false

On a finite input of an IEEE format whose exponent range reaches the precision, the result represents the selected integer exactly and reports no overflow. Fractional input can still set inexact.

Every IEEE interchange format satisfies fmt.fracWidth ≤ fmt.maxNormalExponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.roundToIntegralExactWithStatus_overflow_eq_false {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (mode : IEEERoundingMode) (hfinite : value.isFinite = true) : (value.roundToIntegralExactWithStatus mode).status.overflow = false

Integral rounding of a finite IEEE value never overflows when fmt.fracWidth ≤ fmt.maxNormalExponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.isFinite_roundToIntegral {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (mode : IEEERoundingMode) (hfinite : value.isFinite = true) : (value.roundToIntegral mode).isFinite = true

Integral rounding of a finite IEEE value is finite when the exponent range reaches the precision.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (mode : IEEERoundingMode) (exact : Numerics.Dyadic) (hd : value.toDyadic? = some exact) : (value.roundToIntegral mode).toReal = ↑(roundDyadicToInt mode exact)

The real value of a finite integral rounding is the integer selected by roundDyadicToInt.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.exists_int_toReal_roundToIntegral {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (mode : IEEERoundingMode) (hfinite : value.isFinite = true) : ∃ (n : ℤ), (value.roundToIntegral mode).toReal = ↑n

The result of integral rounding is an integer.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral_towardNegativeInfinity {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (hfinite : value.isFinite = true) : (value.roundToIntegral IEEERoundingMode.towardNegativeInfinity).toReal = ↑⌊value.toReal⌋

Rounding toward negative infinity computes the floor of the real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral_towardPositiveInfinity {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (hfinite : value.isFinite = true) : (value.roundToIntegral IEEERoundingMode.towardPositiveInfinity).toReal = ↑⌈value.toReal⌉

Rounding toward positive infinity computes the ceiling of the real value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral_towardZero {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (hfinite : value.isFinite = true) : (value.roundToIntegral IEEERoundingMode.towardZero).toReal = if 0 ≤ value.toReal then ↑⌊value.toReal⌋ else ↑⌈value.toReal⌉

Rounding toward zero truncates the real value: floor when nonnegative, ceiling otherwise.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.toReal_roundToIntegral_nearestEven {fmt : FloatFormat} (hfmt : fmt.isIEEE = true) (hrange : ↑fmt.fracWidth ≤ fmt.maxNormalExponent) (value : Model fmt) (hfinite : value.isFinite = true) : value.roundToIntegral.toReal = ↑(Flocq.nearestEven value.toReal)

Rounding to nearest computes the nearest integer with ties to even, nearestEven from the Flocq theory. Mathlib's round resolves ties toward positive infinity.