A single spare shift absorbs every fixed linear-operator amplitude at the same radius.

theorem EulerGevrey.amplitude_absorbed (A R : ℝ) (hA : 0 ≤ A) (hAR : A ≤ R) (d n : ℕ) : A * majorant R d n ≤ majorant R (d + 1) n

theorem EulerPacketCylinderField.Field.WordBound.absorb_amplitude {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (hA : 0 ≤ A) (hAR : A ≤ R) : G.WordBound q R 1 (d + 1)

theorem EulerPacketCylinderField.Field.WordBound.absorb_amplitude_to {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d e : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (hR : 1 ≤ R) (hA : 0 ≤ A) (hAR : A ≤ R) (hde : d + 1 ≤ e) : G.WordBound q R 1 e