Cohort identities, including signed zero and decimal rescaling

Moving a trailing decimal zero into the quantum exponent preserves the cohort. Zero's cohort depends on its sign but not its quantum; infinities have singleton cohorts, and NaNs belong to no cohort.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameCohort_shift (s : Bool) (c : ℕ) (q : ℤ) : (finite s (10 * c) q).SameCohort (finite s c (q + 1))

Moving a trailing decimal zero into the quantum exponent preserves the cohort. Representability at a particular width is a separate condition on each datum.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameCohort_zero_iff (s t : Bool) (q r : ℤ) : (finite s 0 q).SameCohort (finite t 0 r) ↔ s = t

Zero's quantum exponent does not change its cohort, but its sign does.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.not_sameCohort_opposite_zeros (q r : ℤ) : ¬(finite false 0 q).SameCohort (finite true 0 r)

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.toRat?_eq_of_sameCohort {s t : Bool} {c d : ℕ} {q r : ℤ} (h : (finite s c q).SameCohort (finite t d r)) : (finite s c q).toRat? = (finite t d r).toRat?

Equal finite cohorts have equal exact rational values. The converse also needs the sign of zero, which the rational value alone cannot retain.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameCohort_infinity_iff (s : Bool) (d : Datum) : (infinity s).SameCohort d ↔ d = infinity s

Each infinity has exactly one datum in its cohort.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.not_sameCohort_nan (s signaling : Bool) (p : ℕ) (d : Datum) : ¬(nan s signaling p).SameCohort d

Cohorts contain floating-point numbers, which exclude NaNs (IEEE 754-2019 §2.1).