Preferred cohorts of exact decimal results

For every representable exact magnitude, projection selects the valid cohort member whose quantum exponent is closest to the requested preferred exponent. The conclusion compares the returned datum with every valid representation of that magnitude, including representations with a different coefficient.

theorem FloatLib.Floats.Formats.DecimalInterchange.roundedPair_quantum_minimal_of_exact (f : Format) (mode : RoundingMode) (s : Bool) (x : ℚ) (d : ℕ) (r : ℤ) (hd : d < f.coefficientBound) (hrmin : f.minQuantum ≤ r) (hrmax : r ≤ f.maxQuantum) (hvalue : x = ↑d * 10 ^ r) : (roundedPair f mode s x).2 ≤ r

Every representation of an exact magnitude is at or above its initial projection grid.

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

Exact projection chooses the exponent closest to the preferred exponent over the whole cohort.