differentiableAt_coordRay_spatialRadius
plain-language theorem explainer
The theorem establishes differentiability of the spatial radius function along any coordinate ray in four-dimensional spacetime, provided the radius is nonzero at the base point. Analysts deriving radial derivatives for relativistic models cite this result to justify subsequent chain-rule steps for quantities like inverse powers of radius. The proof reduces the claim to an application of the square-root differentiability lemma after unfolding the radius definition and confirming the squared-norm input remains nonzero along the ray.
Claim. Let $x : {R}^4$ with spatial radius $r(x) {neq} 0$, and fix coordinate index ${mu}$. The map $t {mapsto} r(x + t e_{mu})$ is differentiable at $t = 0$, where $e_{mu}$ is the standard basis vector.
background
The module supplies the coordinate-ray parametrization coordRay(x, mu, t) = x + t * basisVec mu together with the spatial radius as the Euclidean norm of the three spatial components. The immediate prerequisite is the already-established differentiability of the squared spatial norm along the same ray, plus the evaluation lemma that the ray at t = 0 recovers the original point. Upstream structures from PhiForcingDerived and SpectralEmergence supply the J-cost convexity and dimensional forcing (D = 3 spatial) that motivate working in this 4D coordinate setting.
proof idea
The proof unfolds the spatial-radius definition, invokes the zero-ray evaluation to obtain a nonzero squared-norm value at t = 0, and applies the DifferentiableAt.sqrt constructor to the prior differentiability result for the squared norm along the ray.
why it matters
This result feeds the chain of differentiability statements for radialInv and its partial and second derivatives, closing several of the remaining calculus axioms required for relativistic radial operators. It supports explicit derivative formulas used in downstream radial-derivative proofs and aligns with the framework's eight-tick octave and three-dimensional spatial structure. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.