Executable exact semantics of a posit quire

Every ordinary quire word denotes an exact rational fixed-point value. The reserved quire NaR word denotes ExceptionalValue.notAReal and has no rational or dyadic coordinate.

The definitions in this module are the execution boundary used by quire arithmetic and configured wrappers. Correctness theorems, real embeddings, and projective views live in separate modules.

@[inline]

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

Exact rational value represented by an ordinary quire, or none exactly for quire NaR.

@[inline]

def FloatLib.Floats.Formats.Posit.Quire.Model.decode {format : Format} (value : Model format) : Numerics.NumericalValue ℚ

Complete exact semantics, retaining quire NaR as an exceptional numerical observation.

@[inline]

def FloatLib.Floats.Formats.Posit.Quire.Model.toDyadic? {format : Format} (value : Model format) : Option Numerics.Dyadic

Exact shared-dyadic view of an ordinary quire.

This is the execution bridge used by qToP: the coefficient and fixed scale pass directly to the certified posit dyadic rounder without constructing a rational.