spatialNormSq_coordRay_temporal
plain-language theorem explainer
The squared spatial norm of a 4-vector is unchanged by addition of any multiple of the temporal basis vector. Workers deriving coordinate-invariant differential operators in the relativity calculus would cite the result when separating time shifts from spatial geometry. The proof unfolds the norm definition then rewrites the three spatial components via the preservation lemma for temporal rays.
Claim. For any 4-vector $x$ and real $s$, let $y = x + s e_0$ with $e_0$ the temporal basis vector. Then the squared Euclidean norm of the spatial components of $y$ equals that of $x$.
background
Coordinate rays are defined by adding a scalar multiple of a basis vector: $y = x + t e_μ$. The spatial norm squared extracts the sum of squares on the three spatial coordinates. The supporting lemma shows that a temporal ray (μ = 0) leaves those three coordinates exactly equal to the original values.
proof idea
Unfold the definition of spatialNormSq. Apply the preservation lemma three times, once for each spatial index, to equate the components of the shifted vector with those of x. Rewrite the unfolded expression with these three equalities.
why it matters
The lemma is invoked directly to prove invariance of spatialRadius under temporal rays and to establish that spatialRadius stays nonzero under small coordinate perturbations. It thereby supports the directional derivative formula for spatialRadius in the radial proofs, closing the separation between temporal and spatial calculus steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.