Executable interval and analytic enclosures

Rational interval arithmetic and exponential, logarithmic, and trigonometric kernels, with proofs that their computed endpoints enclose the exact real values. Concrete numerical formats can refine these bounds until they determine a rounding decision.

Interval also accepts arbitrary endpoint representations. Partial outward-rounding contracts separate the common ordered-field enclosure proofs from a format's range and encoding.