Iterates Factorial Hessian

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_hessian_factorial_product_le (n : ℕ) : ↑(n + 1).factorial * ↑(n + 3).factorial ≤ 2 * ↑(n + 2).factorial ^ 2

The material Hessian and its L2 partner cost the same factorial order, up to an absolute factor; the cancellation gains no factorial denominator.