Normal ordering on the source's open positive-time domain.

theorem AVenhance.Infra.Section4.amnr_word_abs_le_on_of_finite_mixed_bounds_and_lower_gradients {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} {N cut : ℕ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiffOn ℝ (↑N) f U) {S H F Cb : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hF : 0 ≤ F) (hCb : 0 ≤ Cb) {z : AmnrSpace} (hz : z ∈ U) (hfb : ∀ (α : List (Fin 2)) (n : ℕ), α.length + 2 * n ≤ N → n ≤ cut → |amnrWord b (amnrMixedWord α n) f z| ≤ F * amnrWeight S H (amnrMixedWord α n)) (hBb : ∀ (p i : Fin 2) (α : List (Fin 2)), ∀ n < cut, α.length + 2 * n + 2 ≤ N → |amnrWord b (amnrMixedWord α n) (amnrVelocityGradient b p i) z| ≤ Cb * H * amnrWeight S H (amnrMixedWord α n)) (w : List (Option (Fin 2))) (hbudget : amnrBudget w ≤ N) (hcut : amnrMaterialCount w ≤ cut) : |amnrWord b w f z| ≤ amnrNormalOrderConstant N Cb N * F * amnrWeight S H w

Local temperature smoothness suffices for the quantitative normal-order estimate. The weighted budget and material cutoff are unchanged.