Exact widening of posit words

Appending zero bits preserves the decoded value, including zero and NaR, whenever the destination is at least as wide as the source. For finite inputs, rounding the exact source value at the destination therefore produces precisely that extended word.

The proof iterates the decoder's one-bit precision identity; neither the storage backend nor particular widths enter the argument.

References

• Posit Standard (2022), §6.1.

theorem FloatLib.Floats.Formats.Posit.Model.nonnegativeRatAt_widen (source target : Format) (hwidth : source.bits ≤ target.bits) {code : ℕ} (hcode : code < source.signMaskNat) : nonnegativeRatAt target (code * 2 ^ (target.bits - source.bits)) = nonnegativeRatAt source code

Any number of appended zero bits preserves a nonnegative finite decoded value.

theorem FloatLib.Floats.Formats.Posit.Model.toRat?_widen {source : Format} (target : Format) (hw : source.bits ≤ target.bits) (value : Model source) : (ofNatBits (value.toNatBits * 2 ^ (target.bits - source.bits))).toRat? = value.toRat?

Zero-bit extension preserves exact decoding for every word, including negative values and NaR.

theorem FloatLib.Floats.Formats.Posit.Model.roundRat_widen {source : Format} (target : Format) (hw : source.bits ≤ target.bits) (value : Model source) (q : ℚ) (hq : value.toRat? = some q) : roundRat target q = ofNatBits (value.toNatBits * 2 ^ (target.bits - source.bits))

Rounding a finite value into a wider descriptor appends exactly the additional zero bits.