The chain-rule bridge between the meridional-plane quantities ∂_r u_r, u_r/r, ∂_z u_z
of eq:aniso:zoom:selected at a time t < 0 and the finite-axis rescaled fields V_n, W_n of
eq:aniso:zoom:fields, evaluated at the corresponding rescaled point (R, 0, -1) with lam² = -t:
the identity that lets Step 2's contradiction (paragraph after eq:aniso:zoom:finite:limit)
read the selected sequence's scaled quantity off the zoom variables at τ = -1.
theorem
CIV.neg_t_mul_meridionalQuantity_selection_eq
{h : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder)
{t : ℝ}
(ht : t < 0)
{lam R zc : ℝ}
(hlam : 0 < lam)
(hR : R ≠ 0)
(hlamsq : lam ^ 2 = -t)
(hp : zoomPoint lam h zc ((R, 0), -1) ∈ unitCylinder)
:
-t * (|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 (meridional (lam * R) zc, t)| + |radialQuotient u (meridional (lam * R) zc, t)| + |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2
(meridional (lam * R) zc, t)|) = |dr (zoomV lam h zc u) ((R, 0), -1)| + |zoomV lam h zc u ((R, 0), -1) / R| + |dz (zoomW lam h zc u) ((R, 0), -1)|