Total comparisons for ordinary trigonometric functions

These operations compare an exact trigonometric value with a rational boundary. Adaptive rational enclosures determine the ordering; irrationality proves that the search terminates outside the explicitly handled rational values at zero. Prepared comparators share a finite prefix of enclosures across boundary queries, with unrestricted refinement beyond that prefix.

Tangent compares sin x - b * cos x with zero and uses the sign of cosine. Inverse sine and cosine compare through their monotone principal branches, after exact comparisons with π locate the boundary. Their real-domain contract is -1 ≤ argument ≤ 1.

These are ordinary radian functions. No rational-angle equality decision for π-scaled functions is inferred from these searches.

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

Prepare a total sine comparator, sharing reduced enclosures across rational boundaries.

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

Prepare a total cosine comparator, including the exact value cos 0 = 1.

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

Prepare a total arctangent comparator, with exact equality at zero.

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

Compare the sine of any rational argument with any rational boundary.

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

Compare the cosine of any rational argument with any rational boundary.

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

Compare the arctangent of any rational argument with any rational boundary.

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

Prepare tangent comparisons without interval division.

Rational arguments are never tangent poles. The cosine sign and the cached sine/cosine enclosures are shared across queries, while each boundary determines a different residual.

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

Compare the tangent of any rational argument with any rational boundary.

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

Prepare inverse sine comparisons on [-1, 1], sharing the π/4 enclosures.

Boundaries outside the principal branch are decided first. Inside it, sine is strictly increasing, so the inverse comparison reduces to a direct sine comparison with reversed order.

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

Compare inverse sine on its real domain with any rational boundary.

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

Prepare inverse cosine comparisons on [-1, 1], sharing the π/4 enclosures.

The principal branch is [0, π], where cosine is strictly decreasing.

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

Compare inverse cosine on its real domain with any rational boundary.