Decimal datums and cohorts

A finite datum stores a sign, an integer coefficient, and a quantum exponent: its value is (-1)^sign * coefficient * 10^quantum. Trailing coefficient zeros are meaningful representation information. For example, 1 × 10^0 and 10 × 10^-1 are different datums in the same cohort.

This representation layer implements IEEE 754-2019 §§3.3 and 3.5. It supplies neither decimal arithmetic nor its rounding, preferred-exponent, or exception rules.

inductive FloatLib.Floats.Formats.DecimalInterchange.Datum : Type

A decimal datum before selecting an interchange width. signaling = true represents a signaling NaN.

• finite (negative : Bool) (coefficient : ℕ) (quantum : ℤ) : Datum
• infinity (negative : Bool) : Datum
• nan (negative signaling : Bool) (payload : ℕ) : Datum

def FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqDatum.decEq (x✝ x✝¹ : Datum) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqDatum : DecidableEq Datum

def FloatLib.Floats.Formats.DecimalInterchange.instReprDatum.repr : Datum → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.instReprDatum : Repr Datum

def FloatLib.Floats.Formats.DecimalInterchange.Datum.Valid (f : Format) : Datum → Prop

Representability at the selected precision and quantum range. NaN payloads have one fewer decimal digit than finite coefficients.

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.Datum.instDecidableValid (f : Format) (d : Datum) : Decidable (Valid f d)

def FloatLib.Floats.Formats.DecimalInterchange.Datum.toRat? : Datum → Option ℚ

The exact rational value of a finite datum; infinities and NaNs have no rational value. Signed zeros remain distinct datums even though both map to zero. Zero bypasses the radix power, so its quantum does not determine the size of an intermediate integer.

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.toRat?_eq (d : Datum) : d.toRat? = match d with | finite s c q => some ((if s = true then -1 else 1) * ↑c * 10 ^ q) | infinity negative => none | nan negative signaling payload => none

The zero shortcut preserves the usual coefficient-times-radix-power interpretation.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.SameCohort : Datum → Datum → Prop

IEEE 754-2019 §§2.1 and 3.5.1 cohorts preserve the sign, including the sign of zero. Each infinity forms a singleton cohort. NaNs have no cohort. Width-specific cohorts restrict this relation to datums satisfying Valid.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.ofBiased (f : Format) (s : Bool) (c e : ℕ) : Datum

Biased exponent reconstructed by either decoder.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.ofBiased_valid (f : Format) (s : Bool) (c e : ℕ) : Valid f (ofBiased f s c e) ↔ c < f.coefficientBound ∧ e < f.exponentBound

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.valid_quantum_iff (f : Format) (s : Bool) (c : ℕ) (q : ℤ) : Valid f (finite s c q) ↔ c < f.coefficientBound ∧ f.minQuantum ≤ q ∧ q ≤ f.maxQuantum

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameCohort_symm {a b : Datum} (h : a.SameCohort b) : b.SameCohort a

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.sameCohort_trans {a b c : Datum} (hab : a.SameCohort b) (hbc : b.SameCohort c) : a.SameCohort c