Correctness of exact posit-quire semantics

A quire is a wide signed fixed-point accumulator with one reserved NaR encoding. This module connects its stored coefficient to exact rational, dyadic, and generic numerical-value views, and proves that all three recognize the same exceptional word.

Successful coefficient construction is preserved exactly at the quire scale. These facts are the semantic base for exact product accumulation within the quire's capacity; rounding back to a posit is a separate operation.

@[simp]

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

The zero quire denotes the exact rational zero.

@[simp]

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

The NaR quire has no ordinary rational interpretation.

@[simp]

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

Exact quire decoding recognizes the canonical zero value.

@[simp]

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

Exact quire decoding recognizes the canonical NaR value.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Quire.Model.toDyadic?_zero (format : Format) : (zero format).toDyadic? = some (Numerics.Dyadic.ofScaledInt 0 (scaleExponent format))

The zero quire maps to a zero-valued dyadic at the quire's fixed binary scale.

@[simp]

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

The NaR quire has no ordinary dyadic interpretation.

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

Rational and dyadic quire views agree exactly.

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

An exact rational is unavailable precisely for the reserved quire NaR word.

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

An exact dyadic is unavailable precisely for the reserved quire NaR word.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.toRat?_ofCoefficient_of_ordinary {format : Format} {coefficient : ℤ} (hcoefficient : OrdinaryCoefficient format coefficient) : (ofCoefficient format coefficient).toRat? = some (Rat.ofInt coefficient * 2 ^ scaleExponent format)

Exact semantics of a successfully encoded ordinary coefficient.

theorem FloatLib.Floats.Formats.Posit.Quire.Model.toDyadic?_ofCoefficient_of_ordinary {format : Format} {coefficient : ℤ} (hcoefficient : OrdinaryCoefficient format coefficient) : (ofCoefficient format coefficient).toDyadic? = some (Numerics.Dyadic.ofScaledInt coefficient (scaleExponent format))

Shared-dyadic semantics of a successfully encoded ordinary coefficient.