partialDeriv_v2_radialInv_proved
plain-language theorem explainer
The directional derivative of the radial inverse function 1/r^n is computed explicitly along each coordinate axis in four-dimensional spacetime. Researchers deriving potentials or field gradients in recognition-weighted models would cite this when evaluating spatial derivatives away from the origin. The proof splits on the time index, uses ray invariance to obtain zero for the temporal component, and applies the chain and quotient rules plus algebraic simplification for the spatial components.
Claim. Let $r(x)$ denote the spatial radius of the four-vector $x$. For natural number $n$, coordinate index $μ ∈ {0,1,2,3}$, and point $x$ with $r(x) ≠ 0$, the directional derivative $∂_μ (r^{-n})$ equals 0 when $μ=0$ and equals $-n x_μ / r^{n+2}$ otherwise.
background
The spatial radius $r(x)$ is the Euclidean norm on the three spatial coordinates of a four-vector. The radial inverse is the function sending $x$ to $1/r(x)^n$. The operator partialDeriv_v2 supplies the directional derivative of a recognition field along the μ-th axis. This theorem belongs to the C2 discharge module that replaces seven placeholder axioms in Derivatives.lean with explicit proofs, relying on prior results such as spatialRadius_coordRay_temporal (invariance along temporal rays) and partialDeriv_v2_spatialRadius_proved (explicit derivative of the radius itself).
proof idea
The proof unfolds partialDeriv_v2 and radialInv, then cases on whether μ equals zero. The temporal case invokes spatialRadius_coordRay_temporal to show constancy along the ray and concludes the derivative is zero. The spatial case first obtains DifferentiableAt for the radius along the ray, lifts to HasDerivAt, applies the power rule, then uses the quotient rule for the reciprocal; the resulting expression is simplified by field_simp and ring_nf after splitting on n zero versus successor.
why it matters
This supplies the partial_inv_holds field inside c2DischargeCert, which certifies that the radial inverse functions meet the C2 requirements originally stated as axioms. It thereby discharges part of the scaffolding in the Relativity.Calculus layer. The explicit form supports downstream computations of gradients for inverse-power terms that appear in recognition cost functions, consistent with the three spatial dimensions fixed by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.