Actual all-order material-gradient energy from its equation.

theorem AVenhance.Infra.Section4.iterate_commuted_material_gradient_energy_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F v : ℝ → Homogenization.Vec 2 → ℝ} {v₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ F v₀ v) (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (hFc : ContinuousOn (fun (z : AmnrSpace) => spaceGrad (iterateSpatialWord w (F z.1)) z.2) (Set.Ici 0 ×ˢ Set.univ)) : (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (amnrMaterial b (fun (s : ℝ) => iterateSpatialWord w (v s)) t)) ≤ ((2 * κ ^ 2 * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) => spaceLap (fun (y : Homogenization.Vec 2) => spaceGrad (iterateSpatialWord w (v t)) y j) x) + 4 * spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (F t))) + 4 * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (fun (y : Homogenization.Vec 2) => iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => v z.1 z.2) (t, y)) x

The actual commuted PDE yields the material-gradient energy estimate. Original forcing-jet continuity is structural; no energy estimate is assumed.