Real rounding and domains of pi-scaled posit functions

The exact rational classifiers and convergent comparison kernels determine the standard rounding of the mathematical result. Tangent poles are excluded explicitly: Mathlib's zero-valued totalization at a pole is not the posit operation's exceptional-value policy.

theorem FloatLib.Floats.Formats.Posit.Model.sinPi_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.sinPi = RealRounding.round format (Real.sin (↑q * Real.pi))

Pi-scaled sine rounds the exact product-angle expression once.

theorem FloatLib.Floats.Formats.Posit.Model.cosPi_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.cosPi = RealRounding.round format (Real.cos (↑q * Real.pi))

Pi-scaled cosine rounds the exact product-angle expression once.

theorem FloatLib.Floats.Formats.Posit.Model.tanPi_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hpole : Int.fract q ≠ 1 / 2) : value.tanPi = RealRounding.round format (Real.tan (↑q * Real.pi))

Pi-scaled tangent has the required real rounding away from its exact half-integer poles.

theorem FloatLib.Floats.Formats.Posit.Model.tanPi_eq_nar_of_pole {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hpole : Int.fract q = 1 / 2) : value.tanPi = nar format

Every half-integer pi-scaled tangent input produces NaR.

theorem FloatLib.Floats.Formats.Posit.Model.arcSinPi_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hlower : -1 ≤ q) (hupper : q ≤ 1) : value.arcSinPi = RealRounding.round format (Real.arcsin ↑q / Real.pi)

The inverse sine is divided by pi before its one rounding.

theorem FloatLib.Floats.Formats.Posit.Model.arcCosPi_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hlower : -1 ≤ q) (hupper : q ≤ 1) : value.arcCosPi = RealRounding.round format (Real.arccos ↑q / Real.pi)

The inverse cosine is divided by pi before its one rounding.

theorem FloatLib.Floats.Formats.Posit.Model.arcTanPi_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.arcTanPi = RealRounding.round format (Real.arctan ↑q / Real.pi)

The inverse tangent is divided by pi before its one rounding.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.sinPi_nar {format : Format} : (nar format).sinPi = nar format

NaR propagates through sinPi.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.cosPi_nar {format : Format} : (nar format).cosPi = nar format

NaR propagates through cosPi.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.arcSinPi_nar {format : Format} : (nar format).arcSinPi = nar format

NaR propagates through arcSinPi.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.arcCosPi_nar {format : Format} : (nar format).arcCosPi = nar format

NaR propagates through arcCosPi.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.arcTanPi_nar {format : Format} : (nar format).arcTanPi = nar format

NaR propagates through arcTanPi.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.tanPi_nar {format : Format} : (nar format).tanPi = nar format

NaR propagates through pi-scaled tangent.

theorem FloatLib.Floats.Formats.Posit.Model.arcSinPi_eq_nar_of_outside {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (houtside : q < -1 ∨ 1 < q) : value.arcSinPi = nar format

arcSinPi rejects finite inputs outside its real domain.

theorem FloatLib.Floats.Formats.Posit.Model.arcCosPi_eq_nar_of_outside {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (houtside : q < -1 ∨ 1 < q) : value.arcCosPi = nar format

arcCosPi rejects finite inputs outside its real domain.