Exact derivative commutators for the material oscillatory terms.

theorem AVenhance.Infra.Section4.iterate_directional_commutator {f : AmnrSpace → ℝ} {d : AmnrSpace → AmnrSpace} {z : AmnrSpace} (hf : ContDiffAt ℝ 2 f z) (hd : DifferentiableAt ℝ d z) (e : AmnrSpace) : (fderiv ℝ (fun (y : AmnrSpace) => (fderiv ℝ f y) (d y)) z) e = (fderiv ℝ (fun (y : AmnrSpace) => (fderiv ℝ f y) e) z) (d z) + (fderiv ℝ f z) ((fderiv ℝ d z) e)

Commuting a fixed derivative past a variable directional derivative produces precisely the derivative of the direction field.

theorem AVenhance.Infra.Section4.iterate_spatial_material_commutator {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} {z : AmnrSpace} (hf : ContDiffAt ℝ 2 f z) (hb : DifferentiableAt ℝ b z) (i : Fin 2) : amnrOp b (some i) (amnrOp b none f) z = amnrOp b none (amnrOp b (some i) f) z + (fderiv ℝ f z) (0, (fderiv ℝ b z) (0, Homogenization.basisVec i))

The spatial/material commutator is the actual velocity-gradient term. This identity supplies both flow commutators in the primitive integration by parts; the velocity gradient is not an assumed error equation.