The finite-axis lift: regularity across X = 0, the lifted scalar, the force limit

Three of the four remaining pieces of the anisotropic zoom-in lift of eq:drift:Bn:def.

• The regularity of the lifted drift B_n across the axis X = 0. The Jacobian bound norm_zoomDriftJacobian_le is off-axis only (0 < zoomLiftRadius), since zoomLiftRadius itself has a cone singularity at X = 0 and is not differentiable there. The honest question is not about zoomLiftRadius, but about B_n's own radial part V_n(|X|, Z, τ) X/|X|. Along every ray through the axis in a single lifted radial coordinate, this part is exactly V_n itself — not merely close to it — because V_n, regarded as a function of the signed Cartesian radial coordinate, is odd (apply_meridional_reflect_zero), and the odd reflection of a function through the origin is exactly what the direction cosine X/|X| builds back out of |X|. This gives a genuine two-sided derivative of B_n's ray restriction at the axis, equal to the derivative of V_n there (hasDerivAt_zoomDrift_diag_ray_zero), together with a quantitative bound of the radial part by C |τ|^{-1/2} times the distance to the axis (abs_zoomDrift_apply_le_mul_zoomLiftRadius), which is Lipschitz regularity. What is not established, and is not claimed, is joint (Fréchet) differentiability of the full map X ↦ B_n(X, Z, τ) at X = 0: that would need V_n(\cdot, Z, τ) to be a smooth function of the square of the radius, a structural fact beyond the pointwise derivative bounds proved in CIV.Zoom.FiniteAxisBounds.
• The force term G_n of eq:interior:force:scaled obeys |G_n| ≤ C λ^5 λ^{2h}, and this bound tends to zero as λ → 0⁺, the limit taken in the zoom scale.
• The lifted potential vorticity Ω_tilde(X, Z, τ) = Ω_n(|X|, Z, τ) of the paragraph before eq:aniso:zoom:lifted, and its finite-axis bound, transported through the lift.

The lifted equation eq:aniso:zoom:lifted itself is stated off the axis in CIV.Zoom.FiniteLiftEquation, where the radial operator ∂_RR + 3R⁻¹∂_R is identified with the Laplacian Δ_X of the four lifted spatial coordinates. No finite-n equation is stated across the axis: the limit equation eq:aniso:zoom:finite:limit, in the form IsDistributionalDriftDiffusion that lem:aniso:comparison uses, is obtained with a cutoff at the axis (deviation D17).

(a) The regularity of the lifted drift across the axis

