RelativeError: isolate the small-scale exponential absorption

The parameter estimate is stated separately from the scalar low/high recombination. Its numeric hypothesis records the choice of the scale parameter and the eventual domination of a polynomial loss by an exponential.

theorem AVenhance.Infra.Section5.RelativeError.e44_parameter_exponential_absorption {ε p δ c A Cν ν r R : ℝ} (hε : 0 < ε) (hc : 0 < c) (hA : 0 < A) (hCν : 0 ≤ Cν) (hr : 0 < r) (hν : (√ν)⁻¹ ≤ Cν * ε.rpow (-p)) (hscale : ε.rpow (-δ) ≤ R / r) (hnumeric : Cν * ε.rpow (-p) * Real.exp (-c * A * ε.rpow (-δ)) ≤ 1) : (√ν)⁻¹ * Real.exp (-c * R * (A / r)) ≤ 1

Convert the scale-ratio and diffusivity bounds into the explicit exponential absorption used by e44_combine_low_mode_and_analytic_tail.