Real semantics of posit trigonometric operations

The operation proofs compose exact comparator semantics with the standard posit rounding algorithm. They cover all finite inputs in the real domain, including exact zero results, domain endpoints, and nonzero saturation. NaR propagation and invalid inverse domains are stated separately.

theorem FloatLib.Floats.Formats.Posit.Model.Trigonometric.evaluate_eq_real (prepare : ℚ → ℕ → Numerics.Enclosure.Comparison.Prepared) (function : ℝ → ℝ) (hprepare : ∀ (argument : ℚ) (levels : ℕ) (boundary : ℚ), (prepare argument levels).compare boundary = cmp (function ↑argument) ↑boundary) {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : evaluate prepare value = RealRounding.round format (function ↑q)

Exact comparison followed by signed posit rounding gives the required real result.

theorem FloatLib.Floats.Formats.Posit.Model.Trigonometric.evaluateUnit_eq_real (prepare : ℚ → ℕ → Numerics.Enclosure.Comparison.Prepared) (function : ℝ → ℝ) (hprepare : ∀ (argument : ℚ) (levels : ℕ) (boundary : ℚ), -1 ≤ argument → argument ≤ 1 → (prepare argument levels).compare boundary = cmp (function ↑argument) ↑boundary) {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (hlower : -1 ≤ q) (hupper : q ≤ 1) : evaluateUnit prepare value = RealRounding.round format (function ↑q)

The same composition applies to a comparator whose contract is restricted to [-1, 1].

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.Trigonometric.evaluate_nar (prepare : ℚ → ℕ → Numerics.Enclosure.Comparison.Prepared) {format : Format} : evaluate prepare (nar format) = nar format

Evaluation propagates NaR without preparing a comparison search.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.Trigonometric.evaluateUnit_nar (prepare : ℚ → ℕ → Numerics.Enclosure.Comparison.Prepared) {format : Format} : evaluateUnit prepare (nar format) = nar format

The closed-domain adapter also propagates NaR.

theorem FloatLib.Floats.Formats.Posit.Model.Trigonometric.evaluateUnit_eq_nar (prepare : ℚ → ℕ → Numerics.Enclosure.Comparison.Prepared) {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) (houtside : q < -1 ∨ 1 < q) : evaluateUnit prepare value = nar format

A finite input outside the closed unit interval produces NaR before evaluation.

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

Sine rounds its exact real value at every finite radian input.

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

Cosine rounds its exact real value at every finite radian input.

theorem FloatLib.Floats.Formats.Posit.Model.tan_eq_real {format : Format} (value : Model format) {q : ℚ} (hvalue : value.toRat? = some q) : value.tan = RealRounding.round format (Real.tan ↑q)

Tangent is correctly rounded at every finite posit input.

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

Inverse sine includes both endpoints of its real domain.

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

Inverse cosine includes both endpoints of its real domain.

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

Inverse tangent rounds its principal real value at every finite input.

@[simp]

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

Sine propagates NaR.

@[simp]

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

Cosine propagates NaR.

@[simp]

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

Tangent propagates NaR.

@[simp]

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

Inverse sine propagates NaR.

@[simp]

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

Inverse cosine propagates NaR.

@[simp]

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

Inverse tangent propagates NaR.

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

Inverse sine rejects real inputs outside [-1, 1].

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

Inverse cosine rejects real inputs outside [-1, 1].