Ordinary posit values as exact rationals

The NaR encoding has no rational denotation. Excluding it gives a subtype on which exact rational decoding is total.

No alternate encoding is introduced: Model.Ordinary format is a proof-carrying view of the same encoded word. The full posit order still belongs to Model format; the rational coordinate here is available for every value of the subtype.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Posit.Model.Ordinary (format : Format) : Type

A posit word accompanied by proof that it is not the unique NaR encoding.

theorem FloatLib.Floats.Formats.Posit.Model.Ordinary.toRat_isSome {format : Format} (value : Ordinary format) : (↑value).toRat?.isSome = true

The optional exact semantics of an ordinary posit is inhabited.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.Ordinary.toRat {format : Format} (value : Ordinary format) : ℚ

Total exact rational semantics of an ordinary posit.

The proof argument to Option.get is erased at runtime. It records that the only absent rational meaning belongs to NaR, which the subtype excludes.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.Ordinary.model_toRat?_eq_some {format : Format} (value : Ordinary format) : (↑value).toRat? = some value.toRat

Forgetting the subtype and decoding recovers exactly the total rational coordinate.

def FloatLib.Floats.Formats.Posit.Model.Ordinary.zero (format : Format) : Ordinary format

Ordinary zero, retaining proof that the zero word is not NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.Ordinary.toRat_zero (format : Format) : (zero format).toRat = 0

The posit zero denotes the rational zero.