Integral result, preferred quantum, and status guarantees

When the format's maximum quantum is nonnegative, every valid finite input produces a finite integer at the specified preferred quantum, with no intermediate precision loss or range exception. This includes all three standard presets. The general invalid characterization also covers custom layouts with a negative maximum quantum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.integral_coefficient_le (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) : mode.roundAt s (↑c * 10 ^ q) (max q 0) ≤ c

The coefficient of a rounded integral value never exceeds the input coefficient.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralExact_finite (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (hv : Datum.Valid f (Datum.finite s c q)) (hzero : 0 ≤ f.maxQuantum) : roundToIntegralExact f mode (Datum.finite s c q) = { value := Datum.finite s (mode.roundAt s (↑c * 10 ^ q) (max q 0)) (max q 0), status := { inexact := decide (↑(mode.roundAt s (↑c * 10 ^ q) (max q 0)) * 10 ^ max q 0 ≠ ↑c * 10 ^ q) } }

The successful output explicitly retains the sign and preferred quantum, including zero.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralExact_invalid_iff (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (hv : Datum.Valid f (Datum.finite s c q)) : (roundToIntegralExact f mode (Datum.finite s c q)).status.invalid = true ↔ f.maxQuantum < 0

For a valid finite input, invalid occurs exactly when the preferred integral quantum cannot be represented. The coefficient bound never causes this failure.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralExact_valid (f : Format) (mode : RoundingMode) (x : Datum) : Datum.Valid f (roundToIntegralExact f mode x).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegral_valid (f : Format) (mode : RoundingMode) (x : Datum) : Datum.Valid f (roundToIntegral f mode x).value

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralExact_integer (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (hv : Datum.Valid f (Datum.finite s c q)) (hzero : 0 ≤ f.maxQuantum) : ∃ (n : ℤ), (roundToIntegralExact f mode (Datum.finite s c q)).value.toRat? = some ↑n

A valid finite input rounds to an integer when the maximum quantum is nonnegative.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralExact_finite_flags (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (hv : Datum.Valid f (Datum.finite s c q)) (hzero : 0 ≤ f.maxQuantum) : (roundToIntegralExact f mode (Datum.finite s c q)).status.invalid = false ∧ (roundToIntegralExact f mode (Datum.finite s c q)).status.overflow = false ∧ (roundToIntegralExact f mode (Datum.finite s c q)).status.underflow = false ∧ (roundToIntegralExact f mode (Datum.finite s c q)).status.divideByZero = false

A valid finite input raises no range, domain, or divide-by-zero exception when the maximum quantum is nonnegative.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegral_inexact (f : Format) (mode : RoundingMode) (x : Datum) : (roundToIntegral f mode x).status.inexact = false

Explicit-direction integral rounding suppresses inexact, including for a nonintegral input.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralExact_inexact_iff (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (v : ℚ) (hv : (roundToIntegralExact f mode (Datum.finite s c q)).value.toRat? = some v) : (roundToIntegralExact f mode (Datum.finite s c q)).status.inexact = true ↔ v ≠ Datum.finiteValue s c q

Exact integral rounding signals inexact precisely for a numerical change.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralExact_of_nonneg_quantum (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (hv : Datum.Valid f (Datum.finite s c q)) (hq : 0 ≤ q) : roundToIntegralExact f mode (Datum.finite s c q) = { value := Datum.finite s c q }

Already nonnegative quantum exponents are preserved, including trailing coefficient zeros.

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegralExact_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (s : Bool) (c : ℕ) (q : ℤ) (hv : Datum.Valid f (Datum.finite s c q)) (hzero : 0 ≤ f.maxQuantum) : ∃ (value : ℚ), (roundToIntegralExact f mode (Datum.finite s c q)).value.toRat? = some value ∧ |value - Datum.finiteValue s c q| ≤ 1 / 2

Both nearest integral modes differ from the input by at most one half, independent of its cohort.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.roundToIntegral_value (f : Format) (mode : RoundingMode) (x : Datum) : (roundToIntegral f mode x).value = (roundToIntegralExact f mode x).value

The two integral variants have exactly the same numerical datum.