Fixed bounded maps preserve the same external-word radius for actual cylinder paths.

theorem EulerCylinderConstantMap.pathMap_block_bound (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {K : Type u_3} [TopologicalSpace K] [CompactSpace K] {ι : Type u_4} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (q : ℕ) (L : E →L[ℝ] F) (p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P E))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((pathMap P L) p)) n a ≤ ‖L‖ * EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) n a