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: it settles equality, as in log2 8 = 3, by exact roots and capped exponentiation, and separates every other boundary with proved logarithm bounds.

The Plus1 functions form 1 + x exactly before any rounding, so a small posit argument is not lost by first adding it to a posit 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 : ℚ) : 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. Each boundary comparison is the exact rational-power comparison of the argument with base ^ candidate.

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.