All-order differentiated material equations for the actual increments.

theorem AVenhance.Infra.Section4.iterateSpatialWord_linear {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (c : ℝ) (w : List (Fin 2)) : (iterateSpatialWord w fun (x : Homogenization.Vec 2) => c * f x + g x) = fun (x : Homogenization.Vec 2) => c * iterateSpatialWord w f x + iterateSpatialWord w g x

Ordered differentiation distributes over the actual constant-coefficient linear combination in the increment equation.

theorem AVenhance.Infra.Section4.iterate_classical_material_word_equation {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F u₀ u) {t : ℝ} (ht : 0 < t) (hF : ContDiff ℝ (↑⊤) (F t)) (w : List (Fin 2)) : iterateSpatialWord w (amnrMaterial b u t) = fun (x : Homogenization.Vec 2) => κ * spaceLap (iterateSpatialWord w (u t)) x + iterateSpatialWord w (F t) x

Differentiate the actual classical PDE at every spatial order. This keeps D^w(D_t u) on the left; commuting D_t past the word is a subsequent step.