Ordering estimates without an artificial velocity zero-order bound.

theorem AVenhance.Infra.Section4.amnrWord_centered_nonempty {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (w : List (Option (Fin 2))) (hw : w ≠ []) (z : AmnrSpace) : (amnrWord b w fun (y : AmnrSpace) => f y - f z) = amnrWord b w f

Centering a scalar at the evaluation point preserves every nonempty actual derivative word. The removed value is a global scalar constant.

theorem AVenhance.Infra.Section4.amnr_word_abs_le_of_nonempty_mixed_bounds_and_lower_gradients {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) {N cut : ℕ} {S H F Cb : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hF : 0 ≤ F) (hCb : 0 ≤ Cb) (z : AmnrSpace) (hfb : ∀ (α : List (Fin 2)) (n : ℕ), amnrMixedWord α 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))) (hw : w ≠ []) (hbudget : amnrBudget w ≤ N) (hcut : amnrMaterialCount w ≤ cut) : |amnrWord b w f z| ≤ amnrNormalOrderConstant N Cb N * F * amnrWeight S H w

Nonempty canonical jets and lower gradient levels control arbitrary nonempty words. No zero-order velocity amplitude is assumed.