Swirl Bound Cutoff Decay

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

theorem CIV.swirlCoeffAt_le_of_swirl_bound_ball (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (hfaxi : IsAxisymmetricOn f unitCylinder) (Mf : ℝ) (hMf : ∀ z ∈ unitCylinder, |f z 1| ≤ Mf) (Rstar : ℝ) (hR : 0 < Rstar ∧ Rstar < 1) (tη η : ℝ) (htη : tη ∈ Set.Ioo (-1) 0) (hη : 0 < η) (hG : ∀ t ∈ Set.Ioo tη 0, ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar → |radialQuotient u (meridional x₁ x₃, t)| ≤ η / -t) (Mb : ℝ) (hbdry : ∀ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm x = Rstar → ∀ t ∈ Set.Ioo tη 0, |u (x, t) 1| ≤ Mb) (Mi : ℝ) (hinit : ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, |u (x, tη) 1| ≤ Mi) : ∃ (Cη : ℝ), 0 ≤ Cη ∧ ∀ t ∈ Set.Ioo tη 0, ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, x 0 ≠ 0 ∨ x 1 ≠ 0 → |swirlCoeffAt u (x, t)| ≤ Cη * (-t) ^ (-η)

Reduction of eq:aniso:closure:w's swirl bound to the single-power decay shape W t ≤ C_η (−t)^{−η} consumed by the Grönwall step of lem:aniso:closure.

The raw bound from CIV.swirl_bound_ball reads (−t)^η |swirlCoeffAt u (x,t)| ≤ (−t_η)^η max(M_b, M_i) + (−t_η)^η M_f (t − t_η). Since t − t_η < −t_η for every t < 0 and M_f ≥ 0 (forced by hMf), the accumulated-source term is bounded by its value at t = 0⁻, yielding a single constant C_η := (−t_η)^η max(M_b, M_i) + (−t_η)^{η+1} M_f for which dividing the raw bound by (−t)^η lands exactly on C_η (−t)^{−η}.