Slice material calculus without assuming an evolution equation.

theorem AVenhance.Infra.Section4.iterate_material_spatial_word_expansion {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) : iterateSpatialWord w (amnrMaterial b u t) x = amnrMaterial b (fun (s : ℝ) => iterateSpatialWord w (u s)) t x + iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (t, x)

Exact material commutation on a positive-time slice, independently of a PDE.

theorem AVenhance.Infra.Section4.iterateWordMaterialError_zero (w : List (Fin 2)) (f : AmnrSpace → ℝ) : iterateWordMaterialError (fun (x : AmnrSpace) => 0) w f = 0

A vanishing drift has no material commutator at any spatial order.

theorem AVenhance.Infra.Section4.iterateSpatialWord_time {u : ℝ → Homogenization.Vec 2 → ℝ} (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) : iterateSpatialWord w (fun (y : Homogenization.Vec 2) => deriv (fun (s : ℝ) => u s y) t) x = deriv (fun (s : ℝ) => iterateSpatialWord w (u s) x) t

Ordered spatial derivatives commute with the actual time derivative. The scalar field need only be smooth on the positive-time domain.