Uniform-on-a-rectangle vanishing of the receding rescaled swirl coefficient

Uniform-on-a-rectangle vanishing of the recentred rescaled swirl coefficient S_n of eq:aniso:zoom:receding (the receding-axis analogue of eq:aniso:zoom:finite:source:b), as the recentring ratio A_n = r_n/λ_n → ∞ (with λ_n → 0⁺), from the circulation bound alone — the uniform-in-n, tested-against-a-fixed-rectangle strengthening of the fixed-point limit, matching Step 3's |S_n| ≤ C_Γ δ/(A_n + R) on a compact set instead of at one point.

theorem CIV.exists_forall_abs_zoomSRec_le_of_isCompact {h rc zc CΓ M lam : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {K : Set (ℝ × ℝ)} (hM : 0 < M) (hKM : ∀ y ∈ K, M ≤ rc / lam + y.1) {Z : ℝ} (hΓ : ∀ y ∈ K, |circulation u (zoomPointRec lam h rc zc ((y.1, y.2), Z))| ≤ CΓ) (y : ℝ × ℝ) : y ∈ K → |zoomSRec lam h rc zc u ((y.1, y.2), Z)| ≤ CΓ * lam ^ (2 * h) / M

theorem CIV.tendstoUniformlyOn_zoomSRec_of_tendsto_circulation_bound {h zc CΓ : ℝ} (u : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (lamSeq rcSeq : ℕ → ℝ) (hlam : ∀ (n : ℕ), 0 < lamSeq n) (hlam0 : Filter.Tendsto lamSeq Filter.atTop (nhds 0)) {K : Set (ℝ × ℝ)} (hK : IsCompact K) {M : ℕ → ℝ} (hMpos : ∀ (n : ℕ), 0 < M n) (hMtop : Filter.Tendsto M Filter.atTop Filter.atTop) (hKM : ∀ (n : ℕ), ∀ y ∈ K, M n ≤ rcSeq n / lamSeq n + y.1) {Z : ℝ} (hΓ : ∀ (n : ℕ), ∀ y ∈ K, |circulation (u n) (zoomPointRec (lamSeq n) h (rcSeq n) zc ((y.1, y.2), Z))| ≤ CΓ) (hh : 0 ≤ h) : TendstoUniformlyOn (fun (n : ℕ) (y : ℝ × ℝ) => zoomSRec (lamSeq n) h (rcSeq n) zc (u n) ((y.1, y.2), Z)) (fun (x : ℝ × ℝ) => 0) Filter.atTop K