Exactly rounded integer roots of posits

For positive degree, raising a nonnegative candidate to that degree preserves order. Exact rational powers therefore decide which side of every posit rounding boundary contains the root, even when the root is irrational. The shared comparator rounder supplies the bisection, saturation, and appended-bit tie rule. Negative degrees invert the exact radicand before the search.

Reference

• Posit Standard (2022), §§4.1, 5.1 and 5.8

@[inline]

def FloatLib.Floats.Formats.Posit.Model.RootRounding.compareRoot (radicand : ℚ) (degree : ℕ) (candidate : ℚ) : Ordering

Compare a nonnegative root with a rational candidate using exact integer powers.

For positive degree and nonnegative radicand, this is real comparison with the root. Negative candidates lie below it. At zero, compare the radicand with zero directly, preserving zero and nonpositive-input handling even outside the positive-degree contract.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.RootRounding.round (format : Format) (radicand : ℚ) (degree : ℕ) : Model format

Model-valued exact root rounding, with positive degree as its semantic domain.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.rootN {format : Format} (value : Model format) (degree : ℤ) : Model format

Integer root, rounded once, choosing the nonnegative root for even degrees and the signed real root for odd degrees. NaR inputs, degree zero, negative inputs with even degree, and zero inputs with negative degree produce NaR.