secondDeriv_radialInv_proved
plain-language theorem explainer
The second directional derivative of the radial function 1 over spatial radius to the power n vanishes if either index is the time direction and otherwise equals n times ((n+2) x_mu x_nu over r to the n+4 minus delta_mu nu over r to the n+2). Researchers deriving Laplacians of radial potentials or verifying harmonic properties in four-dimensional spacetime would cite this when reducing wave or Poisson operators on inverse-power functions. The proof proceeds by index case splits, eventually-equal replacement of the first partial via prior first-
Claim. Let $r(x)$ be the spatial radius of the four-vector $x$. For natural number $n$, indices $mu,nu$ in {0,1,2,3}, and $x$ with $r(x) neq 0$, the second directional derivative $partial_mu partial_nu (r^{-n})$ equals 0 if $mu=0$ or $nu=0$, and otherwise $n bigl( (n+2) frac{x_mu x_nu}{r^{n+4}} - frac{delta_{mu nu}}{r^{n+2}} bigr)$.
background
In the C2 discharge module, spatialRadius extracts the Euclidean norm of the three spatial components of a Fin 4 vector, while radialInv n denotes the map sending x to (spatialRadius x)^{-n}. The operator secondDeriv computes the mixed second partial in coordinate directions mu and nu. This theorem sits inside the replacement of seven axiom declarations in Derivatives.lean by explicit proofs that rely on Mathlib's HasDerivAt, deriv_div, and chain-rule lemmas together with the already-proved first partial partialDeriv_v2_radialInv_proved and the temporal-invariance fact spatialRadius_coordRay_temporal.
proof idea
The tactic proof opens with unfold secondDeriv and splits on whether mu equals 0. The temporal-mu case reduces the first partial to the constant zero function via spatialRadius_coordRay_ne_zero_eventually and applies Filter.EventuallyEq.deriv_eq. The spatial-mu temporal-nu case shows the first partial is invariant along the temporal ray by spatialRadius_coordRay_temporal and coordRay_temporal_spatial, hence its derivative vanishes. In the spatial-spatial case the first partial is replaced by its explicit formula, then the quotient rule is applied after establishing HasDerivAt for the numerator via const_mul and basisVec and for the denominator via partialDeriv_v2_spatialRadius_proved together with pow.
why it matters
This supplies the explicit second derivatives required by the two downstream Laplacian theorems: laplacian_radialInv_n_proved obtains the closed form n(n-1) r^{-n-2} by summing the diagonal terms, while laplacian_radialInv_zero_no_const_proved recovers the harmonic property of 1/r away from the origin. It completes one block of the C2 discharge for radial functions in the relativity calculus, supporting the framework's use of D=3 spatial dimensions and the forced phi-ladder structure for potentials. No open scaffolding remains for this specific result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.