secondDeriv_radialInv_proved
plain-language theorem explainer
The theorem gives the explicit second directional derivative of the radial function 1/r^n in four-dimensional spacetime coordinates, returning zero whenever either index is the temporal direction and otherwise the standard expression n((n+2)x_μ x_ν/r^{n+4} - δ_μν/r^{n+2}). Researchers replacing axiom declarations with proved C2 statements in Recognition Science relativity calculus would cite it. The proof splits on the temporal indices, reduces via the already-proved first partial, and applies the quotient rule on the coordinate ray using HasD
Claim. Let $r(x)$ be the spatial radius of the four-vector $x$. For $n$ a natural number, indices $μ,ν$ in {0,1,2,3}, and $x$ with $r(x)≠0$, the second directional derivative satisfies $∂_μ∂_ν(r^{-n})(x)=0$ if $μ=0$ or $ν=0$, and otherwise equals $n((n+2)x_μ x_ν/r^{n+4}-δ_{μν}/r^{n+2})$.
background
The module replaces seven axiom declarations in Derivatives.lean with proved theorems for radial functions on spacetime. spatialRadius extracts the Euclidean norm on the three spatial components of a Fin 4 → ℝ vector (time index 0). radialInv n is the map sending x to 1/(spatialRadius x)^n. secondDeriv denotes the second directional derivative in directions μ and ν. The local setting is the C2 discharge for Minkowski-space calculus needed by Recognition Science models of potentials and Laplacians. Upstream lemmas include partialDeriv_v2_radialInv_proved (first partial formula) and spatialRadius_coordRay_ne_zero_eventually (eventual non-vanishing along rays).
proof idea
Case analysis on μ=0 via by_cases yields the zero result by eventual constancy and deriv_const. The symmetric case ν=0 reduces to constancy along the temporal ray using spatialRadius_coordRay_temporal and the first partial theorem. In the spatial case the proof invokes Filter.EventuallyEq.deriv_eq to substitute the smooth first-derivative expression, then defines numerator and denominator functions, establishes HasDerivAt for each via const_mul, pow, and the already-proved spatialRadius derivative, and concludes with the quotient rule.
why it matters
The result is invoked directly by laplacian_radialInv_n_proved (which sums the diagonal second derivatives to obtain the closed Laplacian formula) and by laplacian_radialInv_zero_no_const_proved (the n=1 harmonic case). It discharges one of the seven radial axioms listed in the module doc-comment, supporting the framework's reliance on smooth radial potentials away from the origin. No open scaffolding remains for this specific statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.