The divergence-form diffusion split for the actual stream velocity.

theorem AVenhance.Infra.Section5.frozen_stream_advDiffOp_divergence_split {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κ : ℝ) (u : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (hu : ContDiffAt ℝ 2 (u t) x) : advDiffOp (streamVel (Φ m)) κ u t x = deriv (fun (s : ℝ) => u s x) t + Homogenization.vecDot (streamVel (Φ (m - 1)) t x) (spaceGrad (u t) x) - vecDiv (fun (y : Homogenization.Vec 2) => (κ • 1 + psiTilde I hΦ m t y • sigmaMat).mulVec (spaceGrad (u t) y)) x

For the velocity recursion, the new-scale advection-diffusion operator splits into old-stream transport and the exact ψTilde_m divergence form diffusion.