One literal source smallness threshold pays for the terminal coefficient bounds.

theorem AVenhance.Infra.Section4.amnr_source_smallness_threshold {L P e : ℝ} (hL : 0 ≤ L) (hP : 0 ≤ P) (he : 0 ≤ e) (hsmall : e ^ 2 ≤ ((2 + 320 * (L + 1) * (P + 1)) ^ 2)⁻¹) : P * e ^ 2 ≤ 1 / 2 ∧ L * (P * e ^ 2 + e) ≤ 9 / 160