The receding-axis rescaled azimuthal vorticity equation

This file completes the receding-axis zoom of CIV.Zoom.Receding with the rescaled azimuthal-vorticity equation eq:aniso:zoom:receding:equation, the receding preimage clause, and the circulation-based swirl-source bounds.

Every derivative in CIV.Zoom.Receding is stated over zoomPointRec, whose radial slot rc + lam * R differs from the finite-axis zoomPoint's lam * R by the constant offset rc. The scalar chain rules of CIV.Zoom.ScalarChainRule are stated concretely over zoomPoint, and only coincide with the recentred map after the substitution R ↦ R + rc / lam, which needs lam ≠ 0 — a hypothesis none of those chain rules carry. Rather than adding a lam ≠ 0 binder to CIV.Zoom.ScalarChainRule (which this file does not modify), the scalar chain rules below are restated directly for zoomPointRec, built from the same low-level pieces CIV.hasDerivAt_comp_spatialSlice_scalar and CIV.differentiableAt_timeSlice_of_isOpen, which are already stated for an arbitrary curve and already carry no nonvanishing hypothesis on the affine slope. The radial line uses CIV.hasDerivAt_meridional_fst_shift of CIV.Zoom.Receding, already proved there for an arbitrary offset; the vertical and time lines coincide verbatim with the finite-axis case, since only the radial slot of zoomPointRec carries an offset.

Scalar chain rules for the recentred zoom map

theorem CIV.hasDerivAt_zoomRecScalar_r (lam h rc zc : ℝ) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : HasDerivAt (fun (r : ℝ) => Phi (zoomPointRec lam h rc zc ((r, p.1.2), p.2))) (lam * CKN.spatialPartial Phi 0 (zoomPointRec lam h rc zc p)) p.1.1

Differentiating a scalar composed with zoomPointRec in the radial variable. The curve is the offset radial line hasDerivAt_meridional_fst_shift, so no lam ≠ 0 hypothesis is needed.

theorem CIV.hasDerivAt_zoomRecScalar_z (lam h rc zc : ℝ) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : HasDerivAt (fun (s : ℝ) => Phi (zoomPointRec lam h rc zc ((p.1.1, s), p.2))) (lam ^ (1 - 2 * h) * CKN.spatialPartial Phi 2 (zoomPointRec lam h rc zc p)) p.1.2

Differentiating a scalar composed with zoomPointRec in the vertical variable. The vertical slot of zoomPointRec carries the same offset zc as zoomPoint, so this is verbatim the finite-axis chain rule.

theorem CIV.hasDerivAt_zoomRecScalar_t (lam h rc zc : ℝ) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : HasDerivAt (fun (t : ℝ) => Phi (zoomPointRec lam h rc zc (p.1, t))) (lam ^ 2 * CKN.timePartial Phi (zoomPointRec lam h rc zc p)) p.2

Differentiating a scalar composed with zoomPointRec in the time variable. The time slot of zoomPointRec is lam ^ 2 * τ, exactly as for zoomPoint, independent of rc.

theorem CIV.dr_comp_zoomPointRec (lam h rc zc : ℝ) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dr (fun (q : (ℝ × ℝ) × ℝ) => Phi (zoomPointRec lam h rc zc q)) p = lam * CKN.spatialPartial Phi 0 (zoomPointRec lam h rc zc p)

∂_R of a scalar composed with zoomPointRec.

theorem CIV.dz_comp_zoomPointRec (lam h rc zc : ℝ) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dz (fun (q : (ℝ × ℝ) × ℝ) => Phi (zoomPointRec lam h rc zc q)) p = lam ^ (1 - 2 * h) * CKN.spatialPartial Phi 2 (zoomPointRec lam h rc zc p)

∂_Z of a scalar composed with zoomPointRec.

theorem CIV.dtPast_comp_zoomPointRec (lam h rc zc : ℝ) {Phi : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPhi : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Phi z) unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) : dtPast (fun (q : (ℝ × ℝ) × ℝ) => Phi (zoomPointRec lam h rc zc q)) p = lam ^ 2 * CKN.timePartial Phi (zoomPointRec lam h rc zc p)

∂_τ from the past of a scalar composed with zoomPointRec.

The rescaled azimuthal-vorticity equation

theorem CIV.zoomTheta_pde (lam h rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (pres : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u pres f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) (hR : p.1.1 ≠ -(rc / lam)) : dtPast (zoomTheta lam h rc zc u) p + zoomVRec lam h rc zc u p * dr (zoomTheta lam h rc zc u) p + zoomWRec lam h rc zc u p * dz (zoomTheta lam h rc zc u) p - zoomVRec lam h rc zc u p / (rc / lam + p.1.1) * zoomTheta lam h rc zc u p = dr (dr (zoomTheta lam h rc zc u)) p + 1 / (rc / lam + p.1.1) * dr (zoomTheta lam h rc zc u) p + (lam ^ (2 * h)) ^ 2 * dz (dz (zoomTheta lam h rc zc u)) p - zoomTheta lam h rc zc u p / (rc / lam + p.1.1) ^ 2 + 1 / (rc / lam + p.1.1) * dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec lam h rc zc u q ^ 2) p + lam ^ 4 * lam ^ (2 * h) * curlComp f 1 (zoomPointRec lam h rc zc p)

eq:aniso:zoom:receding:equation: the rescaled azimuthal-vorticity equation for zoomTheta in the recentred variables, with A = rc / lam. It is lam ^ 4 * δ times azimuthal_vorticity_pde at the recentred zoom point, δ = lam ^ (2 * h).

The receding-axis circulation identity and swirl bound

