Once-rounded powers with rational exponents

Powers are compared with rational posit boundaries using certified logarithm intervals. If a comparison remains undecided, an exact integer-power comparison resolves it, including equality. The preliminary series degree follows the output width; it does not limit correctness or guess a result. Negative integral powers use the same magnitude comparison and exact sign parity. Integer exponents with magnitude at most the output width use direct rational exponentiation, so simple integer powers do not pay for logarithm intervals.

This avoids denominator-sized integer powers when the interval decides the comparison. The exact fallback still has potentially impractical cost for large exponent numerators or denominators. There is no resource-bound completion guarantee.

The minus-one exponentials compare the power with candidate + 1. Thus subtraction is fused: the power is never first rounded to a posit, even when the result is very close to zero.

NaR propagates. Zero to a nonpositive exponent produces NaR. A negative base requires an integral exponent; all other dyadic exponents give nonreal powers. Finite posit exponents are dyadic, so this condition covers the real domain for negative posit bases.

References

• Posit Working Group, Standard for Posit Arithmetic (2022), March 2, 2022, Sections 4.1, 5.1, 5.5 and 5.6 (including footnote 10), https://posithub.org/docs/posit_standard-2.pdf.

@[noinline]

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

Round a positive-base rational power using certified comparisons with rational boundaries. The real semantics require 0 < base. Small integer exponents are evaluated exactly; otherwise an inconclusive enclosure uses exact algebraic fallback.

@[noinline]

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

Round an exact rational power once. Negative bases require integral exponents, and zero requires a positive exponent. Magnitude comparisons use enclosures before exact fallback.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.pow {format : Format} (base exponent : Model format) : Model format

General posit power with one final rounding and standard NaR propagation. Certified enclosures precede exact comparison; difficult fallback cases can remain expensive.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.exp2 {format : Format} (value : Model format) : Model format

Base-two exponential, rounded once using certified enclosures with exact comparison fallback.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.exp10 {format : Format} (value : Model format) : Model format

Base-ten exponential, rounded once using certified enclosures with exact comparison fallback.

@[noinline]

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

Round a positive-base power minus one with a single signed rounding. The real semantics require 0 < base; shifting the candidates preserves exact cancellation. Small integer exponents use exact rational exponentiation and subtraction before rounding.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.exp2Minus1 {format : Format} (value : Model format) : Model format

Base-two exponential minus one, with fused subtraction and NaR propagation.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.exp10Minus1 {format : Format} (value : Model format) : Model format

Base-ten exponential minus one, with fused subtraction and NaR propagation.