Exact real semantics of ordinary trigonometric comparisons

Every direct comparator returns the ordering of the exact real function value and rational boundary. The inverse sine and cosine contracts require an argument in [-1, 1] and use their usual principal branches. Exact rational values are included: sine, tangent, and arctangent at zero; cosine at zero; inverse sine at zero; and inverse cosine at one.

Prepared and uncached comparators satisfy the same contracts at every cache size.

theorem FloatLib.Numerics.TrigonometricComparison.prepareSin_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareSin argument levels).compare boundary = cmp (Real.sin ↑argument) ↑boundary

Sharing sine enclosures preserves the exact real ordering.

theorem FloatLib.Numerics.TrigonometricComparison.prepareCos_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareCos argument levels).compare boundary = cmp (Real.cos ↑argument) ↑boundary

Sharing cosine enclosures preserves the exact real ordering, including cos 0 = 1.

theorem FloatLib.Numerics.TrigonometricComparison.prepareArctan_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareArctan argument levels).compare boundary = cmp (Real.arctan ↑argument) ↑boundary

Sharing arctangent enclosures preserves the exact real ordering.

theorem FloatLib.Numerics.TrigonometricComparison.compareSin_eq_real (argument boundary : ℚ) : compareSin argument boundary = cmp (Real.sin ↑argument) ↑boundary

Sine comparison is total and agrees with the real ordering.

theorem FloatLib.Numerics.TrigonometricComparison.compareCos_eq_real (argument boundary : ℚ) : compareCos argument boundary = cmp (Real.cos ↑argument) ↑boundary

Cosine comparison is total and agrees with the real ordering.

theorem FloatLib.Numerics.TrigonometricComparison.compareArctan_eq_real (argument boundary : ℚ) : compareArctan argument boundary = cmp (Real.arctan ↑argument) ↑boundary

Arctangent comparison is total and agrees with the real ordering.

theorem FloatLib.Numerics.TrigonometricComparison.prepareTan_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareTan argument levels).compare boundary = cmp (Real.tan ↑argument) ↑boundary

The cosine sign and the residual sign determine the exact tangent ordering.

theorem FloatLib.Numerics.TrigonometricComparison.compareTan_eq_real (argument boundary : ℚ) : compareTan argument boundary = cmp (Real.tan ↑argument) ↑boundary

Tangent comparison terminates and agrees with the exact real value at every rational input.

theorem FloatLib.Numerics.TrigonometricComparison.prepareArcsin_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) (hlower : -1 ≤ argument) (hupper : argument ≤ 1) : (prepareArcsin argument levels).compare boundary = cmp (Real.arcsin ↑argument) ↑boundary

Inverse sine comparison agrees with its real principal branch throughout [-1, 1].

theorem FloatLib.Numerics.TrigonometricComparison.compareArcsin_eq_real (argument boundary : ℚ) (hlower : -1 ≤ argument) (hupper : argument ≤ 1) : compareArcsin argument boundary = cmp (Real.arcsin ↑argument) ↑boundary

Inverse sine comparison is total on its real domain, including endpoints and exact zero.

theorem FloatLib.Numerics.TrigonometricComparison.prepareArccos_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) (hlower : -1 ≤ argument) (hupper : argument ≤ 1) : (prepareArccos argument levels).compare boundary = cmp (Real.arccos ↑argument) ↑boundary

Inverse cosine comparison agrees with its decreasing real principal branch on [-1, 1].

theorem FloatLib.Numerics.TrigonometricComparison.compareArccos_eq_real (argument boundary : ℚ) (hlower : -1 ≤ argument) (hupper : argument ≤ 1) : compareArccos argument boundary = cmp (Real.arccos ↑argument) ↑boundary

Inverse cosine comparison is total on its real domain, including the exact value at one.