IEEE binary total ordering

Model.totalOrder orders complete exact values, retaining zero signs and NaN metadata. Finite values use the shared exponent-scalable exact dyadic comparator; the specification compares their exact rational denotations. Equal values are ordered by sign, then by exponent, reversed for negative values. Binary interchange has a unique representation of each nonzero finite value; the exponent rule also gives a consistent order on unnormalized dyadics.

IEEE 754-2019 §5.10 specifies the sign and signaling-class order of NaNs and leaves the remaining NaN order implementation-defined. FloatLib chooses increasing fraction payload for positive NaNs and decreasing fraction payload for negative NaNs. The complete fraction includes the quiet bit; class is compared first, so this convention is also increasing/decreasing trailing payload. Neither predicate quiets NaNs or produces exception indicators.

totalOrderMag clears signs in the complete exact data. For signed-zero formats this agrees with totalOrder after encoded absolute value, as required by §5.7.2 for IEEE formats. The exact operation also applies to unsigned-zero formats, whose reserved NaN word cannot have its sign bit cleared without changing its classification. Both APIs accept every descriptor; IEEE conformance claims apply to IEEE encodings.

References

• IEEE Standard for Floating-Point Arithmetic, IEEE Std 754-2019, §§5.7.2 and 5.10, DOI 10.1109/IEEESTD.2019.8766229.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.TotalOrderKey : Type

Lexicographic coordinates: value class, numerical value, sign or NaN class, and exponent or payload. Every coordinate has its ordinary mathematical order.

def FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.finiteTotalOrderKey (d : Numerics.Dyadic) : Lex (ℕ × ℤ)

Tie coordinates for finite values: negative signs first, then sign-directed exponents.

def FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrderKey : ExactValue → TotalOrderKey

Exact ordering coordinates. The five value classes are negative NaNs, negative infinity, finite numbers, positive infinity, and positive NaNs, in that order.

def FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrder : ExactValue → ExactValue → Bool

IEEE total order on exact representations, including the exponent of a finite dyadic. Finite comparison avoids shifts proportional to the exponent gap.

def FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.abs : ExactValue → ExactValue

Clear the sign while retaining the exponent, significand, and NaN class and payload.

def FloatLib.Floats.Formats.BinaryInterchange.Model.ExactValue.totalOrderMag (x y : ExactValue) : Bool

Total ordering of exact magnitudes; opposite signs with identical magnitudes are tied.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrder {fmt : FloatFormat} (x y : Model fmt) : Bool

IEEE 754-2019 total ordering, using exact numerical values and complete NaN metadata.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.totalOrderMag {fmt : FloatFormat} (x y : Model fmt) : Bool

IEEE magnitude ordering on complete exact data, generalized to every binary descriptor.