Decimal format conversion guarantees

The numerical statements concern the returned datum for every destination descriptor. Nonoverflowing nearest conversion has at most half a decimal grid unit of error; directed conversion encloses the input on the required side. Representable finite inputs retain their exact value and raise no exception.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.project_signed_magnitude (f : Format) (mode : RoundingMode) (s : Bool) (x : ℚ) (hx : 0 ≤ x) (preferred : ℤ) : project f mode (if s = true then -x else x) preferred s = projectMagnitude f mode s x preferred

Projection preserves an explicit sign when the input is presented as a magnitude.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_finite (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) : convertFormat f mode (Datum.finite s c q) = projectMagnitude f mode s (↑c * 10 ^ q) q

Finite conversion uses the supplied sign and the exact nonnegative decimal magnitude.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_valid (f : Format) (mode : RoundingMode) (x : Datum) : Datum.Valid f (convertFormat f mode x).value

Every conversion produces a valid destination datum, even from an unrestricted datum.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_infinity (f : Format) (mode : RoundingMode) (s : Bool) : convertFormat f mode (Datum.infinity s) = { value := Datum.infinity s }

Infinity retains its sign and raises no exception.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_nan (f : Format) (mode : RoundingMode) (s signaling : Bool) (p : ℕ) : convertFormat f mode (Datum.nan s signaling p) = { value := Datum.nan s false (if p < f.payloadBound then p else 0), status := { invalid := signaling } }

NaN conversion preserves a fitting payload, quiets the NaN, and reports its signaling bit.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_zero (f : Format) (mode : RoundingMode) (s : Bool) (q : ℤ) : convertFormat f mode (Datum.finite s 0 q) = { value := Datum.finite s 0 (max f.minQuantum (min q f.maxQuantum)) }

Signed zero keeps its sign and clamps its source quantum to the destination interval.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_exact (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (h : Datum.Valid f (Datum.finite s c q)) : (convertFormat f mode (Datum.finite s c q)).value.toRat? = (Datum.finite s c q).toRat?

A finite input already representable in the destination retains its exact numerical value.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_exact_status (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (h : Datum.Valid f (Datum.finite s c q)) : (convertFormat f mode (Datum.finite s c q)).status = { }

Changing destination width or cohort cannot raise a flag on an exactly representable input.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_exact_of_representable (f : Format) (mode : RoundingMode) (s : Bool) (c d : ℕ) (q r : ℤ) (hd : Datum.Valid f (Datum.finite s d r)) (hvalue : ↑c * 10 ^ q = ↑d * 10 ^ r) : (convertFormat f mode (Datum.finite s c q)).value.toRat? = (Datum.finite s d r).toRat?

A source cohort need not itself fit the destination: any valid destination representation of the same magnitude makes the conversion exact.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_exact_status_of_representable (f : Format) (mode : RoundingMode) (s : Bool) (c d : ℕ) (q r : ℤ) (hd : Datum.Valid f (Datum.finite s d r)) (hvalue : ↑c * 10 ^ q = ↑d * 10 ^ r) : (convertFormat f mode (Datum.finite s c q)).status = { }

A representable exact value raises no flags even if its source coefficient or quantum must change to fit the destination.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_quantum_closest (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (h : Datum.Valid f (Datum.finite s c q)) (d : ℕ) (r : ℤ) (hout : (convertFormat f mode (Datum.finite s c q)).value = Datum.finite s d r) (e : ℕ) (t : ℤ) (he : Datum.Valid f (Datum.finite s e t)) (hvalue : ↑c * 10 ^ q = ↑e * 10 ^ t) : |q - r| ≤ |q - t|

Exact conversion selects the quantum closest to the source quantum over the entire cohort.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_quantum_closest_of_representable (f : Format) (mode : RoundingMode) (s : Bool) (c d : ℕ) (q r : ℤ) (hd : Datum.Valid f (Datum.finite s d r)) (hvalue : ↑c * 10 ^ q = ↑d * 10 ^ r) (e : ℕ) (t : ℤ) (hout : (convertFormat f mode (Datum.finite s c q)).value = Datum.finite s e t) (a : ℕ) (b : ℤ) (ha : Datum.Valid f (Datum.finite s a b)) (heq : ↑c * 10 ^ q = ↑a * 10 ^ b) : |q - t| ≤ |q - b|

Across different source and destination widths, exact conversion selects a destination cohort member whose quantum is closest to the source quantum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_error_le_half (f : Format) (mode : RoundingMode) (hm : mode = RoundingMode.nearestEven ∨ mode = RoundingMode.nearestAway) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (convertFormat f mode x).status.overflow = false) : ∃ (value : ℚ), (convertFormat f mode x).value.toRat? = some value ∧ |value - a| ≤ 10 ^ roundingQuantum f |a| / 2

Both nearest directions bound the actual conversion error by half the selected grid unit.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_error_lt_one (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (convertFormat f mode x).status.overflow = false) : ∃ (value : ℚ), (convertFormat f mode x).value.toRat? = some value ∧ |value - a| < 10 ^ roundingQuantum f |a|

All five directions keep a nonoverflowing conversion within one selected grid unit.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.le_convertFormat_towardPositive (f : Format) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (convertFormat f RoundingMode.towardPositive x).status.overflow = false) : ∃ (value : ℚ), (convertFormat f RoundingMode.towardPositive x).value.toRat? = some value ∧ a ≤ value

Upward conversion encloses the input from above whenever it does not overflow.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_towardNegative_le (f : Format) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (convertFormat f RoundingMode.towardNegative x).status.overflow = false) : ∃ (value : ℚ), (convertFormat f RoundingMode.towardNegative x).value.toRat? = some value ∧ value ≤ a

Downward conversion encloses the input from below whenever it does not overflow.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_inexact_iff (f : Format) (mode : RoundingMode) (x : Datum) (a value : ℚ) (hx : x.toRat? = some a) (hfinite : (convertFormat f mode x).status.overflow = false) (hv : (convertFormat f mode x).value.toRat? = some value) : (convertFormat f mode x).status.inexact = true ↔ value ≠ a

Finite nonoverflowing conversion raises inexact exactly when the numerical value changes.

theorem FloatLib.Floats.Formats.DecimalInterchange.Conversion.convertFormat_underflow_iff (f : Format) (mode : RoundingMode) (x : Datum) (a : ℚ) (hx : x.toRat? = some a) (hfinite : (convertFormat f mode x).status.overflow = false) : (convertFormat f mode x).status.underflow = true ↔ |a| < f.minNormal ∧ (convertFormat f mode x).status.inexact = true

Decimal underflow uses the exact input magnitude and requires inexactness.