The material error is exactly the ordered velocity-gradient Leibniz error.

theorem AVenhance.Infra.Section4.iterateSpatialWord_transport {b : Homogenization.Vec 2 → Homogenization.Vec 2} {u : Homogenization.Vec 2 → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) (w : List (Fin 2)) (x : Homogenization.Vec 2) : iterateSpatialWord w (fun (y : Homogenization.Vec 2) => Homogenization.vecDot (b y) (spaceGrad u y)) x = ∑ j : Fin 2, (List.map (fun (p : List (Fin 2) × List (Fin 2)) => iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => b y j) x * spaceGrad (iterateSpatialWord p.2 u) x j) (iterateSpatialSplits w)).sum

The scalar transport term has its full ordered product expansion.

theorem AVenhance.Infra.Section4.iterate_time_slice_smooth {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => deriv (fun (s : ℝ) => u s x) t

Smoothness of the actual time derivative on a positive-time spatial slice.

theorem AVenhance.Infra.Section4.iterateWordMaterialError_transport {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {u : ℝ → Homogenization.Vec 2 → ℝ} (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) (w : List (Fin 2)) (x : Homogenization.Vec 2) : iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (t, x) = ∑ j : Fin 2, (List.map (fun (p : List (Fin 2) × List (Fin 2)) => iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => b t y j) x * spaceGrad (iterateSpatialWord p.2 (u t)) x j) (iterateSpatialSplits w)).sum - Homogenization.vecDot (b t x) (spaceGrad (iterateSpatialWord w (u t)) x)

The explicit recursive material error equals the velocity product error. Time commutation is proved, so no commuted equation is supplied as a premise.