Exact tangent values and poles

Reducing the rational angle before introducing pi keeps the pole test exact, even at large arguments. On the open principal interval tangent is injective. Together with the rational value theorem, this proves that the three classifier branches exhaust all rational answers away from poles.

theorem FloatLib.Numerics.TrigonometricComparison.tan_centeredPi (argument : ℚ) : Real.tan (↑(centeredPi argument) * Real.pi) = Real.tan (↑argument * Real.pi)

Centering the rational angle preserves tangent exactly.

theorem FloatLib.Numerics.TrigonometricComparison.centeredPi_mem (argument : ℚ) (hpole : Int.fract argument ≠ 1 / 2) : -1 / 2 < centeredPi argument ∧ centeredPi argument < 1 / 2

Away from a half-integer pole, the centered angle lies in the open principal interval.

theorem FloatLib.Numerics.TrigonometricComparison.cosPi_eq_zero_of_fract_half (argument : ℚ) (hpole : Int.fract argument = 1 / 2) : Real.cos (↑argument * Real.pi) = 0

Half-integer pi-scaled angles are poles of tangent.

theorem FloatLib.Numerics.TrigonometricComparison.cosPi_eq_zero_iff (argument : ℚ) : Real.cos (↑argument * Real.pi) = 0 ↔ Int.fract argument = 1 / 2

The executable half-integer test detects every tangent pole.

theorem FloatLib.Numerics.TrigonometricComparison.tanPiExact_eq_real (argument value : ℚ) (hvalue : tanPiExact argument = some value) : Real.tan (↑argument * Real.pi) = ↑value

Every classified tangent value is exact.

theorem FloatLib.Numerics.TrigonometricComparison.irrational_tanPi_of_exact_none (argument : ℚ) (hpole : Int.fract argument ≠ 1 / 2) (hnone : tanPiExact argument = none) : Irrational (Real.tan (↑argument * Real.pi))

Away from poles, an unclassified tangent value is irrational.