Real semantics of pi-scaled comparisons

The exact-value branches and every adaptive branch return the ordering of the corresponding real function and rational boundary. Inverse sine and cosine use their principal branches on [-1, 1]. Tangent agrees with the totalized real function, including zero at half-integer poles; format wrappers must reject poles when required by their exceptional-value contract.

theorem FloatLib.Numerics.TrigonometricComparison.prepareSinPi_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareSinPi argument levels).compare boundary = cmp (Real.sin (↑argument * Real.pi)) ↑boundary

Prepared pi-scaled sine comparisons agree with the exact real ordering at every cache size.

theorem FloatLib.Numerics.TrigonometricComparison.prepareCosPi_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareCosPi argument levels).compare boundary = cmp (Real.cos (↑argument * Real.pi)) ↑boundary

Prepared pi-scaled cosine comparisons include all classified rational special values.

theorem FloatLib.Numerics.TrigonometricComparison.prepareTanPi_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareTanPi argument levels).compare boundary = cmp (Real.tan (↑argument * Real.pi)) ↑boundary

The tangent helper agrees with the totalized real tangent, including its pole convention.

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

Inverse sine divided by pi has the exact principal-branch ordering throughout [-1, 1].

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

Inverse cosine divided by pi uses the decreasing principal branch, including both endpoints.

theorem FloatLib.Numerics.TrigonometricComparison.prepareArctanPi_eq_real (argument : ℚ) (levels : ℕ) (boundary : ℚ) : (prepareArctanPi argument levels).compare boundary = cmp (Real.arctan ↑argument / Real.pi) ↑boundary

Inverse tangent divided by pi uses the increasing open principal branch.

theorem FloatLib.Numerics.TrigonometricComparison.compareSinPi_eq_real (argument boundary : ℚ) : compareSinPi argument boundary = cmp (Real.sin (↑argument * Real.pi)) ↑boundary

Exact real semantics of pi-scaled sine comparison.

theorem FloatLib.Numerics.TrigonometricComparison.compareCosPi_eq_real (argument boundary : ℚ) : compareCosPi argument boundary = cmp (Real.cos (↑argument * Real.pi)) ↑boundary

Exact real semantics of pi-scaled cosine comparison.

theorem FloatLib.Numerics.TrigonometricComparison.compareTanPi_eq_real (argument boundary : ℚ) : compareTanPi argument boundary = cmp (Real.tan (↑argument * Real.pi)) ↑boundary

Exact real semantics of the totalized pi-scaled tangent comparison.

theorem FloatLib.Numerics.TrigonometricComparison.compareArcsinPi_eq_real (argument boundary : ℚ) (hlower : -1 ≤ argument) (hupper : argument ≤ 1) : compareArcsinPi argument boundary = cmp (Real.arcsin ↑argument / Real.pi) ↑boundary

Exact inverse sine semantics on its closed real domain.

theorem FloatLib.Numerics.TrigonometricComparison.compareArccosPi_eq_real (argument boundary : ℚ) (hlower : -1 ≤ argument) (hupper : argument ≤ 1) : compareArccosPi argument boundary = cmp (Real.arccos ↑argument / Real.pi) ↑boundary

Exact inverse cosine semantics on its closed real domain.

theorem FloatLib.Numerics.TrigonometricComparison.compareArctanPi_eq_real (argument boundary : ℚ) : compareArctanPi argument boundary = cmp (Real.arctan ↑argument / Real.pi) ↑boundary

Exact inverse tangent semantics at every rational input.