Total ordering of decimal datums

IEEE 754-2019 §5.10 orders negative NaNs first, then negative infinity, negative finite values, positive finite values, positive infinity, and positive NaNs. Within the finite parts, numerical value precedes quantum; quantum order is reversed for negative datums, including negative zero.

For positive NaNs, signaling precedes quiet; this rule reverses for negative NaNs. §5.10(d)(5)(iii) leaves the remaining payload order implementation-defined. Here smaller payloads precede larger ones for positive NaNs, with the reverse order for negative NaNs.

The key is injective on complete datums. It orders canonical BID/DPD members after decoding; it deliberately cannot distinguish redundant encodings of the same datum. These predicates never signal invalid.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Datum.OrderKey : Type

Class, numerical value (or NaN kind), then signed quantum (or NaN payload).

def FloatLib.Floats.Formats.DecimalInterchange.Datum.orderKey : Datum → OrderKey

An exact lexicographic key implementing the distinctions required by §5.10.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrder (x y : Datum) : Bool

Non-signaling total order, distinguishing zero signs, cohort members and NaN metadata.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.totalOrderMag (x y : Datum) : Bool

Total order after clearing both signs, including NaN signs.