Correctness of the standard posit quire model

The standard quire model has raw-word round-trip laws, an exact characterization of the reserved NaR word, ordinary coefficient bounds, and rational semantics for integer dyadic conversion.

References

• Posit Working Group, Standard for Posit Arithmetic (2022), March 2, 2022, Sections 3.4 and 5.11, https://posithub.org/docs/posit_standard-2.pdf.

theorem FloatLib.Floats.Formats.Posit.Quire.width_pos (format : Format) : 0 < width format

The quire width is positive for every valid posit descriptor.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Quire.Model.ofNatBits_toNatBits {format : Format} (value : Model format) : ofNatBits format value.toNatBits = value

Re-encoding a quire's complete bit pattern preserves it.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Quire.Model.toNatBits_ofNatBits_of_lt (format : Format) (bits : ℕ) (bits_lt : bits < 2 ^ width format) : (ofNatBits format bits).toNatBits = bits

An in-range unsigned word is unchanged by standard-quire encoding.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Quire.Model.coefficient_zero (format : Format) : (zero format).coefficient = 0

The canonical zero quire has integer coefficient zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Quire.Model.coefficient_nar (format : Format) : (nar format).coefficient = Numerics.Representations.FixedInt.minValue (width format)

The canonical NaR quire uses the reserved sign-bit coefficient.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.zero_ne_nar (format : Format) : zero format ≠ nar format

Zero and quire NaR are distinct at every valid posit width.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Quire.Model.isNaR_nar (format : Format) : (nar format).isNaR = true

The quire NaR predicate recognizes the canonical NaR value.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Quire.Model.isNaR_zero (format : Format) : (zero format).isNaR = false

The canonical zero quire is not NaR.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Quire.Model.isNaR_eq_true_iff {format : Format} (value : Model format) : value.isNaR = true ↔ value = nar format

The executable NaR test recognizes exactly the reserved word.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.eq_nar_iff_coefficient_eq_min {format : Format} (value : Model format) : value = nar format ↔ value.coefficient = Numerics.Representations.FixedInt.minValue (width format)

A quire word equals NaR exactly when its signed coefficient is the reserved minimum.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.coefficient_in_fixedRange {format : Format} (value : Model format) : Numerics.Representations.FixedInt.InRange (width format) value.coefficient

Every stored quire coefficient lies in the inclusive signed range of its physical word.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.ordinaryCoefficient_iff_isNaR_eq_false {format : Format} (value : Model format) : OrdinaryCoefficient format value.coefficient ↔ value.isNaR = false

A coefficient is ordinary exactly when the quire word is not the reserved NaR code.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.ordinaryCoefficient_neg {format : Format} {value : ℤ} (hvalue : OrdinaryCoefficient format value) : OrdinaryCoefficient format (-value)

Negation preserves the set of ordinary quire coefficients.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.ordinaryCoefficient_of_natAbs_lt {format : Format} {value : ℤ} (hvalue : value.natAbs < 2 ^ (width format - 1)) : OrdinaryCoefficient format value

Any integer whose absolute magnitude is below the positive half-range is an ordinary quire coefficient.

The strict bound excludes both signed overflow and the reserved most-negative NaR word.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.coefficient_ofCoefficient_of_ordinary {format : Format} {value : ℤ} (hvalue : OrdinaryCoefficient format value) : (ofCoefficient format value).coefficient = value

Encoding an ordinary coefficient preserves it exactly.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.ofCoefficient_eq_nar_of_not_ordinary {format : Format} {value : ℤ} (hvalue : ¬OrdinaryCoefficient format value) : ofCoefficient format value = nar format

A coefficient outside the ordinary range, including the reserved minimum, becomes NaR.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.coefficientOfDyadic_denotes (format : Format) (value : Numerics.Dyadic) (hscale : scaleExponent format ≤ value.exponent) : Rat.ofInt (coefficientOfDyadic format value) * 2 ^ scaleExponent format = value.toRat

Dyadic-to-quire scaling preserves exact value when the stored exponent is high enough.