Scalar diffusion energies from actual one-higher gradient energies.

theorem AVenhance.Infra.Section4.iterate_word_laplacian_sq_le {u : Homogenization.Vec 2 → ℝ} (w : List (Fin 2)) (x : Homogenization.Vec 2) : spaceLap (iterateSpatialWord w u) x ^ 2 ≤ 2 * ∑ k : Fin 2, Homogenization.vecNormSq (spaceGrad (iterateSpatialWord (k :: w) u) x)

The scalar diffusion square uses exactly the two one-higher word gradients.

theorem AVenhance.Infra.Section4.iterate_word_laplacian_energy_bound {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) {G : ℝ} (hE : ∀ (k : Fin 2), (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord (k :: w) (u t))) ≤ G ^ 2) : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, spaceLap (iterateSpatialWord w (u z.1)) z.2 ^ 2 ≤ 4 * G ^ 2

Full scalar diffusion energy is derived from actual scalar gradients.