Linear integrated control of each actual material velocity term.

theorem AVenhance.Infra.Section4.iterate_truncated_velocity_word_term_linear_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {v : ℝ → Homogenization.Vec 2 → ℝ} {a : AmnrSpace → ℝ} {s : ℝ} (hs1 : s ≤ 1) (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (ha : ContinuousOn a (Set.Ici 0 ×ˢ Set.univ)) (r p : List (Fin 2)) (j : Fin 2) {D H G : ℝ} (hD : 0 ≤ D) (hH : 0 ≤ H) (hG : 0 ≤ G) (hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2), |iterateSpatialWord r (fun (y : Homogenization.Vec 2) => b t y j) x| ≤ D) (hEa : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, a z ^ 2 ≤ H ^ 2) (hEv : (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord p (v t))) ≤ G ^ 2) : |∫ (z : AmnrSpace) in iterateTruncatedCell s, a z * (iterateSpatialWord r (fun (y : Homogenization.Vec 2) => b z.1 y j) z.2 * spaceGrad (iterateSpatialWord p (v z.1)) z.2 j)| ≤ D * H * G

Each material commutator term uses one actual velocity jet and the actual lower scalar gradient energy. The second factor may be the primitive contracted preceding Hessian; only its natural L2 bound is needed.