The tested enstrophy inequality eq:aniso:closure:energy of lem:aniso:closure

This closes by one application of energy_inequality_of_mixed_term_bound_of_split, whose hsplit hypothesis is already discharged there (cutoffStretching_eq_stretchGTerm_add_mixed_sub_angular) and whose only remaining hypothesis, the mixed-term bound hmix, is exactly step_closure_mixed_term's conclusion. Both draw their velocity/vorticity bounds from the same order-≤ 2 annulus data of lem:aniso:annulus: the order-0 bounds hubd, hωbd that energy_inequality_of_mixed_term_bound_of_split needs are one clause of abs_apply_and_vorticityField_le_of_multiPartial_le applied to that same data, so nothing new is carried.

theorem CIV.step_closure_energy_inequality {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u p f unitCylinder) (hMf : ForceC2Bounded f) (haxi : IsAxisymmetricOn u unitCylinder) {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχs : HasCompactSupport χ) {ρ : ℝ} (hρU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 ρ) (hρ1 : CKN.Foundation.Parabolic.vec3Ball 0 ρ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) (hρpos : 0 < ρ) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo (-1) 0) {A : Set CKN.Foundation.Parabolic.Vec3} (hAcl : IsClosed A) (hχA : ∀ x ∉ A, fderiv ℝ χ x = 0) {Rm Rp Mu : ℝ} (hMu : 0 ≤ Mu) (hAsub : A ⊆ {x : CKN.Foundation.Parabolic.Vec3 | Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x ∧ CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp}) (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α (x, t)| ≤ Mu) {G W : ℝ → ℝ} (hGnn : ∀ (t : ℝ), 0 ≤ G t) (hG : ∀ t ∈ Set.Ioo t₀ 0, ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ → meridionalQuantity u (meridional x₁ x₃, t) ≤ G t) (hW : ∀ t ∈ Set.Ioo t₀ 0, ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ → |u (meridional x₁ x₃, t) 1| ≤ W t) : ∃ (Cstar : ℝ), 1 ≤ Cstar ∧ ∀ t ∈ Set.Ioo t₀ 0, deriv (cutoffEnstrophy χ u) t + cutoffEnstrophyDissipation χ u t ≤ Cstar * (G t + W t ^ 2 + 1) * (cutoffEnstrophy χ u t + 1)

eq:aniso:closure:energy. For a classical solution with a C²-bounded force, a cutoff χ supported in B(ρ), 0 < ρ, order-≤ 2 derivative bounds for u on the closed annulus A carrying ∇χ, a meridional bound G and a swirl bound W on B(ρ), there is C_* ≥ 1 with dY/dt + M ≤ C_* (G + W² + 1) (Y + 1) on (t₀, 0).