Correct rounding of configured posit trigonometric operations

The sine, cosine, tangent, and inverse-function theorems identify each configured result with one rounding of the real function, under the stated domain conditions. NaR propagation and out-of-domain results are proved separately. All results hold for every lawful storage codec and every valid posit width.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_sin {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 (sin value) = (toModel value).sin

Configured sine refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_cos {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 (cos value) = (toModel value).cos

Configured cosine refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_tan {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 (tan value) = (toModel value).tan

Configured tangent refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_arcSin {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 (arcSin value) = (toModel value).arcSin

Configured inverse sine refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_arcCos {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 (arcCos value) = (toModel value).arcCos

Configured inverse cosine refines the model operation.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_arcTan {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 (arcTan value) = (toModel value).arcTan

Configured inverse tangent refines the model operation.

theorem FloatLib.Floats.ExecFloat.Posit.sin_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 (sin value) = Formats.Posit.Model.RealRounding.round format (Real.sin ↑q)

Configured sine rounds the exact real result once.

theorem FloatLib.Floats.ExecFloat.Posit.cos_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 (cos value) = Formats.Posit.Model.RealRounding.round format (Real.cos ↑q)

Configured cosine rounds the exact real result once.

theorem FloatLib.Floats.ExecFloat.Posit.tan_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 (tan value) = Formats.Posit.Model.RealRounding.round format (Real.tan ↑q)

Configured tangent rounds the exact real result once.

theorem FloatLib.Floats.ExecFloat.Posit.arcSin_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 (arcSin value) = Formats.Posit.Model.RealRounding.round format (Real.arcsin ↑q)

Configured inverse sine includes both real-domain endpoints.

theorem FloatLib.Floats.ExecFloat.Posit.arcCos_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 (arcCos value) = Formats.Posit.Model.RealRounding.round format (Real.arccos ↑q)

Configured inverse cosine includes both real-domain endpoints.

theorem FloatLib.Floats.ExecFloat.Posit.arcTan_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 (arcTan value) = Formats.Posit.Model.RealRounding.round format (Real.arctan ↑q)

Configured inverse tangent rounds its exact principal value.

theorem FloatLib.Floats.ExecFloat.Posit.sin_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 (sin value) = Formats.Posit.Model.nar format

NaR propagates through configured sine.

theorem FloatLib.Floats.ExecFloat.Posit.cos_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 (cos value) = Formats.Posit.Model.nar format

NaR propagates through configured cosine.

theorem FloatLib.Floats.ExecFloat.Posit.tan_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 (tan value) = Formats.Posit.Model.nar format

NaR propagates through configured tangent.

theorem FloatLib.Floats.ExecFloat.Posit.arcSin_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 (arcSin value) = Formats.Posit.Model.nar format

NaR propagates through configured inverse sine.

theorem FloatLib.Floats.ExecFloat.Posit.arcCos_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 (arcCos value) = Formats.Posit.Model.nar format

NaR propagates through configured inverse cosine.

theorem FloatLib.Floats.ExecFloat.Posit.arcTan_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 (arcTan value) = Formats.Posit.Model.nar format

NaR propagates through configured inverse tangent.

theorem FloatLib.Floats.ExecFloat.Posit.arcSin_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 (arcSin value) = Formats.Posit.Model.nar format

Configured inverse sine rejects the exterior of its real domain.

theorem FloatLib.Floats.ExecFloat.Posit.arcCos_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 (arcCos value) = Formats.Posit.Model.nar format

Configured inverse cosine rejects the exterior of its real domain.