Exactly rounded base-two and base-ten posit logarithms

For a base greater than one, comparing log_base x with a rational boundary q is equivalent to comparing x with base ^ q. The rational-power comparator decides this exactly, using proved logarithm bounds first and exact algebraic comparison when necessary.

The Plus1 functions form 1 + x exactly before any rounding. In particular a small posit argument is not lost by first adding it to a posit representation of one.

Reference: Posit Standard (2022), §§4.1, 4.2, 5.1 and 5.5, https://posithub.org/docs/posit_standard-2.pdf.

def FloatLib.Floats.Formats.Posit.Model.Logarithm.compareTarget (base argument candidate : ℚ) (degree : ℕ) : Ordering

Compare the logarithm of a positive argument with a rational rounding candidate.

def FloatLib.Floats.Formats.Posit.Model.Logarithm.roundRat (format : Format) (base argument : ℚ) : Model format

Round a rational-argument logarithm once; nonpositive arguments produce NaR.

The mathematical domain requires base > 1. The preliminary series degree follows the target width; correctness does not depend on this choice because an inconclusive bound uses exact algebraic comparison. Such fallback cases may require large intermediate integers.

def FloatLib.Floats.Formats.Posit.Model.Logarithm.apply {format : Format} (base offset : ℚ) (value : Model format) : Model format

Apply a logarithm after adding an exact rational offset to the decoded argument.

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

Base-two logarithm, rounded once; NaR and nonpositive inputs produce NaR.

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

Base-two logarithm of exact 1 + x; NaR and inputs at or below -1 produce NaR.

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

Base-ten logarithm, rounded once; NaR and nonpositive inputs produce NaR.

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

Base-ten logarithm of exact 1 + x; NaR and inputs at or below -1 produce NaR.