Exact shift gains and the final coarse factorial splitting for finite packets.

theorem EulerGevrey.majorant_succ_identity (R : ℝ) (d n : ℕ) : majorant R (d + 1) n = R * ↑(n + d + 1) ^ 2 * majorant R d n

theorem EulerGevrey.majorant_mono_shift (R : ℝ) (hR : 1 ≤ R) (d D n : ℕ) (h : d ≤ D) : majorant R d n ≤ majorant R D n

theorem EulerGevrey.linear_grade_cost_absorbed (C R : ℝ) (hC : 0 ≤ C) (hR : C ≤ R) (p d n : ℕ) (hd : 0 < d) (hpd : p ≤ d) : C * ↑p * majorant R (d - 1) n ≤ majorant R d n

A single spare shift pays a linear number of grade terms at one fixed radius.

theorem EulerGevrey.factorial_sum_split (n d : ℕ) : (n + d).factorial ≤ 2 ^ (n + d) * n.factorial * d.factorial

theorem EulerGevrey.majorant_coarse_split (R : ℝ) (hR : 0 ≤ R) (d n : ℕ) : majorant R d n ≤ (4 * R) ^ d * ↑d.factorial ^ 2 * majorant (4 * R) 0 n

Used once at the final coarse split, or for a fixed coefficient shift.