Exactness on every representable decimal

These theorems cover every valid coefficient and quantum in any Format, in all five rounding directions. A change of representation within a cohort is not inexact: only a change in numerical value can raise that exception.

theorem FloatLib.Floats.Formats.DecimalInterchange.roundingQuantum_le_of_valid (f : Format) (s : Bool) (c : ℕ) (q : ℤ) (h : Datum.Valid f (Datum.finite s c q)) : roundingQuantum f (↑c * 10 ^ q) ≤ q

theorem FloatLib.Floats.Formats.DecimalInterchange.roundedPair_exact_value (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (h : Datum.Valid f (Datum.finite s c q)) : ↑(roundedPair f mode s (↑c * 10 ^ q)).1 * 10 ^ (roundedPair f mode s (↑c * 10 ^ q)).2 = ↑c * 10 ^ q

A valid decimal's exact value is fixed, even when another member of its cohort is selected.

theorem FloatLib.Floats.Formats.DecimalInterchange.roundedPair_quantum_le_of_valid (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q : ℤ) (h : Datum.Valid f (Datum.finite s c q)) : (roundedPair f mode s (↑c * 10 ^ q)).2 ≤ q

An exact representable input cannot cause an exponent carry beyond its original exponent.

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_status_of_exact (f : Format) (mode : RoundingMode) (s : Bool) (x : ℚ) (preferred : ℤ) (hq : (roundedPair f mode s x).2 ≤ f.maxQuantum) (hx : ↑(roundedPair f mode s x).1 * 10 ^ (roundedPair f mode s x).2 = x) : (projectMagnitude f mode s x preferred).status = { }

Exact finite projection raises none of the five default exception flags.

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_exact (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q preferred : ℤ) (h : Datum.Valid f (Datum.finite s c q)) : (projectMagnitude f mode s (↑c * 10 ^ q) preferred).value.toRat? = (Datum.finite s c q).toRat?

Every valid finite decimal projects with its exact numerical value.

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_exact_status (f : Format) (mode : RoundingMode) (s : Bool) (c : ℕ) (q preferred : ℤ) (h : Datum.Valid f (Datum.finite s c q)) : (projectMagnitude f mode s (↑c * 10 ^ q) preferred).status = { }

Cohort selection, including zero, never raises inexact on a representable input.