Exact comparisons with natural logarithms and exponentials

The logarithm comparator first tries a finite binary-grid enclosure. Inconclusive probes fall back to exact rational enclosures, doubling the Taylor degree until the ordering is known. The grid precision limits the precheck and never the result of the comparison. The imported termination proof is erased during compilation.

compareExp uses exp x < y ↔ x < log y for positive y. This avoids materializing an enormous exponential when the destination will saturate. prepareExp instead caches exponential enclosures for arguments in [-8, 8], and uses the logarithmic comparison outside that interval.

The constant log 2 needs no comparator of its own: prepareLog 2 compares it with rational boundaries and shares its enclosures across them.

def FloatLib.Numerics.ElementaryComparison.compareLog (argument boundary : ℚ) (hpositive : 0 < argument) : Ordering

Compare the natural logarithm of a positive rational with a rational boundary.

def FloatLib.Numerics.ElementaryComparison.compareExp (argument boundary : ℚ) : Ordering

Compare a rational-input exponential with any rational boundary.

def FloatLib.Numerics.ElementaryComparison.prepareLog (argument : ℚ) (levels : ℕ) (hpositive : 0 < argument) : Enclosure.Comparison.Prepared

Prepare a logarithm comparator that shares its first levels enclosures across boundaries. Deeper levels are computed on demand.

def FloatLib.Numerics.ElementaryComparison.prepareExp (argument : ℚ) (levels : ℕ) : Enclosure.Comparison.Prepared

Prepare an exponential comparator, sharing enclosures for arguments in [-8, 8].

Repeated squaring can create large rational intermediates even when the final comparison is easy. Outside this moderate interval the logarithm-of-boundary comparison avoids that growth. The threshold selects an algorithm. It does not restrict the function's domain or accuracy.