The receding-axis zoom: selected-point identities #
These identities connect the recentred zoom variables at the selected rescaled time
τ = -1 and radial coordinate R to the corresponding Cartesian meridional quantities
at the physical time t = -λ² and radius rc + λR. They are the receding-axis analog of
CIV.Zoom.FiniteSelectionIdentity and form the chain-rule bridge used in Step 3's
contradiction argument.
theorem
CIV.meridional_selected_mem_unitCylinder_of_zoomPointRec
{lam h rc zc t : ℝ}
(hlamsq : lam ^ 2 = -t)
{R : ℝ}
(hp : zoomPointRec lam h rc zc ((R, 0), -1) ∈ unitCylinder)
:
theorem
CIV.neg_t_mul_meridionalQuantity_receding_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 rc zc : ℝ}
(hlam : 0 < lam)
(hR : R ≠ -(rc / lam))
(hlamsq : lam ^ 2 = -t)
(hp : zoomPointRec lam h rc zc ((R, 0), -1) ∈ unitCylinder)
:
-t * (|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0
(meridional (rc + lam * R) zc, t)| + |radialQuotient u (meridional (rc + lam * R) zc, t)| + |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2
(meridional (rc + lam * R) zc, t)|) = |dr (zoomVRec lam h rc zc u) ((R, 0), -1)| + |zoomVRec lam h rc zc u ((R, 0), -1) / (rc / lam + R)| + |dz (zoomWRec lam h rc zc u) ((R, 0), -1)|