Stretching Split

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.stretching_eq_stretchGTerm {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {x : CKN.Foundation.Parabolic.Vec3} {t : ℝ} (hz : (x, t) ∈ unitCylinder) (hoff : polarR x ≠ 0) : ∑ i : Fin 3, ∑ j : Fin 3, curlComp u j (x, t) * CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) j (x, t) * curlComp u i (x, t) = stretchGTerm u x t + CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 (meridional (polarR x) (x 2), t) * curlComp u 0 (meridional (polarR x) (x 2), t) * curlComp u 2 (meridional (polarR x) (x 2), t) - 2 * stretchAngularSwirl u x t * curlComp u 1 (meridional (polarR x) (x 2), t)

The vortex-stretching term ∑ᵢ ∑ⱼ ωⱼ ∂ⱼ uᵢ ωᵢ splits into stretchGTerm and stretchAngularSwirl: the former is the "G-term" (first three terms of eq:aniso:closure:stretch plus the ∂_z u_r mixed term), the latter is the angular swirl factor u_θ · (ω_r / r). The proof moves to the meridional representative via exists_rotZ_polarR and stretching_rotZ_invariant, applies stretching_meridional to expand the sum, then unfolds the two definitions and uses radialQuotient's hoff branch to match by ring.