Euclidean-norm annulus bound from per-component multiPartial bounds

lem:aniso:annulus supplies order-≤2 per-component multiPartial bounds on the regular annulus. The two theorems below bridge that per-component form to the Euclidean-norm form that swirl_bound_of_annulus_bound (eq:aniso:closure:w) requires: the first supplies the direct conversion, the second applies it to obtain the swirl bound eq:aniso:closure:w without a separate norm-form hypothesis on the annulus.

theorem CIV.exists_vec3EuclideanNorm_bound_of_multiPartial_le {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Rm Rp t₀ M : ℝ} (hM : 0 ≤ M) (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α (x, t)| ≤ M) (x : CKN.Foundation.Parabolic.Vec3) : Rm < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rp → ∀ t ∈ Set.Ioo t₀ 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ≤ 3 * M

The Euclidean-norm swirl bound eq:aniso:closure:w derived directly from lem:aniso:annulus's own order-≤2 per-component conclusion, without a separate norm-form hypothesis on the annulus.

theorem CIV.swirl_bound_of_annulus_bound_of_multiPartial_le {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsol : IsClassicalSolutionOn u p f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (hfaxi : IsAxisymmetricOn f unitCylinder) (Mf : ℝ) (hMf : ∀ z ∈ unitCylinder, |f z 1| ≤ Mf) {Rlo Rhi t₀ M Rstar : ℝ} (hM : 0 ≤ M) (hbound : ∀ (x : CKN.Foundation.Parabolic.Vec3), Rlo < CKN.Foundation.Parabolic.vec3EuclideanNorm x → CKN.Foundation.Parabolic.vec3EuclideanNorm x < Rhi → ∀ t ∈ Set.Ioo t₀ 0, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w i) α (x, t)| ≤ M) (hR : 0 < Rstar ∧ Rstar < 1) (hRlo : Rlo < Rstar) (hRhi : Rstar < Rhi) (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) {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 (3 * M) Mi + (-t₀) ^ η * Mf * (t - t₀)