Homogeneous material derivatives from actual analytic scalar energies.

theorem AVenhance.Infra.Section4.iterate_material_velocity_scale {B r C κ L : ℝ} (hB : 0 ≤ B) (hr : 0 ≤ r) (hC : 0 ≤ C) (hκ : 0 < κ) (hL : 0 < L) (hscale : B * r ≤ C * κ * L ^ 2) : B ^ 2 * (r / L) ^ 2 ≤ C ^ 2 * κ ^ 2 * L ^ 2

The physical velocity-gradient scale is compared before any word or factorial estimates; this is pure real algebra.

theorem AVenhance.Infra.Section4.iterate_analytic_homogeneous_material_energy_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hsol : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) u₀ u) (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (a : ℕ) {B G r L C : ℝ} (hB : 0 ≤ B) (hr : 0 ≤ r) (hC : 0 ≤ C) (hκ : 0 < κ) (hL : 0 < L) (hg : 2 * (r / L) ^ 2 ≤ 1 / 2) (hscale : B * r ≤ C * κ * L ^ 2) (hjet : ∀ (t : ℝ) (x : Homogenization.Vec 2), ∀ p ∈ List.filter (fun (p : List (Fin 2) × List (Fin 2)) => decide (1 ≤ p.1.length)) (iterateSpatialSplits w), ∀ (j : Fin 2), |iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => b t y j) x| ≤ B * ↑p.1.length.factorial * r ^ p.1.length) (hE : ∀ (q : List (Fin 2)), q.length ≤ w.length + 1 → (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (iterateSpatialWord q (u t))) ≤ G ^ 2 * (↑(q.length + a).factorial * L ^ q.length) ^ 2) : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, amnrMaterial b (fun (t : ℝ) => iterateSpatialWord w (u t)) z.1 z.2 ^ 2 ≤ (8 + 64 * C ^ 2) * κ ^ 2 * G ^ 2 * (↑(w.length + 1 + a).factorial * L ^ (w.length + 1)) ^ 2

The actual homogeneous PDE bounds each material word using only actual one-higher scalar gradients and velocity jets. No material bound is assumed.