Component energies are controlled by the actual vector gradient energy.

theorem AVenhance.Infra.Section4.iterate_component_sq_le_normSq (a : Homogenization.Vec 2) (j : Fin 2) : a j ^ 2 ≤ Homogenization.vecNormSq a

Every coordinate square lies below the vector square.

theorem AVenhance.Infra.Section4.iterate_word_gradient_component_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)) (j : Fin 2) : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, spaceGrad (iterateSpatialWord w (u z.1)) z.2 j ^ 2 ≤ spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (u t))

The actual word-gradient component inherits the full gradient energy bound, with integrability proved from the smooth scalar carrier.