Rational trigonometric arguments and rounding boundaries

At a nonzero rational argument, sine, cosine, and tangent are transcendental. If sine or cosine were algebraic, the identity sin² x + cos² x = 1 would make both algebraic, and Euler's formula would contradict the transcendence of exp (x * I). Tangent reduces to cosine through cos² x = 1 / (1 + tan² x).

The irrationality corollaries rule out exact rational rounding boundaries. The input zero must be handled separately by executable comparisons.

theorem FloatLib.Numerics.Enclosure.transcendental_cos_ratCast (q : ℚ) (hq : q ≠ 0) : Transcendental ℚ (Real.cos ↑q)

Cosine at a nonzero rational argument is transcendental.

theorem FloatLib.Numerics.Enclosure.transcendental_sin_ratCast (q : ℚ) (hq : q ≠ 0) : Transcendental ℚ (Real.sin ↑q)

Sine at a nonzero rational argument is transcendental.

theorem FloatLib.Numerics.Enclosure.cos_ratCast_ne_zero (q : ℚ) (hq : q ≠ 0) : Real.cos ↑q ≠ 0

A nonzero rational argument cannot be a pole of tangent.

theorem FloatLib.Numerics.Enclosure.transcendental_tan_ratCast (q : ℚ) (hq : q ≠ 0) : Transcendental ℚ (Real.tan ↑q)

Tangent at a nonzero rational argument is transcendental.

theorem FloatLib.Numerics.Enclosure.irrational_sin_ratCast (q : ℚ) (hq : q ≠ 0) : Irrational (Real.sin ↑q)

Sine at a nonzero rational input cannot equal a rational rounding boundary.

theorem FloatLib.Numerics.Enclosure.irrational_cos_ratCast (q : ℚ) (hq : q ≠ 0) : Irrational (Real.cos ↑q)

Cosine at a nonzero rational input cannot equal a rational rounding boundary.

theorem FloatLib.Numerics.Enclosure.irrational_tan_ratCast (q : ℚ) (hq : q ≠ 0) : Irrational (Real.tan ↑q)

Tangent at a nonzero rational input cannot equal a rational rounding boundary.

theorem FloatLib.Numerics.Enclosure.irrational_arctan_ratCast (q : ℚ) (hq : q ≠ 0) : Irrational (Real.arctan ↑q)

Inverse tangent at a nonzero rational input is irrational.

theorem FloatLib.Numerics.Enclosure.irrational_arcsin_ratCast (q : ℚ) (hq : q ≠ 0) (hlower : -1 ≤ q) (hupper : q ≤ 1) : Irrational (Real.arcsin ↑q)

Inverse sine at a nonzero rational in its real domain is irrational.

theorem FloatLib.Numerics.Enclosure.irrational_arccos_ratCast (q : ℚ) (hq : q ≠ 1) (hlower : -1 ≤ q) (hupper : q ≤ 1) : Irrational (Real.arccos ↑q)

Inverse cosine is irrational throughout its rational real domain except at 1.