Order of positive Posit encodings

Regime order and exponent/fraction-tail order imply that unsigned codes below the sign mask are strictly ordered by their exact rational meanings. Crossing a variable-length regime boundary changes how many bits remain for exponent and fraction, so ordinary fixed-field lexicographic reasoning is not enough.

The theorem justifies native unsigned comparison for positive finite posits and supports the signed order development without decoding both operands again.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt_zero (format : Format) : nonnegativeRatAt format 0 = 0

The exact rational lookup maps the zero code to rational zero.

theorem FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt_eq_trailingRat_mul_regime (format : Format) {code : ℕ} (hpos : 0 < code) (hcode : code < format.signMaskNat) : nonnegativeRatAt format code = trailingRat (ofNatBits code).trailingBits code * 2 ^ ((ofNatBits code).regimeValue * 4)

A positive code below the sign mask denotes its exponent/fraction tail scaled by the regime power.

The exponent factor 4 is the Posit Standard (2022)'s regime step 2 ^ exponentBits.

theorem FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt_nextPrecision_two_mul (format : Format) {code : ℕ} (hcode : code < format.signMaskNat) : nonnegativeRatAt format.nextPrecision (2 * code) = nonnegativeRatAt format code

Appending a zero low bit while increasing the posit width preserves the exact finite value.

This is the even half of the standard's (n + 1)-bit rounding construction: an n-bit code U is embedded as U0, while the adjacent boundary is U1. The theorem holds for every valid static width, including the zero code.

theorem FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt_lt_of_regimeValue_eq (format : Format) {left right : ℕ} (hleftPos : 0 < left) (hlt : left < right) (hright : right < format.signMaskNat) (hregime : (ofNatBits left).regimeValue = (ofNatBits right).regimeValue) : nonnegativeRatAt format left < nonnegativeRatAt format right

Within one regime block, increasing a positive unsigned code strictly increases its exact value.

Division by the trailing-field modulus yields equal regime prefixes; taking remainders removes them. Code order is then exactly order of the bounded exponent/fraction remainder, whose rational interpretation is strictly monotone.

theorem FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt_pos (format : Format) {code : ℕ} (hpos : 0 < code) (hcode : code < format.signMaskNat) : 0 < nonnegativeRatAt format code

Every positive unsigned code below the sign mask denotes a strictly positive rational.

theorem FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt_lt_of_regimeValue_lt (format : Format) {left right : ℕ} (hleftPos : 0 < left) (hlt : left < right) (hright : right < format.signMaskNat) (hregime : (ofNatBits left).regimeValue < (ofNatBits right).regimeValue) : nonnegativeRatAt format left < nonnegativeRatAt format right

Strictly increasing regime values strictly separate the corresponding positive codes.

theorem FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt_lt_of_lt (format : Format) {left right : ℕ} (hlt : left < right) (hright : right < format.signMaskNat) : nonnegativeRatAt format left < nonnegativeRatAt format right

Unsigned posit codes below the sign mask are strictly ordered by their exact rational meanings.

This is the width-independent ordering theorem used by bisection, rounding, comparison, and every certified execution backend.

theorem FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt_strictMonoOn (format : Format) : StrictMonoOn (nonnegativeRatAt format) (Set.Iio format.signMaskNat)

Exact rational lookup is strictly monotone on the complete nonnegative finite code interval.

theorem FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt_le_iff (format : Format) {left right : ℕ} (hleft : left < format.signMaskNat) (hright : right < format.signMaskNat) : nonnegativeRatAt format left ≤ nonnegativeRatAt format right ↔ left ≤ right

On nonnegative finite codes, rational-value comparison is exactly unsigned-code comparison.

theorem FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt_injOn (format : Format) : Set.InjOn (nonnegativeRatAt format) (Set.Iio format.signMaskNat)

Equality of exact nonnegative finite values is equality of their unsigned posit codes.