The swirl bound eq:aniso:closure:w

The weighted swirl component ψ = (−t)^η u_θ obeys the parabolic equation weighted_swirl_pde off the axis, with zeroth-order coefficient γ = r⁻² + u_r/r + η/(−t). When η > 0 and the meridional quantity G is small enough that |u_r/r| ≤ η/(−t) on (t_η, 0) (hypothesis hG), γ ≥ 0, and CIV.axisMaximumPrinciple bounds ψ on the closed meridional half-disc by its parabolic boundary values plus the accumulated source. This file assembles that bound, first on the meridional plane (swirl_bound) and then, through the swirl coefficient swirlCoeffAt, at every off-axis point of the ball (swirl_bound_ball).

The chain rule through the meridional embedding

The weighted swirl profile and its translation into dr, dz, dtPast

The drift, zeroth-order coefficient and source, and the translated PDE

Embedding the meridional half-disc in the unit cylinder

The hypotheses of CIV.axisMaximumPrinciple for the swirl profile

The boundary bound, including the corner shared by the two pieces

The swirl bound, eq:aniso:closure:w, on the meridional plane

theorem CIV.swirl_bound (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) (t : ℝ) : t ∈ Set.Ioo tη 0 → ∀ (x₁ x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar → (-t) ^ η * |u (meridional x₁ x₃, t) 1| ≤ (-tη) ^ η * max Mb Mi + (-tη) ^ η * Mf * (t - tη)

The swirl bound eq:aniso:closure:w: for t ∈ (t_η, 0) and a meridional point in vec3Ball 0 R_*, the weighted swirl (−t)^η u_θ is bounded by its value on the parabolic boundary (−t_η)^η max(M_b, M_i) plus the accumulated weighted source (−t_η)^η M_f (t − t_η), derived by applying CIV.axisMaximumPrinciple at s := t and reading off its conclusion m + M (p.2 − t₁) there: since M := (−t_η)^η M_f bounds (−t)^η |f_θ| uniformly for t_η < t < 0 (monotonicity of (−t)^η, η > 0) and p.2 − t₁ = t − t_η at p = ((x₁, x₃), t), this is the sharp instantiation of the maximum principle's own bound, not a further relaxation of it.

theorem CIV.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) (t : ℝ) : t ∈ Set.Ioo tη 0 → ∀ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar, x 0 ≠ 0 ∨ x 1 ≠ 0 → (-t) ^ η * |swirlCoeffAt u (x, t)| ≤ (-tη) ^ η * max Mb Mi + (-tη) ^ η * Mf * (t - tη)

The swirl bound eq:aniso:closure:w at every off-axis point of vec3Ball 0 R_*, not only on the meridional plane. The raw Cartesian component u (x, t) 1 is not invariant under the rotations about the axis, so it is the swirl coefficient swirlCoeffAt u = Γ / r that carries the meridional conclusion of swirl_bound to a general point: writing x = Q_φ (r, 0, z) with r ≥ 0 (exists_rotZ_meridional), the point is off the axis exactly when r > 0, the rotation preserves the Euclidean norm, and swirlCoeffAt_rotZ_meridional identifies swirlCoeffAt u (x, t) with the meridional value u ((r, 0, z), t) 1 to which swirl_bound applies.