The receding-axis endpoint argument

Step 3 of Section 4: the algebraic core of eq:aniso:zoom:receding:limit's time-τ = −1 slice. On the whole meridional half-plane lifted to ℝ × ℝ (no axis restriction, unlike the finite-axis case of CIV/Zoom/EndpointFiniteAxis.lean, whose divergence identity carries a V / R term), a divergence-free pair (V, W) with ∂_R W = 0 and V bounded has W independent of R and, once boundedness is used, both ∂_R V and ∂_Z W vanish identically — the receding-axis analogue of CIV.endpoint_vanishing.

theorem CIV.endpoint_axial_const_rec (W : ℝ × ℝ → ℝ) (DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (hW : ∀ (p : ℝ × ℝ), HasFDerivAt W (DW p) p) (hWr : ∀ (p : ℝ × ℝ), (DW p) (1, 0) = 0) (R Z : ℝ) : W (R, Z) = W (0, Z)

theorem CIV.endpoint_dz_axial_const_rec (W : ℝ × ℝ → ℝ) (DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (hW : ∀ (p : ℝ × ℝ), HasFDerivAt W (DW p) p) (hWr : ∀ (p : ℝ × ℝ), (DW p) (1, 0) = 0) (R Z : ℝ) : (DW (R, Z)) (0, 1) = (DW (0, Z)) (0, 1)

theorem CIV.endpoint_radial_eq_rec (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (hV : ∀ (p : ℝ × ℝ), HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), HasFDerivAt W (DW p) p) (hdiv : ∀ (p : ℝ × ℝ), (DV p) (1, 0) + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), (DW p) (1, 0) = 0) (R Z : ℝ) : V (R, Z) = V (0, Z) - R * (DW (0, Z)) (0, 1)

theorem CIV.endpoint_dz_axial_eq_zero_rec (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (M : ℝ) (hV : ∀ (p : ℝ × ℝ), HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), HasFDerivAt W (DW p) p) (hbdd : ∀ (p : ℝ × ℝ), |V p| ≤ M) (hdiv : ∀ (p : ℝ × ℝ), (DV p) (1, 0) + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), (DW p) (1, 0) = 0) (Z : ℝ) : (DW (0, Z)) (0, 1) = 0

theorem CIV.endpoint_dr_radial_eq_zero_rec (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (M : ℝ) (hV : ∀ (p : ℝ × ℝ), HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), HasFDerivAt W (DW p) p) (hbdd : ∀ (p : ℝ × ℝ), |V p| ≤ M) (hdiv : ∀ (p : ℝ × ℝ), (DV p) (1, 0) + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), (DW p) (1, 0) = 0) (p : ℝ × ℝ) : (DV p) (1, 0) = 0

theorem CIV.endpoint_vanishing_rec (V W : ℝ × ℝ → ℝ) (DV DW : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ) (M : ℝ) (hV : ∀ (p : ℝ × ℝ), HasFDerivAt V (DV p) p) (hW : ∀ (p : ℝ × ℝ), HasFDerivAt W (DW p) p) (hbdd : ∀ (p : ℝ × ℝ), |V p| ≤ M) (hdiv : ∀ (p : ℝ × ℝ), (DV p) (1, 0) + (DW p) (0, 1) = 0) (hWr : ∀ (p : ℝ × ℝ), (DW p) (1, 0) = 0) : (∀ (p : ℝ × ℝ), (DV p) (1, 0) = 0) ∧ ∀ (p : ℝ × ℝ), (DW p) (0, 1) = 0