Fixed-width bit runs in positive Posit encodings

Representation lemmas describe bit runs in the nonnegative half of a Posit Standard encoding. Exact-width leading runs are reduced to Nat.log2; a run of one bits is reduced to the leading-zero run of the fixed-width complement using mathlib's BitVec complement theorems; and equal or ordered regime prefixes are related to the remaining encoded tail.

These facts are independent of the storage carrier. Tail-order and rounding proofs use them alongside native execution backends.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt (format : Format) (code : ℕ) : ℚ

Exact rational value of the posit word with unsigned code code.

Codes in [0, format.signMaskNat) are the nonnegative finite posits. The function is total on naturals: it first reduces the code modulo the format's modulus, then maps zero and NaR to zero and other words to their signed rational value.

theorem FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt_of_pos_lt_signMask (format : Format) {code : ℕ} (hpos : 0 < code) (hcode : code < format.signMaskNat) : nonnegativeRatAt format code = (ofNatBits code).decodeFields.toRat

A positive code below the sign mask takes the finite branch of exact posit decoding.

Fixed-width bit runs

theorem FloatLib.Floats.Formats.Posit.Model.countLeadingRun_false_eq_log2 (value width : ℕ) (hpos : 0 < value) (hlt : value < 2 ^ width) : countLeadingRun value width false = width - (value.log2 + 1)

For a positive value bounded by 2 ^ width, the leading-zero run is the width minus its binary length.

theorem FloatLib.Floats.Formats.Posit.Model.countLeadingRun_mod_twoPow (value width : ℕ) (bit : Bool) : countLeadingRun value width bit = countLeadingRun (value % 2 ^ width) width bit

A leading-run scan depends only on the low width bits being scanned.

theorem FloatLib.Floats.Formats.Posit.Model.countLeadingRun_true_eq_false_of_testBit_flip (left right width : ℕ) (hflip : ∀ index < width, right.testBit index = !left.testBit index) : countLeadingRun left width true = countLeadingRun right width false

Complementary bit streams have complementary leading runs.

theorem FloatLib.Floats.Formats.Posit.Model.countLeadingRun_true_eq_fixedComplement (value width : ℕ) (hvalue : value < 2 ^ width) : countLeadingRun value width true = countLeadingRun (2 ^ width - 1 - value) width false

A leading-one run is the leading-zero run of the complement inside the same fixed width.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.countLeadingRun_zero_false (width : ℕ) : countLeadingRun 0 width false = width

The all-zero word has a zero-bit run occupying the complete inspected width.

theorem FloatLib.Floats.Formats.Posit.Model.countLeadingRun_false_anti {left right width : ℕ} (hle : left ≤ right) (hright : right < 2 ^ width) : countLeadingRun right width false ≤ countLeadingRun left width false

Within a fixed width, increasing an unsigned word can only shorten its leading-zero run.

theorem FloatLib.Floats.Formats.Posit.Model.countLeadingRun_true_mono {left right width : ℕ} (hle : left ≤ right) (hright : right < 2 ^ width) : countLeadingRun left width true ≤ countLeadingRun right width true

Within a fixed width, increasing an unsigned word can only lengthen its leading-one run.

theorem FloatLib.Floats.Formats.Posit.Model.countLeadingRun_two_mul {value width : ℕ} (hpos : 0 < value) (hbound : value < 2 ^ width) : countLeadingRun (2 * value) (width + 1) ((2 * value).testBit width) = countLeadingRun value width (value.testBit (width - 1))

Appending a low zero bit to a positive bounded word preserves its leading regime run.

For the all-ones word the appended zero becomes the first terminator, and the run length is again unchanged.

theorem FloatLib.Floats.Formats.Posit.Model.regimeBit_ofNatBits (format : Format) {code : ℕ} (hcode : code < format.signMaskNat) : (ofNatBits code).regimeBit = code.testBit (format.payloadBits - 1)

The regime bit of a nonnegative code is the top bit of its payload.

theorem FloatLib.Floats.Formats.Posit.Model.regimeBit_ofNatBits_eq_true_iff (format : Format) {code : ℕ} (hcode : code < format.signMaskNat) : (ofNatBits code).regimeBit = true ↔ format.oneCodeNat ≤ code

The regime bit of a nonnegative code is set exactly when the code is at least the code of one.

theorem FloatLib.Floats.Formats.Posit.Model.regimeRunLength_ofNatBits (format : Format) {code : ℕ} (hcode : code < format.signMaskNat) : (ofNatBits code).regimeRunLength = countLeadingRun code format.payloadBits (code.testBit (format.payloadBits - 1))

The regime run of a nonnegative code is the leading run of its top payload bit.

theorem FloatLib.Floats.Formats.Posit.Model.regimeValue_ofNatBits_le_of_le (format : Format) {left right : ℕ} (hle : left ≤ right) (hright : right < format.signMaskNat) : (ofNatBits left).regimeValue ≤ (ofNatBits right).regimeValue

Unsigned code order below the sign mask induces nondecreasing signed regime values.

Below the code of one, leading-zero runs shorten as codes rise; at and above it, leading-one runs lengthen.

theorem FloatLib.Floats.Formats.Posit.Model.regimeValue_eq_iff {format : Format} (left right : Model format) : left.regimeValue = right.regimeValue ↔ left.regimeBit = right.regimeBit ∧ left.regimeRunLength = right.regimeRunLength

Two decoded words have the same regime value exactly when both the regime bit and run length agree.

The positivity of every regime run separates the negative zero-run regimes from the nonnegative one-run regimes.

theorem FloatLib.Floats.Formats.Posit.Model.trailingBits_eq_and_prefix_eq_of_regimeValue_eq {format : Format} (left right : Model format) (hleftBound : left.magnitudeBits < 2 ^ format.payloadBits) (hrightBound : right.magnitudeBits < 2 ^ format.payloadBits) (hregime : left.regimeValue = right.regimeValue) : left.trailingBits = right.trailingBits ∧ left.magnitudeBits / 2 ^ left.trailingBits = right.magnitudeBits / 2 ^ right.trailingBits

Equal regimes have equal trailing widths and equal high-bit prefixes.

The second conclusion says that division by the trailing-field modulus leaves the same regime prefix in both magnitudes. It is the representation lemma that turns unsigned code order into strict order of the low exponent/fraction fields.