partialDeriv_v2_radialInv
plain-language theorem explainer
The directional derivative of the radial inverse-power function 1/r^n is computed explicitly in four-dimensional coordinates. Researchers deriving Laplacians or second derivatives for potentials in relativity or electrostatics would cite this when reducing radial calculations to coordinate components. The proof splits into temporal and spatial cases, applying the constant derivative for time and the quotient rule combined with the known derivative of the radius for space.
Claim. Let $r(x)$ denote the spatial radius of the four-vector $x$. For the function $f(x) = r(x)^{-n}$, the partial derivative satisfies $∂_μ f(x) = 0$ if $μ=0$ and $∂_μ f(x) = -n x_μ r(x)^{-(n+2)}$ otherwise, whenever $r(x) ≠ 0$.
background
In this module spatialRadius denotes the Euclidean norm of the spatial components of a four-vector. The function radialInv n maps a point to the reciprocal of that norm raised to the power n. partialDeriv_v2 supplies the directional derivative along a coordinate axis, extending the placeholder interface defined in the Hamiltonian module. The local setting is the calculus of radial functions on Minkowski space, preparing explicit formulas for potentials that appear in Poisson and wave equations. This result rests on the upstream lemma partialDeriv_v2_spatialRadius_proved, which states that the derivative of the radius itself equals x_μ / r for spatial indices.
proof idea
The proof unfolds the definitions and splits on whether the index μ equals zero. The temporal case reduces the composition along the coordinate ray to a constant via spatialRadius_coordRay_temporal and invokes deriv_const. The spatial case cases on n, establishes HasDerivAt for the radius power and its reciprocal using pow and inv rules, then applies algebraic simplification with ring and power identities to reach the target expression -n x_μ / r^{n+2}.
why it matters
This supplies the explicit first derivative required by secondDeriv_radialInv and laplacian_radialInv_n_proved. It closes one of the six remaining calculus axioms listed in §XXIII.B′ and directly supports Laplacian computations for inverse-power radial functions that arise in gravitational and electrostatic potentials within the Recognition framework. The result feeds the chain of radial derivative identities used in the broader relativity calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.