The on-axis (R = 0) counterpart of CIV.Zoom.FiniteSelectionIdentity's selected-point identity for Step 2's contradiction (paragraph after eq:aniso:zoom:finite:limit): at the axis the manuscript's u_r/r term is by definition ∂_r u_r (radialQuotient_on_axis), so the identity becomes (-t)(2|∂_r u_r| + |∂_z u_z|) = 2|∂_R V_n| + |∂_Z W_n| at ((0,0),-1), with no division by the vanishing radius; this is the case the finite-axis dichotomy's on-axis branch needs and that CIV.Zoom.FiniteSelectionIdentity's own R ≠ 0 hypothesis excludes.

theorem CIV.neg_t_mul_meridionalQuantity_selection_eq_of_axis {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 zc : ℝ} (hlam : 0 < lam) (hlamsq : lam ^ 2 = -t) (hp : zoomPoint lam h zc ((0, 0), -1) ∈ unitCylinder) : -t * (|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 (meridional 0 zc, t)| + |radialQuotient u (meridional 0 zc, t)| + |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2 (meridional 0 zc, t)|) = |dr (zoomV lam h zc u) ((0, 0), -1)| + |dr (zoomV lam h zc u) ((0, 0), -1)| + |dz (zoomW lam h zc u) ((0, 0), -1)|