Exact comparisons with natural logarithms and exponentials

The runtime compares rational enclosures, doubling the Taylor degree until the ordering is known. 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 direct exponential enclosures for arguments in [-8, 8], and uses the logarithmic comparison outside that interval.

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. Cached levels are reused across boundary queries; levels beyond this prefix 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.