Exact posit decoding and rounding round trips

Rounding an exactly decoded finite posit recovers its original word at every descriptor width. The sign/magnitude lemmas isolate whole-word two's-complement symmetry so character conversion, integer functions, and changes of precision can reuse the same decoding argument.

theorem FloatLib.Floats.Formats.Posit.Model.ofNatBits_magnitudeBits {format : Format} (value : Model format) : (if value.signBit = true then (ofNatBits value.magnitudeBits).neg else ofNatBits value.magnitudeBits) = value

Restore the complete word from its sign and unsigned magnitude.

theorem FloatLib.Floats.Formats.Posit.Model.decodeFields_toRat_eq_signed_magnitude {format : Format} (value : Model format) (hnar : value ≠ nar format) (hzero : value ≠ zero format) : value.decodeFields.toRat = if value.signBit = true then -nonnegativeRatAt format value.magnitudeBits else nonnegativeRatAt format value.magnitudeBits

Decoded fields factor as their sign times the exact value of the unsigned magnitude word.

theorem FloatLib.Floats.Formats.Posit.Model.toRat?_eq_signed_magnitude {format : Format} (value : Model format) (hnar : value ≠ nar format) : value.toRat? = some (if value.signBit = true then -nonnegativeRatAt format value.magnitudeBits else nonnegativeRatAt format value.magnitudeBits)

Every finite word, including zero, decodes as its signed unsigned-magnitude value.

theorem FloatLib.Floats.Formats.Posit.Model.roundRat_toRat? {format : Format} (value : Model format) (exact : ℚ) (hexact : value.toRat? = some exact) : roundRat format exact = value

Standard posit rounding is a left inverse of exact rational decoding at every width.