The gradient-squared identity for axisymmetric fields on the meridional plane

On the meridional plane {x₂ = 0} away from the axis, the full Cartesian gradient-squared ∑ᵢ ∑ⱼ (∂ⱼ vᵢ)² splits into the meridional part ∑ᵢ ((∂₁ vᵢ)² + (∂₃ vᵢ)²) plus the angular contribution (v₀² + v₁²) / r². This is eq:aniso:closure:gradient.

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

For an axisymmetric field on the meridional plane, off the axis, the full Cartesian gradient-squared equals the meridional gradient-squared plus the 1/r² angular contribution.