The H_n half of the zoom force terms

The receding vorticity equation carries the force term λ^4 λ^{2h} (curl f)_θ at the recentred point. This module attaches the missing bound and its vanishing in the zoom scale, the companion of abs_zoomForce_le and tendsto_zoomForce_bound_nhdsWithin_zero for the other force term.

theorem CIV.abs_recedingForce_le {lam h rc zc : ℝ} (hlam : 0 < lam) {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {M : ℝ} (hM : ∀ z ∈ unitCylinder, ∀ (i : Fin 3) (α : Fin 3 → ℕ), α 0 + α 1 + α 2 ≤ 2 → |multiPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => f w i) α z| ≤ M) {p : (ℝ × ℝ) × ℝ} (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : |lam ^ 4 * lam ^ (2 * h) * curlComp f 1 (zoomPointRec lam h rc zc p)| ≤ 2 * M * (lam ^ 4 * lam ^ (2 * h))

|H_n| ≤ 2 M λ^4 λ^{2h} at every recentred point of the unit cylinder, uniformly in the point: the azimuthal vorticity of a C²-bounded force is bounded by 2 M (abs_azimuthalVorticity_le_of_forceC2Bounded), and λ^4 λ^{2h} ≥ 0 for λ > 0.

theorem CIV.abs_recedingForce_le_of_forceC2Bounded {lam h rc zc : ℝ} (hlam : 0 < lam) {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hMf : ForceC2Bounded f) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (p : (ℝ × ℝ) × ℝ), zoomPointRec lam h rc zc p ∈ unitCylinder → |lam ^ 4 * lam ^ (2 * h) * curlComp f 1 (zoomPointRec lam h rc zc p)| ≤ C * (lam ^ 4 * lam ^ (2 * h))

The ForceC2Bounded form of abs_recedingForce_le, with a nonnegative constant depending only on the force, matching the shape of abs_zoomForce_le.

theorem CIV.tendsto_recedingForce_bound_nhdsWithin_zero {C h : ℝ} (hh0 : 0 ≤ h) : Filter.Tendsto (fun (lam : ℝ) => C * (lam ^ 4 * lam ^ (2 * h))) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

The bound of abs_recedingForce_le tends to zero as λ → 0⁺, since λ^4 λ^{2h} = λ^{4 + 2h} and 4 + 2h > 0. This is the uniform vanishing of the H_n term.