The differential inequality eq:aniso:closure:tested

This module assembles the tested enstrophy balance of Regularity of asymptotically axisymmetric solutions to the 3D Navier–Stokes equations with analytic forcing, arXiv:2609.20803, from the three tested terms of CIV.Closure.EnstrophyBalanceTerms.

Substituting the Cartesian vorticity equation cartesian_vorticity_pde in the time derivative of Y splits it into a transport, a diffusion, a stretching and a force term. The first two are integrated by parts, the cutoff errors they leave behind are constants because ∇χ is supported where |u| and |ω| are bounded, and the force term is bounded by C (Y + 1). What remains is

½ Y' + M ≤ ∫ χ² (ω·∇u)·ω + C (Y + 1),

stated with deriv Y t, which is the form closure_gronwall_bound consumes.

Stage (iii): the tested enstrophy balance

theorem CIV.cutoff_enstrophy_balance {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) {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hχ : ContDiff ℝ (↑⊤) χ) (hχs : HasCompactSupport χ) (hχU : tsupport χ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 1) {t₀ : ℝ} (ht₀ : t₀ ∈ Set.Ioo (-1) 0) {A : Set CKN.Foundation.Parabolic.Vec3} (hAcl : IsClosed A) (hχA : ∀ x ∉ A, fderiv ℝ χ x = 0) {Mu Mω : ℝ} (hMu : 0 ≤ Mu) (hubd : ∀ x ∈ A, ∀ t ∈ Set.Ioo t₀ 0, ∀ (i : Fin 3), |u (x, t) i| ≤ Mu) (hωbd : ∀ x ∈ A, ∀ t ∈ Set.Ioo t₀ 0, ∀ (i : Fin 3), |vorticityField u (x, t) i| ≤ Mω) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Ioo t₀ 0, HasDerivAt (cutoffEnstrophy χ u) (deriv (cutoffEnstrophy χ u) t) t ∧ 1 / 2 * deriv (cutoffEnstrophy χ u) t + cutoffEnstrophyDissipation χ u t ≤ cutoffStretching χ u t + C * (cutoffEnstrophy χ u t + 1)

The tested enstrophy balance eq:aniso:closure:tested. For a classical solution with a C²-bounded force and a cutoff χ whose gradient is supported in a closed set A on which |u| and |ω| are bounded on a time window (t₀, 0), the cutoff enstrophy Y is differentiable in time and

½ Y' + M ≤ ∫ χ² (ω·∇u)·ω + C (Y + 1)

on that same time window, with a constant depending only on χ, on the force bound and on the bounds on A. The derivative is written as deriv Y t, the form in which closure_gronwall_bound consumes it.