One spare factorial shift pays all finite grade sums without changing the external radius.

theorem EulerGevrey.finite_cost_absorbed (C R : ℝ) (hC : 0 ≤ C) (hCR : C ≤ R) (m d n : ℕ) (hd : 0 < d) (hm : m ≤ d ^ 2) : C * ↑m * majorant R (d - 1) n ≤ majorant R d n

theorem EulerPacketCylinderField.Field.wordBound_finset_absorb {P T : ℝ} [Fact (0 < P)] {ι : Type u_1} (s : Finset ι) (f : ι → EulerPacketProfileRecursion.VectorField) (G : (i : ι) → Field P T (f i)) (q : ℕ) (R C : ℝ) (d : ℕ) (shift : ι → ℕ) (hR : 1 ≤ R) (hC : 0 ≤ C) (hCR : C ≤ R) (hd : 0 < d) (hcount : s.card ≤ d ^ 2) (hshift : ∀ i ∈ s, shift i < d) (hG : ∀ i ∈ s, (G i).WordBound q R C (shift i)) : (finsetSum s f G).WordBound q R 1 d

theorem EulerPacketShiftArithmetic.padded_grade_count (p : ℕ) (hp : 2 ≤ p) : 100 * (p + 2) ^ 2 ≤ meanForceShift p ^ 2 ∧ 100 * (p + 2) ^ 2 ≤ highForceShift p ^ 2

Even a padded quadratic family of grade terms is paid by the source's spare shift.