Correct rounding of configured posit pi-scaled trigonometric operations

The configured pi-scaled operations inherit the model's real-rounding theorems through any lawful storage codec. Separate equations cover NaR inputs, inverse-function domain failures, and the half-integer poles of tanPi.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_sinPi {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (sinPi value) = (toModel value).sinPi

Configured sine refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_cosPi {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (cosPi value) = (toModel value).cosPi

Configured cosine refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_tanPi {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (tanPi value) = (toModel value).tanPi

Configured tangent refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_arcSinPi {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (arcSinPi value) = (toModel value).arcSinPi

Configured inverse sine refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_arcCosPi {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (arcCosPi value) = (toModel value).arcCosPi

Configured inverse cosine refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_arcTanPi {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (arcTanPi value) = (toModel value).arcTanPi

Configured inverse tangent refines the model operation.

theorem FloatLib.Floats.ExecFloat.Posit.sinPi_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) : toModel (sinPi value) = Formats.Posit.Model.RealRounding.round format (Real.sin (↑q * Real.pi))

Configured sine rounds the exact real result once.

theorem FloatLib.Floats.ExecFloat.Posit.cosPi_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) : toModel (cosPi value) = Formats.Posit.Model.RealRounding.round format (Real.cos (↑q * Real.pi))

Configured cosine rounds the exact real result once.

theorem FloatLib.Floats.ExecFloat.Posit.tanPi_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) (hpole : Int.fract q ≠ 1 / 2) : toModel (tanPi value) = Formats.Posit.Model.RealRounding.round format (Real.tan (↑q * Real.pi))

Configured tangent rounds the exact real result once.

theorem FloatLib.Floats.ExecFloat.Posit.arcSinPi_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) (hlower : -1 ≤ q) (hupper : q ≤ 1) : toModel (arcSinPi value) = Formats.Posit.Model.RealRounding.round format (Real.arcsin ↑q / Real.pi)

Configured inverse sine includes both real-domain endpoints.

theorem FloatLib.Floats.ExecFloat.Posit.arcCosPi_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) (hlower : -1 ≤ q) (hupper : q ≤ 1) : toModel (arcCosPi value) = Formats.Posit.Model.RealRounding.round format (Real.arccos ↑q / Real.pi)

Configured inverse cosine includes both real-domain endpoints.

theorem FloatLib.Floats.ExecFloat.Posit.arcTanPi_eq_real {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) : toModel (arcTanPi value) = Formats.Posit.Model.RealRounding.round format (Real.arctan ↑q / Real.pi)

Configured inverse tangent rounds its exact principal value.

theorem FloatLib.Floats.ExecFloat.Posit.sinPi_eq_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hvalue : toModel value = Formats.Posit.Model.nar format) : toModel (sinPi value) = Formats.Posit.Model.nar format

NaR propagates through configured sine.

theorem FloatLib.Floats.ExecFloat.Posit.cosPi_eq_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hvalue : toModel value = Formats.Posit.Model.nar format) : toModel (cosPi value) = Formats.Posit.Model.nar format

NaR propagates through configured cosine.

theorem FloatLib.Floats.ExecFloat.Posit.tanPi_eq_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hvalue : toModel value = Formats.Posit.Model.nar format) : toModel (tanPi value) = Formats.Posit.Model.nar format

NaR propagates through configured tangent.

theorem FloatLib.Floats.ExecFloat.Posit.arcSinPi_eq_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hvalue : toModel value = Formats.Posit.Model.nar format) : toModel (arcSinPi value) = Formats.Posit.Model.nar format

NaR propagates through configured inverse sine.

theorem FloatLib.Floats.ExecFloat.Posit.arcCosPi_eq_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hvalue : toModel value = Formats.Posit.Model.nar format) : toModel (arcCosPi value) = Formats.Posit.Model.nar format

NaR propagates through configured inverse cosine.

theorem FloatLib.Floats.ExecFloat.Posit.arcTanPi_eq_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) (hvalue : toModel value = Formats.Posit.Model.nar format) : toModel (arcTanPi value) = Formats.Posit.Model.nar format

NaR propagates through configured inverse tangent.

theorem FloatLib.Floats.ExecFloat.Posit.arcSinPi_eq_nar_of_outside {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) (houtside : q < -1 ∨ 1 < q) : toModel (arcSinPi value) = Formats.Posit.Model.nar format

Configured inverse sine rejects the exterior of its real domain.

theorem FloatLib.Floats.ExecFloat.Posit.arcCosPi_eq_nar_of_outside {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) (houtside : q < -1 ∨ 1 < q) : toModel (arcCosPi value) = Formats.Posit.Model.nar format

Configured inverse cosine rejects the exterior of its real domain.

theorem FloatLib.Floats.ExecFloat.Posit.tanPi_eq_nar_of_pole {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {q : ℚ} (hvalue : toRat? value = some q) (hpole : Int.fract q = 1 / 2) : toModel (tanPi value) = Formats.Posit.Model.nar format

Configured pi-scaled tangent rejects every half-integer pole.