Closest preferred exponent

A higher-quantum member of a finite cohort differs by an exact power of ten in its integer coefficient. Consequently, a coefficient with no trailing zero cannot move to a higher quantum. Starting from the smallest representable quantum, preferredCohort therefore selects the exponent closest to the preferred one.

theorem FloatLib.Floats.Formats.DecimalInterchange.coefficient_eq_mul_of_quantum_le (c d : ℕ) {q r : ℤ} (hqr : q ≤ r) (hvalue : ↑c * 10 ^ q = ↑d * 10 ^ r) : c = d * 10 ^ (r - q).toNat

Equality of decimal values on nested grids gives an exact integer coefficient factor.

theorem FloatLib.Floats.Formats.DecimalInterchange.coefficient_mod_ten_eq_zero_of_quantum_lt (c d : ℕ) {q r : ℤ} (hqr : q < r) (hvalue : ↑c * 10 ^ q = ↑d * 10 ^ r) : c % 10 = 0

A higher exponent requires a trailing zero in the original coefficient.

theorem FloatLib.Floats.Formats.DecimalInterchange.preferredCohort_quantum_closest (f : Format) (c : ℕ) (q preferred : ℤ) (hq : q ≤ f.maxQuantum) (hminimal : ∀ (d : ℕ) (r : ℤ), d < f.coefficientBound → f.minQuantum ≤ r → r ≤ f.maxQuantum → ↑c * 10 ^ q = ↑d * 10 ^ r → q ≤ r) (d : ℕ) (r : ℤ) (hd : d < f.coefficientBound) (hrmin : f.minQuantum ≤ r) (hrmax : r ≤ f.maxQuantum) (hvalue : ↑c * 10 ^ q = ↑d * 10 ^ r) : |preferred - (q + ↑(stripTrailing (min preferred f.maxQuantum - q).toNat c).2)| ≤ |preferred - r|

Among coarser representable members, the chosen exponent is closest to the preferred one. The minimal-quantum premise is discharged for projection by its coefficient range theorem.

theorem FloatLib.Floats.Formats.DecimalInterchange.quantum_le_of_full_coefficient (f : Format) (c d : ℕ) (q r : ℤ) (hc : f.payloadBound ≤ c) (hd : d < f.coefficientBound) (hvalue : ↑c * 10 ^ q = ↑d * 10 ^ r) : q ≤ r

A coefficient with a full leading digit cannot be represented at a finer quantum. This statement compares equal numerical values; trailing zeros do not affect it.