The swirl component of the scalar Navier–Stokes equation on the meridional plane

eq:aniso:scalar:nse:swirl is the swirl component of the momentum equation restricted to the meridional plane {x₂ = 0} off the axis. It states that the time derivative, the cylindrical convective term u_r ∂_r u_θ + u_z ∂_z u_θ + u_r u_θ / r, and the forcing balance the cylindrical Laplacian ∂_r² u_θ + r⁻¹ ∂_r u_θ + ∂_z² u_θ - r⁻² u_θ.

The angular derivative of the pressure drops out of the swirl component because the pressure of a classical solution with axisymmetric velocity and axisymmetric force is itself axisymmetric (pressure_rotZ_invariant). The rotation invariance of the pressure is therefore not a hypothesis here: only the axisymmetry of the force is.

theorem CIV.scalar_nse_swirl (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) (haxi : IsAxisymmetricOn u unitCylinder) (hfaxi : IsAxisymmetricOn f unitCylinder) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) z + u z 0 * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 0 z + u z 2 * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 2 z + u z 0 / z.1 0 * u z 1 = CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 0 0 z + CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 0 z / z.1 0 + CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 1) 2 2 z - u z 1 / z.1 0 ^ 2 + f z 1