Ordered correction estimates from canonical lower-level jets.

theorem AVenhance.Infra.Section4.amnrMaterialError_spatial_abs_le_of_canonical_lower_bounds {b c : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} {S H V Cv Cf Cb : ℝ} {N : ℕ} (hb : ContDiff ℝ (↑⊤) b) (hc : ContDiff ℝ (↑⊤) c) (hf : ContDiff ℝ (↑⊤) f) (hS : 0 ≤ S) (hH : 0 ≤ H) (hV : 0 ≤ V) (hCv : 1 ≤ Cv) (hCf : 0 ≤ Cf) (hCb : 0 ≤ Cb) (hVS : V * S = H) (α : List (Fin 2)) (n : ℕ) (hn : 1 ≤ n) (hbudget : α.length + 2 * n ≤ N) (z : AmnrSpace) (hv : ∀ (p : Fin 2) (η : List (Fin 2)) (r : ℕ), η.length + 2 * r + 1 ≤ N → r < n → |amnrWord c (amnrMixedWord η r) (amnrAdvectionVelocity b c p) z| ≤ Cv * V * amnrWeight S H (amnrMixedWord η r)) (hs : ∀ (η : List (Fin 2)) (r : ℕ), amnrMixedWord η r ≠ [] → η.length + 2 * r + 1 ≤ N → r < n → |amnrWord c (amnrMixedWord η r) f z| ≤ Cf * V * amnrWeight S H (amnrMixedWord η r)) (hB : ∀ (p i : Fin 2) (η : List (Fin 2)), ∀ r < n, η.length + 2 * r + 2 ≤ N → |amnrWord c (amnrMixedWord η r) (amnrVelocityGradient c p i) z| ≤ Cb * H * amnrWeight S H (amnrMixedWord η r)) : |amnrWord c (List.map some α) (amnrMaterialErrorValue b c f n) z| ≤ ↑(amnrMaterialErrorCardinality n * (n + 1) ^ α.length) * ((amnrNormalOrderConstant (N - 1) Cb (N - 1) * Cv) ^ n * (amnrNormalOrderConstant (N - 1) Cb (N - 1) * Cf) * V * S ^ α.length * H ^ n)

Canonical lower-level jets suffice for the actual material correction. The normal-order induction preserves every budget and needs only lower gradients.