Ordered Posit exponent and fraction tails

The finite exponent/fraction tail is ordered independently of regime encoding, and its value determines the corresponding part of exact Posit decoding. Separating the trailing fields is useful because two positive posit words with the same regime should be compared without reopening the variable-length regime parser.

These lemmas form the local bridge used by the full code-order theorem: regime bits establish the coarse scale interval, while this module handles exact order inside that interval.

Ordered exponent/fraction tails

@[inline]

def FloatLib.Floats.Formats.Posit.Model.natToRat (value : ℕ) : ℚ

Exact rational injection of a natural field value.

theorem FloatLib.Floats.Formats.Posit.Model.natToRat_eq_cast (value : ℕ) : natToRat value = ↑value

The exact rational injection agrees with the natural-number cast.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.trailingRat (trailing raw : ℕ) : ℚ

Exact positive value contributed by trailing exponent/fraction bits before applying the regime.

The Posit Standard (2022) takes at most two exponent bits. When fewer are present, they are the high bits and omitted low exponent bits are restored as zero.

theorem FloatLib.Floats.Formats.Posit.Model.trailingRat_lt_of_lt {trailing left right : ℕ} (hleft : left < 2 ^ trailing) (hright : right < 2 ^ trailing) (hlt : left < right) : trailingRat trailing left < trailingRat trailing right

The exact exponent/fraction tail is strictly ordered by its bounded raw field.

theorem FloatLib.Floats.Formats.Posit.Model.trailingRat_mod_twoPow (trailing raw : ℕ) : trailingRat trailing (raw % 2 ^ trailing) = trailingRat trailing raw

Only the low trailing bits contribute to an exponent/fraction tail.

This is the modular form used when a complete posit magnitude is split into its regime prefix and remaining field.

theorem FloatLib.Floats.Formats.Posit.Model.trailingRat_succ_two_mul (trailing raw : ℕ) : trailingRat (trailing + 1) (2 * raw) = trailingRat trailing raw

Appending a zero bit to an exponent/fraction tail preserves its exact rational value.

For tails shorter than two bits this restores one more standard exponent bit as zero. Thereafter it appends a zero fraction bit, doubling both the explicit numerator and denominator.

theorem FloatLib.Floats.Formats.Posit.Model.trailingRat_bounds (trailing raw : ℕ) : 1 ≤ trailingRat trailing raw ∧ trailingRat trailing raw < 16

Every exponent/fraction tail of a Posit Standard (2022) word lies in [1, 16).

The constant 16 = 2 ^ 4 is the multiplicative change in value at each regime step. Adjacent regime blocks cannot overlap, independently of the total posit width.

theorem FloatLib.Floats.Formats.Posit.Model.decodeFields_toRat_eq_trailingRat_mul_regime {format : Format} (value : Model format) (hsign : value.signBit = false) : value.decodeFields.toRat = trailingRat value.trailingBits value.magnitudeBits * 2 ^ (value.regimeValue * Int.ofNat format.regimeExponentStep)

For decoded fields with a clear sign bit, the rational field value factors into the trailing field and a regime power. This describes field decoding; zero and NaR are handled separately by the complete decoder.