Exact rational values at rational multiples of pi

Most rational angles have irrational sine and cosine. The exceptions must be handled before interval refinement: an interval may otherwise straddle an exact rounding boundary forever. Reduction modulo one leaves four cosine cases; the removed integer controls the sign. No approximate value of pi enters this classification.

def FloatLib.Numerics.TrigonometricComparison.halfTurnSign (turns : ℤ) : ℚ

Sign contributed by an integer number of half-turns.

Only parity matters. Reducing modulo two also avoids passing an arbitrarily large exponent to the runtime's power operation for wide posit inputs.

def FloatLib.Numerics.TrigonometricComparison.cosPiExact (argument : ℚ) : Option ℚ

The rational cosine value, when it exists, at the angle argument * π.

def FloatLib.Numerics.TrigonometricComparison.sinPiExact (argument : ℚ) : Option ℚ

Classify exact sine values by the complementary cosine angle.

def FloatLib.Numerics.TrigonometricComparison.centeredPi (argument : ℚ) : ℚ

Reduce a pi-scaled angle to [-1/2, 1/2), preserving its tangent.

def FloatLib.Numerics.TrigonometricComparison.tanPiExact (argument : ℚ) : Option ℚ

Exact rational tangent values; half-integer poles are checked separately.

def FloatLib.Numerics.TrigonometricComparison.arctanPiExact (argument : ℚ) : Option ℚ

The rational values of inverse tangent divided by pi.

def FloatLib.Numerics.TrigonometricComparison.arcsinPiExact (argument : ℚ) : Option ℚ

The rational values of inverse sine divided by pi on its real domain.

def FloatLib.Numerics.TrigonometricComparison.arccosPiExact (argument : ℚ) : Option ℚ

Inverse cosine uses the complementary inverse sine angle.