Least-quantum cohorts of inexact projections

IEEE 754-2019 §5.2 selects the smallest available quantum for inexact results. The coefficient is either on the subnormal grid or has a full leading digit; therefore no equal valid value can have a smaller quantum. This includes finite results delivered on directed overflow.

theorem FloatLib.Floats.Formats.DecimalInterchange.roundedPair_minimum_or_full (f : Format) (mode : RoundingMode) (s : Bool) {x : ℚ} (hx : 0 ≤ x) : (roundedPair f mode s x).2 = f.minQuantum ∨ f.payloadBound ≤ (roundedPair f mode s x).1

theorem FloatLib.Floats.Formats.DecimalInterchange.roundedPair_quantum_minimal (f : Format) (mode : RoundingMode) (s : Bool) {x : ℚ} (hx : 0 ≤ x) (d : ℕ) (r : ℤ) (hd : d < f.coefficientBound) (hr : f.minQuantum ≤ r) (hvalue : ↑(roundedPair f mode s x).1 * 10 ^ (roundedPair f mode s x).2 = ↑d * 10 ^ r) : (roundedPair f mode s x).2 ≤ r

theorem FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_inexact_quantum_minimal (f : Format) (mode : RoundingMode) (s : Bool) {x : ℚ} (hx : 0 ≤ x) (preferred : ℤ) (hinexact : (projectMagnitude f mode s x preferred).status.inexact = true) (c : ℕ) (q : ℤ) (hout : (projectMagnitude f mode s x preferred).value = Datum.finite s c q) (d : ℕ) (r : ℤ) (hv : Datum.Valid f (Datum.finite s d r)) (hvalue : ↑c * 10 ^ q = ↑d * 10 ^ r) : q ≤ r

Every finite inexact result uses the least quantum in its valid cohort.