Correctness properties of exact posit semantics

The complete and partial rational decoders preserve zero and finite fields, identify NaR exactly, and agree with the shared dyadic decoder used by integer arithmetic kernels.

This is the semantic junction between user-facing rational meanings and implementation-facing dyadics. Proving the agreement once lets order, rounding, and arithmetic developments choose the more convenient exact representation without creating parallel definitions of what a posit word means.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.ExactValue.forget_zero {format : Format} : zero.forget = Numerics.NumericalValue.finite 0

Forgetting exact zero produces finite rational zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.ExactValue.forget_finite {format : Format} (fields : DecodedFields format) : (finite fields).forget = Numerics.NumericalValue.finite fields.toRat

Forgetting decoded finite fields preserves their exact rational value.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.ExactValue.forget_nar {format : Format} : nar.forget = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.notAReal

Forgetting NaR records the common notAReal exceptional value.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.ExactValue.toRat?_zero {format : Format} : zero.toRat? = some 0

The optional rational view maps exact zero to rational zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.ExactValue.toRat?_finite {format : Format} (fields : DecodedFields format) : (finite fields).toRat? = some fields.toRat

The optional rational view preserves decoded finite fields exactly.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.ExactValue.toRat?_nar {format : Format} : nar.toRat? = none

The optional rational view is unavailable for NaR.

theorem FloatLib.Floats.Formats.Posit.Model.toRat?_eq_toDyadic?_map {format : Format} (value : Model format) : value.toRat? = Option.map Numerics.Dyadic.toRat value.toDyadic?

The rational and shared-dyadic decoders commute.

Integer kernels may therefore prove their rounding behavior in Numerics.Dyadic and reuse the result against the public rational specification.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.decode_zero (format : Format) : (zero format).decode = Numerics.NumericalValue.finite 0

Decoding the canonical zero word produces finite rational zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.decode_nar (format : Format) : (nar format).decode = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.notAReal

Decoding the unique NaR word produces the common notAReal exception.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toRat?_zero (format : Format) : (zero format).toRat? = some 0

The optional exact-rational semantics of the canonical zero word is zero.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.toRat?_nar (format : Format) : (nar format).toRat? = none

The optional exact-rational semantics of the unique NaR word is unavailable.

theorem FloatLib.Floats.Formats.Posit.Model.toRat?_eq_none_iff {format : Format} (value : Model format) : value.toRat? = none ↔ value.isNaR = true

An exact rational is unavailable precisely for the unique NaR word.