The actual gradient diffusion term as an ordered two-spatial contraction.

theorem AVenhance.Infra.Section4.amnr_classical_gradient_smooth_infty {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κ F u₀ u) (i : Fin 2) : ContDiffOn ℝ (↑⊤) (amnrTGradient u i) (Set.Ioi 0 ×ˢ Set.univ)

Actual classical gradients have all local smoothness orders; this is independent of the finite quantitative source jet budget.

theorem AVenhance.Infra.Section4.amnr_classical_gradient_diffusion {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κ F u₀ u) (B : AmnrSpace → Homogenization.Vec 2) (i : Fin 2) {z : AmnrSpace} (hz : 0 < z.1) : spaceGrad (spaceLap (u z.1)) z.2 i = ∑ q : Fin 2, amnrWord B [some q, some q] (amnrTGradient u i) z

Gradient diffusion is precisely the ordered coordinate Laplacian of the actual gradient field, on the full positive-time spatial slice.