Rational interval arcsine and arccosine

Arcsine reduces an interior endpoint to atan (x / sqrt (1 - x²)). Integer square-root bounds enclose the denominator, and the rational arctangent kernel encloses the quotient. The endpoints -1 and 1 use the proved enclosure of π/4 instead of dividing by zero. Arccosine follows from π/2 - asin x, with an exact zero at x = 1.

Both operations reject intervals extending outside [-1, 1]. The Taylor degree terms controls the arctangent and π enclosures; precision is the number of fractional binary digits in the square-root bounds. An interior point returns none if those bounds cannot separate its square root from zero. InverseTrigProof proves containment over the reals.

def FloatLib.Numerics.Interval.Internal.asinPointBounds? (x : ℚ) (terms precision : ℕ) : Option (Interval ℚ)

Enclose a rational arcsine value, treating the two endpoints and zero explicitly.

def FloatLib.Numerics.Interval.asinBounds? (I : Interval ℚ) (terms precision : ℕ) : Option (Interval ℚ)

Enclose arcsine on an ordered interval contained in [-1, 1], including both endpoints.

A point interval is evaluated once, and zero gives the exact interval [0, 0]. Invalid input bounds or a square-root lower bound that is too coarse return none.

def FloatLib.Numerics.Interval.acosBounds? (I : Interval ℚ) (terms precision : ℕ) : Option (Interval ℚ)

Enclose arccosine on an ordered interval contained in [-1, 1].

The exact input [1, 1] gives [0, 0]. Other inputs use π/2 - asin x and the known nonnegativity of arccosine. Domain and precision failures are the same as for asinBounds?.