spatialRadius_coordRay_temporal
plain-language theorem explainer
The lemma shows that the spatial radius of a four-vector stays fixed under displacement along the temporal coordinate ray. Researchers deriving relativistic directional derivatives cite it to confirm that time-like shifts leave spatial quantities unchanged. The proof is a direct reduction that unfolds the radius definition and rewrites via the already-established invariance of the squared spatial norm.
Claim. Let $r(x) = (x_1^2 + x_2^2 + x_3^2)^{1/2}$ denote the spatial radius of a four-vector $x$. For any real number $s$, $r(x + s e_0) = r(x)$, where $e_0$ is the temporal basis vector.
background
The Derivatives module introduces coordRay as the operation that adds a scalar multiple of a chosen basis vector to a four-vector. spatialNormSq sums the squares of the three spatial components, and spatialRadius is defined as its square root. The upstream lemma spatialNormSq_coordRay_temporal already establishes that this squared norm is invariant under temporal shifts, supplying the key algebraic identity. The module develops coordinate calculus for relativistic derivatives using these ray operations.
proof idea
This is a one-line wrapper that unfolds spatialRadius to expose the square root of spatialNormSq, then rewrites the claim using the lemma spatialNormSq_coordRay_temporal that proves the squared norm is unchanged under the same temporal ray.
why it matters
It supplies the invariance step required by partialDeriv_v2_spatialRadius and partialDeriv_v2_radialInv, where temporal derivatives of spatial radius and its inverse are shown to vanish. The result supports the chain to secondDeriv_radialInv and the closure of calculus axioms in the Relativity section, consistent with the need for coordinate-ray invariants in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.