Complete rational-value classification for pi-scaled sine and cosine

Niven's theorem supplies completeness, including thirds as well as the more familiar integer and half-integer angles. Every unclassified value is irrational, so converging rational enclosures eventually separate it from any rational rounding boundary.

theorem FloatLib.Numerics.TrigonometricComparison.halfTurnSign_eq_zpow (turns : ℤ) : halfTurnSign turns = (-1) ^ turns

The parity computation is the exact sign from the integer-angle cosine identity.

theorem FloatLib.Numerics.TrigonometricComparison.cosPiExact_eq_real (argument value : ℚ) (hvalue : cosPiExact argument = some value) : Real.cos (↑argument * Real.pi) = ↑value

Every reported rational cosine value is exact.

theorem FloatLib.Numerics.TrigonometricComparison.irrational_cosPi_of_exact_none (argument : ℚ) (hnone : cosPiExact argument = none) : Irrational (Real.cos (↑argument * Real.pi))

An unclassified cosine value is irrational, so refinement cannot stall at a boundary.

theorem FloatLib.Numerics.TrigonometricComparison.sinPiExact_eq_real (argument value : ℚ) (hvalue : sinPiExact argument = some value) : Real.sin (↑argument * Real.pi) = ↑value

Every reported rational sine value is exact.

theorem FloatLib.Numerics.TrigonometricComparison.irrational_sinPi_of_exact_none (argument : ℚ) (hnone : sinPiExact argument = none) : Irrational (Real.sin (↑argument * Real.pi))

An unclassified sine value is irrational.