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, so no rounded approximation to π enters the argument reduction.

The arctangent partial sums are evaluated by binary splitting with one final normalization. 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.

The Taylor coefficients follow the NIST Digital Library of Mathematical Functions: §4.19.E1 for sine, §4.19.E2 for cosine, and §4.24.E3 for arctangent. SinCosProof proves the remainder bounds using Mathlib's Taylor theorem. AtanProof bounds the arctangent tail by a geometric series and uses Mathlib's Machin identity to enclose π/4.

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

Sum of the first n terms of the arctangent series, in exact rational arithmetic.

@[csimp]

theorem FloatLib.Numerics.Enclosure.atanTaylor_eq_binarySplit : atanTaylor = Taylor.atan

The arctangent Taylor sum equals its evaluation by binary splitting.

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

Enclose atan x for x in [0, 1], with a series argument of magnitude at most one half.

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

Enclose atan x for nonnegative x, inverting arguments above one into [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 : ℕ) : ℚ

Sine Taylor polynomial through degree, with exact rational coefficients.

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

Cosine Taylor polynomial through 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, because 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.