Cohort preservation and preferred-exponent bounds

Removing trailing zeros preserves the exact rational value and sign. The algorithm stops either at its exponent limit or at a coefficient with no trailing zero, so it never discards a significant decimal digit.

theorem FloatLib.Floats.Formats.DecimalInterchange.stripTrailing_count_le (fuel c : ℕ) : (stripTrailing fuel c).2 ≤ fuel

theorem FloatLib.Floats.Formats.DecimalInterchange.stripTrailing_value (fuel c : ℕ) : c = (stripTrailing fuel c).1 * 10 ^ (stripTrailing fuel c).2

Exact integer decomposition, including zero.

theorem FloatLib.Floats.Formats.DecimalInterchange.stripTrailing_coefficient_le (fuel c : ℕ) : (stripTrailing fuel c).1 ≤ c

The adjusted coefficient never exceeds the original one.

theorem FloatLib.Floats.Formats.DecimalInterchange.stripTrailing_stopped (fuel c : ℕ) : (stripTrailing fuel c).2 = fuel ∨ (stripTrailing fuel c).1 % 10 ≠ 0

Stopping before the requested quantum means that no further exact decimal shift is possible.

theorem FloatLib.Floats.Formats.DecimalInterchange.preferredCohort_sameCohort (f : Format) (s : Bool) (c : ℕ) (q preferred : ℤ) : (Datum.finite s c q).SameCohort (preferredCohort f s c q preferred)

Cohort adjustment preserves the exact coefficient-times-quantum value and sign.

theorem FloatLib.Floats.Formats.DecimalInterchange.preferredCohort_toRat? (f : Format) (s : Bool) (c : ℕ) (q preferred : ℤ) : (preferredCohort f s c q preferred).toRat? = some ((if s = true then -1 else 1) * ↑c * 10 ^ q)

The selected cohort has exactly the original signed rational value.

theorem FloatLib.Floats.Formats.DecimalInterchange.preferredCohort_valid (f : Format) (s : Bool) (c : ℕ) (q preferred : ℤ) (h : Datum.Valid f (Datum.finite s c q)) : Datum.Valid f (preferredCohort f s c q preferred)

Cohort adjustment keeps a representable finite datum in the same format.