coordRay_temporal_spatial
plain-language theorem explainer
The lemma shows that shifting a four-vector along the temporal direction by any real amount leaves its three spatial components fixed. Workers deriving radial derivatives or spatial norms in relativistic calculus cite it to justify invariance under time translations. The proof reduces directly to the definitions of the ray and basis vector via a single simplification step.
Claim. Let $x : {R}^4$, $s {in} R$, and index $i {in} {0,1,2,3}$ with $i {neq} 0$. The $i$-th component of the vector $x + s e_0$ equals the original $x_i$, where $e_0$ denotes the standard temporal basis vector.
background
The module introduces the standard basis vector $e_mu$ as the function returning 1 at position $mu$ and 0 elsewhere. The coordinate ray is defined by adding a scalar multiple of this basis vector to the input four-vector, shifting it along one coordinate axis. The local setting treats the four indices as one temporal and three spatial directions, with the lemma isolating the temporal shift case. Upstream definitions of the basis vector and coordinate ray supply the algebraic expansion used here.
proof idea
The proof is a one-line wrapper that applies the definitions of the coordinate ray and basis vector together with the index hypothesis via simplification.
why it matters
This lemma supplies the invariance step required by the second directional derivative theorem for radial inverse powers and by the spatial-norm invariance result. Both appear in the radial derivatives proofs that close the calculus layer. It supports the framework separation of temporal and spatial directions, consistent with the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.