The divergence of an axisymmetric field in cylindrical form

On the meridional plane {x₂ = 0} away from the axis, the Cartesian divergence of a smooth axisymmetric field is the cylindrical divergence ∂_r u_r + u_r/r + ∂_z u_z, the left-hand side of eq:aniso:scalar:nse:div. The only input is the θ-derivative relation ∂₂u₂ = u_r/r of spatialPartial_one_one_meridional; the identity is pointwise and does not use the equation.

theorem CIV.sum_spatialPartial_meridional {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) (hplane : z.1 1 = 0) (hr : z.1 0 ≠ 0) : ∑ j : Fin 3, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w j) j z = CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 z + u z 0 / z.1 0 + CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2 z

On the meridional plane, off the axis, the Cartesian divergence of a smooth axisymmetric field is the cylindrical divergence of eq:aniso:scalar:nse:div.