differentiableAt_coordRay_partialDeriv_v2_radialInv_proved
plain-language theorem explainer
The theorem establishes differentiability at the origin for the map sending s to the partial derivative with respect to coordinate mu of r to the minus n, when the argument is taken along a coordinate ray in four dimensions, assuming the spatial radius at the base point is nonzero. Researchers verifying smoothness conditions for radial potentials in relativistic field equations would cite it during C2 discharge checks. The proof proceeds by case split on the index mu, reducing the zero case to a constant via eventual equality and the nonzero mu
Claim. Let $r$ be the spatial radius on $mathbb{R}^4$. For natural number $n$, base point $x$ with $r(x) neq 0$, and indices $mu, nu$, the map $s mapsto partial_mu (r^{-n})$ evaluated at the point obtained by varying the $nu$-th coordinate of $x$ by parameter $s$ is differentiable at $s=0$.
background
The module replaces seven axiom declarations from the Derivatives module with proved theorems on radial derivatives. Spatial radius denotes the Euclidean norm of the three spatial components of a four-vector. Coordinate ray parametrizes a straight line in the chosen coordinate direction nu from base point x, leaving the spatial radius invariant when the temporal component is varied. Upstream lemmas supply differentiability of individual coordinate components along the ray, differentiability of the spatial radius along the ray, and the explicit algebraic formula for the partial derivative of the radial inverse power.
proof idea
Case analysis on whether mu equals zero. For mu zero the partial is identically zero near the origin, so the result follows from differentiability of the constant function after congruence via the eventually nonzero radius condition. For mu nonzero the partial agrees eventually with the explicit quotient -n times the mu-component of the ray point over spatial radius to the power n+2; differentiability of the quotient is obtained by the division rule applied to the differentiable coordinate component and the powered spatial radius, with the denominator nonzero at zero by hypothesis.
why it matters
The result is collected into the c2DischargeCert definition that certifies all required C2 properties for radial derivatives hold after the axioms in Derivatives.lean are discharged. It supports replacement of unresolved axioms by theorems in the relativity calculus layer, ensuring smoothness of radial potentials without hidden hypotheses. Within the Recognition framework this closes a necessary step for geodesic and field smoothness arguments that rely on the eight-tick octave and D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.