FloatLib.Floats.Interval

This namespace collects interval and enclosure utilities used across FloatLib:

• proof-friendly interval enclosures for rounding-on-ℝ formats,
• quantized intervals (endpoints snapped to a chosen Flocq-style rounded-real grid),
• format-generic executable endpoint intervals (BinaryInterchange.Model.Interval fmt).

The optional Arb-backed transcendental enclosure adapter is an explicit import: FloatLibTests.Arb.ModelTranscendentals.

The interval API belongs under FloatLib.Floats because format semantics and executable numerical code both depend on it. External validators remain under FloatLibTests, keeping their additional trust assumptions out of the public numerical core.

References

• IEEE 1788-2015 (interval arithmetic standard).
• Moore, Kearfott, Cloud, Introduction to Interval Analysis (2009).
• Rump, "INTLAB, INTerval LABoratory" (1999).
• Boldo & Melquiond, “Flocq” (ARITH 2011) for rounded-arithmetic-on-ℝ modeling.