Correctly rounded posit trigonometric operations

Each finite input is decoded exactly. A prepared comparator then compares the mathematical function value with posit rounding boundaries, sharing its enclosure data across the search. Only the final result is rounded. Inverse sine and cosine reject inputs outside [-1, 1]; all six operations propagate NaR.

The radian functions and principal branches follow the Posit Standard (2022), §5.5.

def FloatLib.Floats.Formats.Posit.Model.Trigonometric.evaluate {format : Format} (prepare : ℚ → ℕ → Numerics.Enclosure.Comparison.Prepared) (value : Model format) : Model format

Round using a prepared comparator, propagating NaR. An exact comparator gives the real rounding contract in evaluate_eq_real.

def FloatLib.Floats.Formats.Posit.Model.Trigonometric.evaluateUnit {format : Format} (prepare : ℚ → ℕ → Numerics.Enclosure.Comparison.Prepared) (value : Model format) : Model format

Check the closed real domain of inverse sine or cosine before preparing its comparator.

def FloatLib.Floats.Formats.Posit.Model.sin {format : Format} (value : Model format) : Model format

Correctly rounded sine of a radian argument. NaR propagates.

def FloatLib.Floats.Formats.Posit.Model.cos {format : Format} (value : Model format) : Model format

Correctly rounded cosine of a radian argument. NaR propagates.

def FloatLib.Floats.Formats.Posit.Model.tan {format : Format} (value : Model format) : Model format

Correctly rounded tangent. A finite posit, being rational, is never a radian tangent pole.

def FloatLib.Floats.Formats.Posit.Model.arcSin {format : Format} (value : Model format) : Model format

Inverse sine on its principal branch [-π/2, π/2]; invalid inputs produce NaR.

def FloatLib.Floats.Formats.Posit.Model.arcCos {format : Format} (value : Model format) : Model format

Inverse cosine on its principal branch [0, π]; invalid inputs produce NaR.

def FloatLib.Floats.Formats.Posit.Model.arcTan {format : Format} (value : Model format) : Model format

Correctly rounded inverse tangent on its principal branch (-π/2, π/2).