differentiableAt_coordRay_radialInv
plain-language theorem explainer
The result establishes differentiability at the origin for the map sending parameter t along a coordinate ray to the reciprocal of the nth power of the spatial radius, provided the base radius is nonzero. Analysts working on coordinate expansions in four-dimensional relativistic models cite it to justify differentiation of radial expressions. The argument unfolds the radial inverse definition and applies the quotient rule together with the already-established differentiability of the spatial radius along the identical ray.
Claim. Let $r$ denote the spatial radius on $R^4$. For natural number $n$, point $x$ with $r(x) neq 0$, and index $mu$, the function $t mapsto 1/r(x + t e_mu)^n$ is differentiable at $t=0$.
background
The module supplies derivative tools for four-vectors using coordinate rays. coordRay(x, mu, t) traces the line through x in the direction of the standard basis vector e_mu. spatialRadius extracts the Euclidean norm of the three spatial components. radialInv n y returns the reciprocal of that norm raised to the nth power, a form common in potential or field expansions. The upstream result differentiableAt_coordRay_spatialRadius already guarantees that the radius itself varies differentiably along the same ray when nonzero at the base point. Nonnegativity of the squared spatial norm, drawn from spatialNormSq_nonneg, ensures the radius stays positive under the given hypothesis.
proof idea
The proof unfolds radialInv to expose a constant numerator over the nth power of the spatial radius along the ray. It invokes DifferentiableAt.div with the constant function on top and the power of the spatial-radius differentiability result below. A short positivity subproof uses spatialNormSq_nonneg and the radius-ne-zero equivalence to confirm the denominator stays nonzero at t=0, after which coordRay_zero simplifies the evaluation.
why it matters
This supplies a basic differentiability fact required for higher-order operations such as second derivatives and the Laplacian within the same module. It completes a local step in the coordinate calculus chain that supports smooth radial dependence in relativistic expressions. In the Recognition Science setting it underwrites the continuous geometry presupposed by the forcing chain (T0-T8) and the Recognition Composition Law, where spatial norms enter mass formulas and Berry thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.