Quantitative finite-jet induction for derived flow-transport coefficients.

theorem AVenhance.Infra.Section4.amnrWord_const {b : AmnrSpace → Homogenization.Vec 2} (w : List (Option (Fin 2))) (c : ℝ) : (amnrWord b w fun (x : AmnrSpace) => c) = if w = [] then fun (x : AmnrSpace) => c else 0

Every nonempty actual differential word annihilates a scalar constant.

theorem AVenhance.Infra.Section4.amnrWord_add_global {b : AmnrSpace → Homogenization.Vec 2} {f g : AmnrSpace → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (w : List (Option (Fin 2))) : amnrWord b w (f + g) = amnrWord b w f + amnrWord b w g

Addition commutes with actual ordered words when their smooth primitive functions supply every intermediate derivative.

theorem AVenhance.Infra.Section4.amnrFlowMaterialCoefficient_mixed_abs_le_of_gradient_bounds {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) b) {N : ℕ} {S H Cb : ℝ} (hS : 0 ≤ S) (hH : 0 ≤ H) (hCb : 0 ≤ Cb) {z : AmnrSpace} (hBb : ∀ (i p : Fin 2) (w : List (Option (Fin 2))), IsAmnrMixedWord w → amnrBudget w + 2 ≤ N → |amnrWord b w (amnrVelocityGradient b i p) z| ≤ Cb * H * amnrWeight S H w) (n : ℕ) (w : List (Option (Fin 2))) (hw : IsAmnrMixedWord w) (hbudget : amnrBudget w + 2 * n ≤ N) (q p : Fin 2) : |amnrWord b w (amnrFlowMaterialCoefficient b n q p) z| ≤ (1 + 2 ^ (N + 1) * Cb) ^ n * H ^ n * amnrWeight S H w

Every mixed jet of the derived flow-transport coefficient is bounded from the actual velocity-gradient jets. This generic conditional helper does not assert the primitive gradient bounds. Each induction level loses two units.