First spatial derivatives of material jets of the actual stream summands.

theorem AVenhance.Infra.Section4.amnr_nextStreamTerm_word_zero_off_large {β : ℝ} (I : Ingredients β) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (b : AmnrSpace → Homogenization.Vec 2) (w : List (Option (Fin 2))) (z : AmnrSpace) (hfar : tauPP β I.Λ m / 2 + tauP β I.Λ m < |z.1 - ↑(lIdx β I.Λ m k) * tauPP β I.Λ m|) : amnrWord b w (fun (y : AmnrSpace) => I.nextStreamTerm m φ hφ y.1 y.2 k) z = 0

A stream summand and all its differential words vanish beyond the large cutoff window. This support property applies to the actual construction.

theorem AVenhance.Infra.Section4.amnr_stream_timeAmplitude_derivative_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (k : ℤ) (ℓ : ℕ) (hℓ : ℓ ≤ Nstar β) (t : ℝ) : |iteratedDeriv ℓ (I.hatZetaML m (lIdx β I.Λ m k) * I.zetaMK m k) t| ≤ 2 ^ ℓ * I.Chat * I.Czeta * (tau β I.Λ m)⁻¹ ^ ℓ

All derivatives of the actual stream time amplitude have the fine rate.