Material transport of the flow-pulled iterate gradient.

theorem AVenhance.Infra.Section5.final_iterate_pulled_gradient_transport {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm κprev : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (l : ℤ) {t : ℝ} (ht : 0 < t) (y : Homogenization.Vec 2) (i : Fin 2) : deriv (fun (r : ℝ) => G I hΦ m (T (Nstar β)) l r (I.xFlow hΦ m l r y) i) t = (I.flowGrad hΦ m l t (I.xFlow hΦ m l t y)).mulVec (gradDiv (fun (r : ℝ) (z : Homogenization.Vec 2) => (I.Kmat κm m r + I.sMat hΦ m κm r z).mulVec (spaceGrad (T (Nstar β) r) z) + iterateError I hΦ m κm κprev T r z) t (I.xFlow hΦ m l t y)) i

The pulled gradient of the last T-iterate satisfies the source transport identity e.tbm1.two. The forcing from the finite iteration tail is retained in the divergence, exactly as in the source's e_{m-1}.