theorem CIV.zoomV_odd (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (haxi : IsAxisymmetricOn u unitCylinder) {r Z τ : ℝ} (hp : zoomPoint lam h zc ((r, Z), τ) ∈ unitCylinder) : zoomV lam h zc u ((-r, Z), τ) = -zoomV lam h zc u ((r, Z), τ)

V_n is odd under reflection of its radial argument: the underlying Cartesian velocity component u_1 is odd across the meridional reflection x_1 ↦ -x_1 (apply_meridional_reflect_zero), and zoomV is u_1 composed with the affine zoom-in map.

def CIV.zoomAxisPoint (Z : ℝ) : CKN.Vec 5

The point of Vec 5 on the axis at height Z: the four radial coordinates vanish, and the fifth (vertical) coordinate is Z.

Equations

• CIV.zoomAxisPoint Z = Function.update 0 4 Z

theorem CIV.zoomAxisPoint_apply_four (Z : ℝ) : zoomAxisPoint Z 4 = Z

theorem CIV.zoomDrift_diag_ray_eq (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (haxi : IsAxisymmetricOn u unitCylinder) {i : Fin 5} (hi : i ≠ 4) {Z s τ : ℝ} (hp : zoomPoint lam h zc ((|s|, Z), τ) ∈ unitCylinder) : zoomDrift lam h zc u (Function.update (zoomAxisPoint Z) i s, τ) i = zoomV lam h zc u ((s, Z), τ)

The exact regularity across the axis: along any ray through the axis in a single lifted radial coordinate i, the diagonal (matching) radial component of the lifted drift B_n equals V_n itself, for every real s — not merely close to it. This is the honest statement in place of smoothness of zoomLiftRadius, which has a cone singularity at s = 0: the singularity of X ↦ X/|X| there is exactly cancelled by the fact that V_n, as a function of the signed Cartesian radial coordinate, is odd (zoomV_odd), so V_n(|s|, Z, τ) · s/|s| collapses to V_n(s, Z, τ) on both sides of s = 0, and to 0 (by zoomV_axis) at s = 0 itself.

theorem CIV.hasDerivAt_zoomDrift_diag_ray_zero (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {i : Fin 5} (hi : i ≠ 4) {Z τ : ℝ} (hp : zoomPoint lam h zc ((0, Z), τ) ∈ unitCylinder) : HasDerivAt (fun (s : ℝ) => zoomDrift lam h zc u (Function.update (zoomAxisPoint Z) i s, τ) i) (dr (zoomV lam h zc u) ((0, Z), τ)) 0

Genuine two-sided differentiability of B_n's diagonal ray-restriction at the crossing s = 0: zoomDrift_diag_ray_eq identifies the ray-restriction with V_n on a whole neighbourhood of s = 0 (not merely pointwise), so its derivative at the crossing exists and equals the derivative of V_n there, already available off the axis. This is the sharpest statement available: it does not extend to a joint (Fréchet) derivative of the full map X ↦ B_n(X, Z, τ) at X = 0 in every direction at once, which would need V_n(\cdot, Z, τ) to depend smoothly on the square of its argument — a structural fact beyond the pointwise derivative bounds proved in CIV.Zoom.FiniteAxisBounds.

theorem CIV.abs_zoomDrift_apply_le_mul_zoomLiftRadius {C h lam zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hC : 0 ≤ C) (hτ : q.2 ≤ -1) {i : Fin 5} (hi : i ≠ 4) : |zoomDrift lam h zc u q i| ≤ C * (-q.2) ^ (-(1 / 2)) * zoomLiftRadius q.1

The quantitative Lipschitz-to-axis bound: every radial component of the lifted drift B_n is within C |τ|^{-1/2} times the distance to the axis, in every direction at once (not just along coordinate rays) — this is the genuine, general-purpose "Lipschitz across X = 0" content of the footnote to eq:drift:Bn:def. It follows from the same segment bound abs_zoomV_div_le that supplies the diagonal entry of norm_zoomDriftJacobian_le, combined with the direction-cosine bound abs_le_zoomLiftRadius; it holds at the axis itself, where both sides vanish.

(d) The force term vanishes in the zoom scale

noncomputable def CIV.zoomForce (lam h zc : ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : (ℝ × ℝ) × ℝ) : ℝ

The rescaled force term G_n of eq:interior:force:scaled: λ^5 λ^{2h} times the potential vorticity of the force, evaluated at the zoom point — the force term of eq:aniso:zoom:finite:equation, exactly as it enters zoomOmega_pde.

Equations

• CIV.zoomForce lam h zc f p = lam ^ 5 * lam ^ (2 * h) * CIV.potentialVorticity f (CIV.zoomPoint lam h zc p)

theorem CIV.abs_zoomForce_le {lam h zc : ℝ} (hlam : 0 < lam) {f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hf : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => f z) unitCylinder) (hfaxi : IsAxisymmetricOn f unitCylinder) (hMf : ForceC2Bounded f) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (p : (ℝ × ℝ) × ℝ), zoomPoint lam h zc p ∈ unitCylinder → |zoomForce lam h zc f p| ≤ C * (lam ^ 5 * lam ^ (2 * h))

|G_n| ≤ C λ^5 λ^{2h} on the preimage of the unit cylinder, uniformly in the point: the potential vorticity of a C²-bounded, axisymmetric, C^∞ force is bounded by a constant depending only on the force (abs_potentialVorticity_force_le), and λ^5 λ^{2h} ≥ 0 for λ > 0.

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

The bound of abs_zoomForce_le tends to zero in the zoom scale, as λ → 0⁺: this is |G_n| ≤ C M_f λ^5 δ_n → 0, the fourth of the missing pieces, since λ^5 λ^{2h} = λ^{5 + 2h} and 5 + 2h > 0.

(b) The lifted scalar Ω_tilde

noncomputable def CIV.zoomOmegaLift (lam h zc : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (q : CKN.Vec 5 × ℝ) : ℝ

The lifted potential vorticity Ω_tilde(X, Z, τ) = Ω_n(|X|, Z, τ) of the paragraph before eq:aniso:zoom:lifted: zoomOmega composed with the lift zoomLiftPoint, a function of the lifted spatial point (X, Z) ∈ Vec 5 and the rescaled time τ.

Equations

• CIV.zoomOmegaLift lam h zc u q = CIV.zoomOmega lam h zc u (CIV.zoomLiftPoint q)

theorem CIV.abs_zoomOmegaLift_le {C h lam zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) : |zoomOmegaLift lam h zc u q| ≤ C * ((lam ^ (2 * h)) ^ 2 * (-q.2) ^ (-(3 / 2) + h) + (-q.2) ^ (-(3 / 2) - h))

The finite-axis bound eq:aniso:zoom:finite:bound for the lifted scalar, on and off the axis: abs_zoomOmega_le_of_mem transported through the lift.

theorem CIV.abs_zoomOmegaLift_le_two_mul_const {C h lam zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) (hu : ContDiffOn ℝ 2 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) {q : CKN.Vec 5 × ℝ} (hp : zoomPoint lam h zc (zoomLiftPoint q) ∈ unitCylinder) (hC : 0 ≤ C) (hδ : lam ^ (2 * h) ≤ 1) (hh0 : 0 < h) (hh1 : h < 1 / 2) (hτ : q.2 ≤ -1) : |zoomOmegaLift lam h zc u q| ≤ 2 * C

The uniform-in-n bound 2C for τ ≤ -1, the form the compactness argument of eq:aniso:zoom:finite:compactness actually uses: abs_zoomOmega_le_two_mul_const transported through the lift.