Actual gradient jets from velocity jets through the current material level.

theorem AVenhance.Infra.Section4.amnr_velocityGradient_mixed_abs_le_of_bounded_velocity_jets {b : AmnrSpace → Homogenization.Vec 2} {S H V Kv Cb : ℝ} {N : ℕ} (hb : ContDiff ℝ (↑⊤) b) (hS : 0 ≤ S) (hH : 0 ≤ H) (hV : 0 ≤ V) (hKv : 0 ≤ Kv) (hCb : 0 ≤ Cb) (hVS : V * S = H) (α : List (Fin 2)) (n : ℕ) (hbudget : α.length + 2 * n + 2 ≤ N) (i p : Fin 2) (z : AmnrSpace) (hv : ∀ (η : List (Fin 2)), ∀ r ≤ n, amnrMixedWord η r ≠ [] → η.length + 2 * r + 1 ≤ N → |amnrWord b (amnrMixedWord η r) (fun (y : AmnrSpace) => b y i) z| ≤ Kv * V * S ^ η.length * H ^ r) (hB : ∀ (j q : Fin 2) (η : List (Fin 2)), ∀ r < n, η.length + 2 * r + 2 ≤ N → |amnrWord b (amnrMixedWord η r) (amnrVelocityGradient b j q) z| ≤ Cb * H * S ^ η.length * H ^ r) : |amnrWord b (amnrMixedWord α n) (amnrVelocityGradient b i p) z| ≤ (1 + 2 ^ N * Cb) ^ n * Kv * H * S ^ α.length * H ^ n

Bounded velocity jets through the current level and strictly lower gradient jets imply the actual gradient bound. Centering removes only the scalar value at the evaluation point, and every derivative budget is retained.