The public statement CIV.Main.forceUnderCore

This module proves the statement CIV.forceUnderCore (cor:interior:nonanalytic). At a singular point, the force violates eq:interior:force:analytic by the contrapositive of thm:main, so it does not vanish on the unit cylinder, since the zero force is analytic. If it vanished on a cylinder B(R') × (-δ', 0), the Navier–Stokes scaling by R = min R' δ' would carry the hypotheses of thm:main with the zero force to the unit cylinder (CIV.isSuitableWeakSolution_rescale_unitCylinder, CIV.globalEnergyClass_rescale, CIV.axisymmetricCore_rescale), and thm:main would make the origin regular (CIV.boundedNearOrigin_of_rescale).

theorem CIV.Main.forceUnderCore (q : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0) q u Du p f) (henergy : GlobalEnergyClass u Du p) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (hp : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p z) unitCylinder) (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (h : ℝ) (hh : 0 < h ∧ h < 1 / 2) (hMf : ForceC2Bounded f) (C : ℝ) (hC : 0 < C) (hbounds : AnisotropicBounds C h (angularMean u)) (hcore : ∀ t ∈ Set.Ioo (-1) 0, ∃ ρ ∈ Set.Ioo 0 1, IsAxisymmetricOn u (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) {t})) (hsing : ¬BoundedNearOrigin u) : ¬ForceSpatiallyAnalytic f ∧ (∃ z ∈ unitCylinder, f z ≠ 0) ∧ ∀ (R' δ' : ℝ), 0 < R' → R' ≤ 1 → 0 < δ' → δ' ≤ 1 → ∃ z ∈ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R') (Set.Ioo (-δ') 0), f z ≠ 0

The public statement of cor:interior:nonanalytic: at a singular point, under the other hypotheses of thm:main, the force is not spatially analytic, does not vanish identically on the unit cylinder, and does not vanish identically on any cylinder B(R') × (-δ', 0).