Classical solenoidality of smooth J fields

The J condition on a regularized velocity slice gives the pointwise divergence identity used in its high-order pressure cancellation.

theorem ESS.lps_smooth_isInJ_solenoidal {u : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hJ : CKN.IsInJ u) (hu : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => u x i) (x : CKN.Foundation.Parabolic.Vec3) : ∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => u y i) i x = 0

A spatially smooth J field is solenoidal at every point (eq:lps-regularized-Hm-identity).