Once-rounded integer powers and compound

Integer exponentiation takes place in the exact rational field. Compound also forms 1 + x exactly, so neither that addition nor the intermediate powers are rounded to the posit format. The integer exponent is fixed: exponent zero gives the constant one on every finite input, including a zero base. Zero to a negative power produces NaR. This differs from the two-posit pow operation, whose two-variable limit at (0, 0) is not unique.

Reference

• Posit Standard (2022), §§4.2, 5.1, 5.6 and 5.8

@[inline]

def FloatLib.Floats.Formats.Posit.Model.roundIntPower (format : Format) (base : ℚ) (exponent : ℤ) : Model format

Round an exact rational integer power once. Zero to a negative power produces NaR; this explicit domain check prevents the total field convention 0⁻¹ = 0 from defining the result. For the fixed exponent zero, the underlying function is the constant one.

@[inline]

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

Fixed integer power, rounded once. NaR propagates; zero to a negative power produces NaR.

@[inline]

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

Compound (1 + x) ^ n, rounded once. NaR propagates; x = -1 with negative exponent produces NaR. Exponent zero gives one even at x = -1, since the integer parameter is fixed in §5.8. Both the addition and exponentiation are exact before the final posit rounding.