Forcing-gradient energy without pointwise scalar analytic hypotheses.

theorem AVenhance.Infra.Section4.iterate_word_forcing_gradient_flux_formula {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (w : List (Fin 2)) (x : Homogenization.Vec 2) (k : Fin 2) : spaceGrad (iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad v y))) x k = ∑ i : Fin 2, iterateWordFlux A v (i :: k :: w) x i

The gradient of the actual differentiated forcing is a sum of two explicit flux components at two additional derivative letters.

theorem AVenhance.Infra.Section4.iterate_word_forcing_gradient_flux_sq_bound {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (w : List (Fin 2)) (x : Homogenization.Vec 2) : Homogenization.vecNormSq (spaceGrad (iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad v y))) x) ≤ 2 * ∑ k : Fin 2, ∑ i : Fin 2, Homogenization.vecNormSq (iterateWordFlux A v (i :: k :: w) x)

Squaring this finite component sum costs two, with no dependence on n.