Connect joint commutator words to the actual spatially differentiated PDE.

theorem AVenhance.Infra.Section4.iterate_amnrWord_spatial_slice {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} (hb : ContDiffOn ℝ (↑⊤) b U) (hf : ContDiffOn ℝ (↑⊤) f U) {t : ℝ} (ht : ∀ (x : Homogenization.Vec 2), (t, x) ∈ U) (w : List (Fin 2)) (x : Homogenization.Vec 2) : amnrWord b (List.map some w) f (t, x) = iterateSpatialWord w (fun (y : Homogenization.Vec 2) => f (t, y)) x

On a full spatial slice of an open domain, joint spatial words equal ordered spatial derivatives of the slice. Only positive-time germs are used.

theorem AVenhance.Infra.Section4.iterate_classical_commuted_word_equation {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F u₀ u) (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) (hF : ContDiff ℝ (↑⊤) (F t)) (w : List (Fin 2)) (x : Homogenization.Vec 2) : amnrMaterial b (fun (s : ℝ) => iterateSpatialWord w (u s)) t x = κ * spaceLap (iterateSpatialWord w (u t)) x + iterateSpatialWord w (F t) x - iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (t, x)

Exact all-order commuted material equation on the positive-time domain. The error is the explicit drift commutator; forcing regularity remains a structural input rather than a differentiated equation hypothesis.