Value bound for the receding-axis vertical rescaled field zoomWRec

The value bound (order (0,0)) for zoomWRec, cleanly separated from the nonnegative swirl source zoomSRec and normalized to the shared exponent -1/2 exactly as its second-derivative bounds are in CIV/Zoom/RecedingSecondDerivativeBoundsW.lean. The companion compact-time-rectangle wrapper completes the pattern of CIV.exists_forall_abs_zoomVRec_le_of_isCompact (CIV/Zoom/VRecBoundedRectangle.lean) for the vertical field.

theorem CIV.abs_zoomWRec_le_rpow_neg_half {C h lam rc zc : ℝ} (hlam : 0 < lam) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hb : AnisotropicBounds C h u) {p : (ℝ × ℝ) × ℝ} (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) (hC : 0 ≤ C) (hh0 : 0 ≤ h) (hτ : p.2 ≤ -1) : |zoomWRec lam h rc zc u p| ≤ C * (-p.2) ^ (-(1 / 2))

theorem CIV.exists_forall_abs_zoomWRec_le_of_isCompact {C h : ℝ} (hC : 0 ≤ C) (hh0 : 0 ≤ h) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (rc zc : ℝ) {J : Set ℝ} (hJ : IsCompact J) (hJsub : ∀ τ ∈ J, τ ≤ -1) : ∃ (M : ℝ), ∀ (lam : ℝ), 0 < lam → ∀ (p : (ℝ × ℝ) × ℝ), zoomPointRec lam h rc zc p ∈ unitCylinder → p.2 ∈ J → |zoomWRec lam h rc zc u p| ≤ M

theorem CIV.exists_forall_abs_zoomVRec_le_and_abs_zoomWRec_le_of_isCompact {C h : ℝ} (hC : 0 ≤ C) (hh0 : 0 ≤ h) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hb : AnisotropicBounds C h u) (rc zc : ℝ) {J : Set ℝ} (hJ : IsCompact J) (hJsub : ∀ τ ∈ J, τ ≤ -1) : ∃ (M : ℝ), ∀ (lam : ℝ), 0 < lam → ∀ (p : (ℝ × ℝ) × ℝ), zoomPointRec lam h rc zc p ∈ unitCylinder → p.2 ∈ J → |zoomVRec lam h rc zc u p| ≤ M ∧ |zoomWRec lam h rc zc u p| ≤ M