Rational-power comparison using logarithm bounds

Clearing an exponent's denominator is exact, but can create enormous integers even when the input rationals are small. Bounds for exponent * log base - log target often decide the same comparison with much less work. An interval that contains zero leaves the comparison undecided; the exact algebraic comparator then handles it, including equality.

The degree controls only the preliminary bound computation. It is never used to guess a result or to replace an undecided comparison with a rounded approximation.

def FloatLib.Numerics.RationalPower.logDifference (base exponent target : ℚ) (degree : ℕ) : RationalInterval

Enclose the logarithm of a power divided by a target, for positive base and target.

def FloatLib.Numerics.RationalPower.compareWithEnclosure (base exponent target : ℚ) (degree : ℕ) : Ordering

Compare a rational real power with a rational target, using bounds before exact arithmetic.

The semantic domain has base > 0; the target and exponent may have either sign. Exact integer-power comparison remains the fallback, so hard cases can still require large integers.