Irrationality of exponentials at nonzero rational arguments

Adaptive rounding needs more than convergent intervals: an interval can straddle an exact rounding boundary forever. For the exponential at a nonzero rational argument, irrationality rules out that case.

The transcendence theorem in Elementary.Transcendental supplies the non-boundary fact. Inverting the exponential gives the corresponding logarithm result, with log 1 = 0 handled separately.

theorem FloatLib.Numerics.Enclosure.irrational_exp_intCast (m : ℤ) (hm : m ≠ 0) : Irrational (Real.exp ↑m)

The exponential of a nonzero integer is irrational.

theorem FloatLib.Numerics.Enclosure.irrational_exp_ratCast (q : ℚ) (hq : q ≠ 0) : Irrational (Real.exp ↑q)

A nonzero rational input has an irrational exponential. The zero case is exactly 1.

theorem FloatLib.Numerics.Enclosure.irrational_log_ratCast (q : ℚ) (hq : 0 < q) (hqone : q ≠ 1) : Irrational (Real.log ↑q)

A positive rational input other than 1 has an irrational natural logarithm.