Termination of adaptive elementary comparison

The Taylor degree doubles at each refinement. Positive rational arguments other than 1 have irrational logarithms, so the convergent enclosures eventually exclude any rational boundary. The exactly representable value log 1 = 0 is handled before this search. The exponential argument is analogous, with exp 0 = 1 handled separately.

theorem FloatLib.Numerics.Enclosure.exists_log_separating (argument boundary : ℚ) (hpositive : 0 < argument) (hone : argument ≠ 1) : ∃ (n : ℕ), Comparison.Separates (log argument (2 ^ n)) boundary

The adaptive logarithm comparison terminates at every rational boundary.

theorem FloatLib.Numerics.Enclosure.exists_exp_separating (argument boundary : ℚ) (hnonzero : argument ≠ 0) : ∃ (n : ℕ), Comparison.Separates (exp argument (2 ^ n)) boundary

The adaptive exponential comparison terminates away from its exact zero-input case.