Exact comparisons for pi-scaled trigonometric functions

Exact rational-angle classifiers decide every rational special value before refinement. Sine and cosine first remove full turns exactly, so their classifiers and interval generators receive bounded angles even when the input has a very large integer part. All other direct values are irrational, and converging rational intervals separate every rational boundary. The inverse operations compare through their monotone principal branches; the branch endpoints are rational in units of pi, so no inverse enclosure is necessary.

The numerical tangent helper agrees with Mathlib's totalized tangent, which is zero at a pole. A format operation must reject half-integer tangent arguments before using this helper when its contract requires an invalid result there. Inverse sine/cosine contracts require [-1, 1].

def FloatLib.Numerics.TrigonometricComparison.prepareSinPi (argument : ℚ) (levels : ℕ) : Enclosure.Comparison.Prepared

Prepare exact pi-scaled sine comparisons, with complete rational special-value handling.

def FloatLib.Numerics.TrigonometricComparison.prepareCosPi (argument : ℚ) (levels : ℕ) : Enclosure.Comparison.Prepared

Prepare exact pi-scaled cosine comparisons, including thirds and half-integer angles.

def FloatLib.Numerics.TrigonometricComparison.compareSinPi (argument boundary : ℚ) : Ordering

Compare sin (argument * π) with a rational boundary.

def FloatLib.Numerics.TrigonometricComparison.compareCosPi (argument boundary : ℚ) : Ordering

Compare cos (argument * π) with a rational boundary.

def FloatLib.Numerics.TrigonometricComparison.prepareTanPi (argument : ℚ) (levels : ℕ) : Enclosure.Comparison.Prepared

Prepare pi-scaled tangent comparisons using the cosine sign and a linear residual.

The half-integer branch returns the ordering of zero, matching the totalized real tangent. Format wrappers with an invalid-result policy at poles must perform the same exact pole test.

def FloatLib.Numerics.TrigonometricComparison.compareTanPi (argument boundary : ℚ) : Ordering

Compare the totalized real tangent at argument * π with a rational boundary.

def FloatLib.Numerics.TrigonometricComparison.prepareArcsinPi (argument : ℚ) (levels : ℕ) : Enclosure.Comparison.Prepared

Prepare inverse sine divided by pi, using rational branch bounds and direct sine comparisons.

def FloatLib.Numerics.TrigonometricComparison.compareArcsinPi (argument boundary : ℚ) : Ordering

Compare arcsin argument / π on its real domain with a rational boundary.

def FloatLib.Numerics.TrigonometricComparison.prepareArccosPi (argument : ℚ) (levels : ℕ) : Enclosure.Comparison.Prepared

Prepare inverse cosine divided by pi, comparing cosine on its decreasing [0, π] branch.

def FloatLib.Numerics.TrigonometricComparison.compareArccosPi (argument boundary : ℚ) : Ordering

Compare arccos argument / π on its real domain with a rational boundary.

def FloatLib.Numerics.TrigonometricComparison.prepareArctanPi (argument : ℚ) (levels : ℕ) : Enclosure.Comparison.Prepared

Prepare inverse tangent divided by pi, whose branch is the open interval (-1/2, 1/2).

def FloatLib.Numerics.TrigonometricComparison.compareArctanPi (argument boundary : ℚ) : Ordering

Compare arctan argument / π with any rational boundary.