theorem CIV.mul_zoomSRec_eq_circulation (lam h rc zc : ℝ) (hlam : lam ≠ 0) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : (rc / lam + p.1.1) * zoomSRec lam h rc zc u p = lam ^ (2 * h) * circulation u (zoomPointRec lam h rc zc p)

The receding-axis circulation identity: (A + R) * S_n = δ * Γ at the recentred zoom point, with A = rc / lam and δ = lam ^ (2 * h).

theorem CIV.abs_zoomSRec_le_of_circulation {lam h rc zc CΓ : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : (ℝ × ℝ) × ℝ} (hApos : 0 < rc / lam + p.1.1) (hΓ : |circulation u (zoomPointRec lam h rc zc p)| ≤ CΓ) : |zoomSRec lam h rc zc u p| ≤ CΓ * lam ^ (2 * h) / (rc / lam + p.1.1)

Item (c): the receding-axis circulation bound |S_n| ≤ C_Γ δ / (A + R), for A + R > 0.

The receding-axis swirl-source form and value bound

theorem CIV.dz_zoomSRecSq_div_eq (lam h rc zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec lam h rc zc u q ^ 2 / (rc / lam + q.1.1)) p = 1 / (rc / lam + p.1.1) * dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec lam h rc zc u q ^ 2) p

Item (d), the form part: along the vertical slice through p, A + R does not depend on Z, so the swirl-source term 1 / (A + R) * ∂_Z (S_n ^ 2) of zoomTheta_pde is the vertical derivative of the conservative swirl source S_n ^ 2 / (A + R).

theorem CIV.abs_zoomSRecSq_div_le {lam h rc zc CΓ : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p : (ℝ × ℝ) × ℝ} (hApos : 0 < rc / lam + p.1.1) (hCΓ : 0 ≤ CΓ) (hΓ : |circulation u (zoomPointRec lam h rc zc p)| ≤ CΓ) : |zoomSRec lam h rc zc u p ^ 2 / (rc / lam + p.1.1)| ≤ CΓ ^ 2 * (lam ^ (2 * h)) ^ 2 / (rc / lam + p.1.1) ^ 3

Item (d), the value bound: the receding-axis swirl-source value S_n ^ 2 / (A + R) is bounded by C_Γ ^ 2 δ ^ 2 / (A + R) ^ 3, for A + R > 0, from the circulation bound of abs_zoomSRec_le_of_circulation.

The receding preimage clause

theorem CIV.eventually_zoomPointRec_mem_unitCylinder {h rc zc ρ : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hm : rc ^ 2 + zc ^ 2 < ρ ^ 2) (hρ : ρ < 1) (K : Set ((ℝ × ℝ) × ℝ)) (hK : IsCompact K) (hKt : ∀ p ∈ K, p.2 < 0) : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ p ∈ K, zoomPointRec lam h rc zc p ∈ unitCylinder

Item (b), the cylinder clause: for a compact set K of negative-time points bounded away from the axis offset by |rc| ^ 2 + |zc| ^ 2 < ρ ^ 2 < 1, the recentred zoom point of every point of K eventually lies in the unit cylinder Q.

theorem CIV.eventually_zoomPointRec_mem_ball {h rc zc ρ Rstar : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hm : rc ^ 2 + zc ^ 2 < ρ ^ 2) (hρ : ρ < Rstar) (K : Set ((ℝ × ℝ) × ℝ)) (hK : IsCompact K) : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ p ∈ K, (zoomPointRec lam h rc zc p).1 ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar

Item (b), the ball clause: for a compact set K bounded away from the axis offset by rc ^ 2 + zc ^ 2 < ρ ^ 2 < R_*, the recentred zoom point of every point of K eventually has its spatial part in the ball B(R_*).

theorem CIV.eventually_zoomPointRec_time_mem (rc : ℝ) {h zc tstar : ℝ} (htstar : tstar < 0) (K : Set ((ℝ × ℝ) × ℝ)) (hK : IsCompact K) (hKt : ∀ p ∈ K, p.2 < 0) : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ p ∈ K, (zoomPointRec lam h rc zc p).2 ∈ Set.Ioo tstar 0

Item (b), the time clause: the time slot of zoomPointRec is lam ^ 2 * τ, exactly as for zoomPoint, independent of rc, so this reduces to eventually_zoomPoint_time_mem.

theorem CIV.eventually_zoomPointRec_mem_ball_and_time {h rc zc ρ Rstar tstar : ℝ} (hh : 0 < h ∧ h < 1 / 2) (hρ0 : 0 ≤ ρ) (hm : rc ^ 2 + zc ^ 2 < ρ ^ 2) (hρ : ρ < Rstar) (htstar : tstar < 0) (K : Set ((ℝ × ℝ) × ℝ)) (hK : IsCompact K) (hKt : ∀ p ∈ K, p.2 < 0) : ∀ᶠ (lam : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ p ∈ K, (zoomPointRec lam h rc zc p).1 ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar ∧ (zoomPointRec lam h rc zc p).2 ∈ Set.Ioo tstar 0

Item (b) in full: the ball and time clauses together, the set on which the circulation bound abs_zoomSRec_le_of_circulation and the anisotropic bounds of CIV.Zoom.Receding hold.

theorem CIV.tendsto_zoomPointRec_ratio_atTop {rc : ℝ} (hrc : 0 < rc) : Filter.Tendsto (fun (lam : ℝ) => rc / lam) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop

The receding-axis regime named in item (b): for a fixed positive radial offset rc, the ratio A = rc / lam tends to infinity as the zoom scale lam shrinks to 0.