Actual all-order material forcing energy for the increments.

theorem AVenhance.Infra.Section4.iterate_increment_word_TForcing_energy_bound {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => θprev z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hm : 1 ≤ m) (hκm : 0 < κm) (hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) (i : ℕ) (hi : i ≤ Nstar β) (w : List (Fin 2)) (D E : ℕ → ℝ) (hD : ∀ (t : ℝ) (x : Homogenization.Vec 2) (r : List (Fin 2)) (j k : Fin 2), |iterateMatrixWord (fun (y : Homogenization.Vec 2) => I.Kmat κm m t - κprev • 1 + I.sMat hΦ m κm t y) r x j k| ≤ D r.length) (hE : ∀ (r : List (Fin 2)), r.length ≤ w.length + 2 → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord r (iterateIncrement T i t))) ≤ E r.length) : (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord w (I.TForcing hΦ m κm κprev (iterateIncrement T i) t))) ≤ 64 * ∑ j ∈ Finset.range (w.length + 3), ↑((w.length + 2).choose j) ^ 2 * 2 ^ j * D j ^ 2 * E (w.length + 2 - j)

The actual differentiated TForcing gradient is bounded by preceding increment energies and actual coefficient jets. Natural integrability and regularity are discharged from the scalar carrier and flow smoothness.