Correctness of power comparison from logarithm bounds

The real logarithm is strictly increasing on positive values. Consequently a strict sign certificate for the logarithm difference determines the original comparison. When no such certificate is available, the exact denominator-clearing theorem supplies the result.

theorem FloatLib.Numerics.RationalPower.contains_logDifference (base exponent target : ℚ) (degree : ℕ) (hbase : 0 < base) (htarget : 0 < target) : (logDifference base exponent target degree).Contains (Real.log (↑base ^ ↑exponent) - Real.log ↑target)

The executable interval contains the exact difference of real logarithms.

theorem FloatLib.Numerics.RationalPower.rpow_lt_of_logDifference_hi_neg (base exponent target : ℚ) (degree : ℕ) (hbase : 0 < base) (htarget : 0 < target) (hnegative : (logDifference base exponent target degree).hi < 0) : ↑base ^ ↑exponent < ↑target

A strictly negative upper bound proves that the real power is below the target.

theorem FloatLib.Numerics.RationalPower.lt_rpow_of_logDifference_lo_pos (base exponent target : ℚ) (degree : ℕ) (hbase : 0 < base) (htarget : 0 < target) (hpositive : 0 < (logDifference base exponent target degree).lo) : ↑target < ↑base ^ ↑exponent

A strictly positive lower bound proves that the target is below the real power.

theorem FloatLib.Numerics.RationalPower.compareWithEnclosure_eq_real (base exponent target : ℚ) (degree : ℕ) (hbase : 0 < base) : compareWithEnclosure base exponent target degree = cmp (↑base ^ ↑exponent) ↑target

The bounds and exact fallback together always return the real-power ordering.