Rational trigonometric enclosures

The arctangent series is evaluated only for arguments in (-1, 1). Inversion and the arctangent addition identity at π/4 reduce every rational input to a series argument of magnitude at most one half. Machin's identity π / 4 = 4 * atan (1/5) - atan (1/239) supplies a rational enclosure of the constant; no rounded approximation to π enters the argument reduction.

The natural argument controls the number of terms. These operations return rational bounds, not rounded floating-point values. In particular, containment and convergence alone do not assert termination of a rounding search at an exact rounding boundary.

These kernels provide analytic foundations for the trigonometric functions listed in §5.5 of the Posit Standard (2022); they do not by themselves implement that section's rounding contract.

def FloatLib.Numerics.Enclosure.atanTaylor (x : ℚ) (n : ℕ) : ℚ

The first n terms of the arctangent series, evaluated exactly.

def FloatLib.Numerics.Enclosure.atanRadius (x : ℚ) (n : ℕ) : ℚ

A geometric majorant of the arctangent tail, valid for |x| < 1.

def FloatLib.Numerics.Enclosure.atanSmall (x : ℚ) (degree : ℕ) : RationalInterval

A rational enclosure of the arctangent on its open series domain.

def FloatLib.Numerics.Enclosure.piQuarter (degree : ℕ) : RationalInterval

A rational enclosure of π/4 using Machin's rapidly convergent arctangent identity.

def FloatLib.Numerics.Enclosure.atanUnit (x : ℚ) (degree : ℕ) : RationalInterval

Reduce an argument in [0, 1] to magnitude at most one half.

def FloatLib.Numerics.Enclosure.atanNonnegative (x : ℚ) (degree : ℕ) : RationalInterval

Inversion reduces a nonnegative rational argument to [0, 1].

def FloatLib.Numerics.Enclosure.atan (x : ℚ) (degree : ℕ) : RationalInterval

Enclose the arctangent of any rational argument, using oddness for negative inputs.

def FloatLib.Numerics.Enclosure.sinCoefficient (n : ℕ) : ℚ

The nth derivative of sine at zero: alternating signs on odd indices and zero otherwise.

def FloatLib.Numerics.Enclosure.cosCoefficient (n : ℕ) : ℚ

The nth derivative of cosine at zero: alternating signs on even indices and zero otherwise.

def FloatLib.Numerics.Enclosure.sinTaylor (x : ℚ) (degree : ℕ) : ℚ

The sine Taylor polynomial through the requested degree, with exact rational coefficients.

def FloatLib.Numerics.Enclosure.cosTaylor (x : ℚ) (degree : ℕ) : ℚ

The cosine Taylor polynomial through the requested degree.

def FloatLib.Numerics.Enclosure.trigRadius (x : ℚ) (degree : ℕ) : ℚ

Global Lagrange remainder bound, since every sine and cosine derivative is bounded by one.

def FloatLib.Numerics.Enclosure.restrictUnit (interval : RationalInterval) : RationalInterval

Intersect a trigonometric enclosure with the known range [-1, 1].

def FloatLib.Numerics.Enclosure.sin (x : ℚ) (degree : ℕ) : RationalInterval

Enclose sine at any rational argument using the global Taylor remainder.

The bound is valid even when the degree is too small to be informative. Large arguments can require large degrees; this baseline performs no reduction by an approximate multiple of π.

def FloatLib.Numerics.Enclosure.cos (x : ℚ) (degree : ℕ) : RationalInterval

Enclose cosine globally and intersect the Taylor bounds with its real range.