Posit interval endpoints

intervalRounding brackets an exact rational using adjacent posit words for any supported width. It reuses the existing monotone-code bisection, rather than assuming the nearest posit rounder rounds outward. Negative bounds are obtained by reversing and negating the positive bounds. An exactly represented input receives a point enclosure.

The distinction from ordinary posit rounding matters at the extremes: a small positive value is bracketed by zero and minPos, while a magnitude beyond maxPos cannot have a finite posit enclosure and returns none. The exact endpoint check rejects NaR and any failed bracket. The common Numerics.Interval arithmetic uses this same checked rounding operation.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Posit.Interval (format : Format) : Type

An interval with exact-width posit words as endpoints.

def FloatLib.Floats.Formats.Posit.intervalCandidates (format : Format) (x : ℚ) : Interval format

Adjacent positive-code candidates, mirrored when the input is negative.

def FloatLib.Floats.Formats.Posit.intervalRounding (format : Format) : Numerics.OutwardRounding (Model format) ℚ

Checked outward rounding for arbitrary posit widths.

Overflow is reported as none; the standard's saturated maxPos output is not an upper bound for values beyond the format's range. No infinity is introduced into the posit representation.