differentiableAt_coordRay_spatialNormSq
plain-language theorem explainer
The result establishes differentiability at the origin for the squared spatial norm of a 4-vector displaced along any coordinate ray. Workers deriving chain-rule expressions for spatial radius or directional derivatives in Minkowski space cite it as an intermediate step. The proof is a short term-mode reduction that unfolds the norm into three squared components and applies additivity of differentiability to each.
Claim. Let $x : ℝ^4$ and let $μ ∈ {0,1,2,3}$. The map $t ↦ ∑_{i=1}^3 (x_i + t δ_{μ i})^2$ is differentiable at $t=0$.
background
The module Relativity.Calculus.Derivatives supplies the coordinate ray coordRay x μ t, which adds t times the standard basis vector e_μ to the point x. spatialNormSq extracts the sum of squares of the three spatial components of a 4-vector. The lemma sits among a family of differentiability statements that prepare the ground for radial calculus. Upstream, the definition of coordRay and the component-wise result differentiableAt_coordRay_i_sq are already available.
proof idea
The proof unfolds spatialNormSq to a sum of three squared terms, then applies DifferentiableAt.add twice. Each summand is dispatched by the already-proved lemma differentiableAt_coordRay_i_sq applied to the appropriate spatial index.
why it matters
The declaration is invoked by differentiableAt_coordRay_spatialRadius and partialDeriv_v2_spatialRadius, which in turn supply the explicit form x_μ / r for spatial directional derivatives. Within the Recognition framework it closes a small piece of the derivative infrastructure needed for radial quantities in the relativity layer, without adding hypotheses or touching the phi-ladder or J-cost structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.