TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.P3109.Arithmetic.Queries.Order

Integer indices for P3109 numerical order #

Excluding NaN, the encoded datum set is a consecutive interval of integers: negative magnitude codes receive negative indices, zero receives zero, and nonnegative codes keep their indices. The exact decoder preserves this order, including the infinite endpoints in extended formats. These indices allow adjacency arguments without enumerating a descriptor's code space.

source
def FloatLib.Floats.Formats.P3109.Format.orderIndex (format : Format) (bits : ℕ) :
ℤ

An integer index in numerical order; its value at the NaN code is not used.

Instances For
    source
    theorem FloatLib.Floats.Formats.P3109.Format.less_decodeNat_iff_orderIndex (format : Format) (left right : ℕ) (hleft : left < format.modulus) (hright : right < format.modulus) (hleftNan : left ≠ format.nanBits) (hrightNan : right ≠ format.nanBits) :
    Arithmetic.less (Arithmetic.toRat (format.decodeNat left)) (Arithmetic.toRat (format.decodeNat right)) = true ↔ format.orderIndex left < format.orderIndex right

    Exact decoded strict order is the integer-index order on every pair of non-NaN codes.