The source's exponential tail follows quantitatively from its polynomial grade base.

theorem EulerPacketTailBound.grade_ratio_le_decay (k B : ℝ) (hk : 0 < k) (hB : B ≤ k ^ (1 / 100)) : B / k ≤ k ^ (-99 / 100)

theorem EulerPacketTailBound.grade_ratio_le_half (k B : ℝ) (hk : 4 ≤ k) (hB : B ≤ k ^ (1 / 100)) : B / k ≤ 1 / 2

theorem EulerPacketTailBound.normalized_tail_exponential (k B C X : ℝ) (hk : 4 ≤ k) (hB0 : 0 ≤ B) (hC0 : 0 ≤ C) (hB : B ≤ k ^ (1 / 100)) (hC : C ≤ k ^ (1 / 100)) (N : ℕ) (hX : 6 ≤ X) (hN : X - 1 ≤ ↑N) : 2 * C * k * B * (B / k) ^ (N + 1) ≤ Real.exp (-(7 / 10) * X * Real.log k)