Actual previous material-error gradient in the induction's analytic weights.

theorem AVenhance.Infra.Section4.iterate_analytic_material_error_gradient_energy_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {v : ℝ → Homogenization.Vec 2 → ℝ} (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (a : ℕ) {B G r L : ℝ} (hL : 0 < L) (hg : 2 * (r / L) ^ 2 ≤ 1 / 2) (hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2) (q : List (Fin 2)), 1 ≤ q.length → ∀ (j : Fin 2), |iterateSpatialWord q (fun (y : Homogenization.Vec 2) => b t y j) x| ≤ B * ↑q.length.factorial * r ^ q.length) (hE : ∀ (q : List (Fin 2)), q.length ≤ w.length → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord q (v t))) ≤ G ^ 2 * (↑(q.length + a).factorial * L ^ q.length) ^ 2) : (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) ≤ 136 * B ^ 2 * r ^ 2 * G ^ 2 * (↑(w.length + 1 + a).factorial * L ^ w.length) ^ 2

The actual error-gradient energy uses only scalar gradient orders up to n. Its factorial has shift n+a+1, exactly fitting the next increment.