secondDeriv_radialInv
plain-language theorem explainer
The second directional derivative of the radial inverse 1/r^n equals n times ((n+2) x_μ x_ν / r^{n+4} minus Kronecker delta over r^{n+2}) for spatial indices μ, ν and vanishes whenever either index is temporal. Relativists and potential theorists in Recognition Science cite it to obtain the Laplacian of inverse-power potentials away from the origin. The proof splits into three cases on the indices, reduces the nonzero case to the quotient rule applied to the smooth expression -n x_μ / r^{n+2} along a coordinate ray, and simplifies the resulting
Claim. Let $n$ be a natural number, let $x$ be a point in four-dimensional space with nonzero spatial radius $r(x)$, and let indices $μ,ν$ run over $0,1,2,3$. Then the second directional derivative $∂_ν ∂_μ (r^{-n})$ equals zero if $μ=0$ or $ν=0$, and otherwise equals $n·((n+2)x_μ x_ν/r^{n+4} - δ_{μν}/r^{n+2})$.
background
In this module the radial inverse function is defined by radialInv n := fun x => (spatialRadius x)^(-n). The operator secondDeriv f μ ν x computes the second directional derivative of f along the coordinate directions μ then ν at point x, built from the first-order partialDeriv_v2 that itself uses the coordRay parametrization. spatialRadius extracts the Euclidean norm of the three spatial components of a four-vector, treating the zeroth component as time. The local setting is the standard calculus of smooth functions on Minkowski space needed to close the Mathlib axioms listed in §XXIII.B′. Upstream lemmas such as partialDeriv_v2_radialInv supply the explicit first-derivative formula -n x_μ / r^{n+2} (for spatial μ) that the second-derivative argument starts from.
proof idea
The tactic proof unfolds secondDeriv and performs case analysis on whether μ equals zero. When μ=0 the inner partial is identically zero, so the outer derivative is zero. When ν=0 but μ nonzero the inner partial is constant along the temporal ray, again yielding zero. In the remaining case the proof shows the inner partial equals the smooth expression -n (coordRay x ν s)μ / r(coordRay x ν s)^{n+2} eventually near s=0, then applies HasDerivAt.div to the quotient of numerator -n·(x_μ + s δ{μν}) and denominator r^{n+2}, using the known derivative of spatialRadius along the ray and the power rule; algebraic simplification with ring and field_simp produces the target formula.
why it matters
This theorem supplies the explicit second derivatives required by the two Laplacian statements laplacian_radialInv_n and laplacian_radialInv_zero_no_const that immediately follow it; those in turn close the Mathlib calculus axioms for inverse-power potentials. Within Recognition Science the result supports the derivative infrastructure needed for the D=3 spatial sector (T8) and for any potential whose recognition cost is built from radial inverses. It touches the open question of extending the same calculus to the full eight-tick octave structure once the temporal components are reintroduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.