Exact noncommuting material-power differences for the velocity induction.

theorem AVenhance.Infra.Section4.amnr_material_operator_change (b c : AmnrSpace → Homogenization.Vec 2) (f : AmnrSpace → ℝ) (z : AmnrSpace) : amnrOp b none f z - amnrOp c none f z = ∑ p : Fin 2, (b z p - c z p) * amnrOp c (some p) f z

The change of material operator is the actual fast advection, even for Lean's total Fréchet derivative.