Applying a finite outer word to the primitive gradient PDE.

theorem AVenhance.Infra.Section4.amnr_gradient_material_word_equation {U : Set AmnrSpace} (hU : IsOpen U) {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiffOn ℝ (↑⊤) b U) {g F : Fin 2 → AmnrSpace → ℝ} (hg : ∀ (p : Fin 2), ContDiffOn ℝ (↑⊤) (g p) U) {N : ℕ} (hF : ∀ (q : Fin 2), ContDiffOn ℝ (↑N) (F q) U) {κ : ℝ} (p : Fin 2) (hEq : Set.EqOn (amnrOp b none (g p)) (fun (z : AmnrSpace) => κ * ∑ q : Fin 2, amnrWord b [some q, some q] (g p) z + ∑ q : Fin 2, amnrWord b [some p, some q] (F q) z - ∑ q : Fin 2, amnrVelocityGradient b q p z * g q z) U) (w : List (Option (Fin 2))) (hw : w.length + 2 ≤ N) : Set.EqOn (amnrWord b (w ++ [none]) (g p)) (fun (z : AmnrSpace) => κ * ∑ q : Fin 2, amnrWord b (w ++ [some q, some q]) (g p) z + ∑ q : Fin 2, amnrWord b (w ++ [some p, some q]) (F q) z - amnrWord b w (fun (y : AmnrSpace) => ∑ q : Fin 2, amnrVelocityGradient b q p y * g q y) z) U

Finite-order flux regularity suffices to differentiate the primitive PDE. The two spatial letters are retained explicitly for the budget accounting.