spatialNormSq_coordRay_temporal
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not claim invariance under shifts along any spatial axis.
- Does not treat the full Minkowski interval that includes the time component.
- Does not extend to non-Euclidean spatial metrics or curved backgrounds.
- Does not supply bounds on admissible values of the shift parameter s.
Lean usage
lemma spatialRadius_coordRay_temporal (x : Fin 4 → ℝ) (s : ℝ) : spatialRadius (coordRay x 0 s) = spatialRadius x := by unfold spatialRadius; rw [spatialNormSq_coordRay_temporal]formal statement (Lean)
173lemma spatialNormSq_coordRay_temporal (x : Fin 4 → ℝ) (s : ℝ) :
174 spatialNormSq (coordRay x 0 s) = spatialNormSq x := by
proof body
Term-mode proof.
175 unfold spatialNormSq
176 have h1 : (coordRay x 0 s) 1 = x 1 := coordRay_temporal_spatial x s 1 (by decide)
177 have h2 : (coordRay x 0 s) 2 = x 2 := coordRay_temporal_spatial x s 2 (by decide)
178 have h3 : (coordRay x 0 s) 3 = x 3 := coordRay_temporal_spatial x s 3 (by decide)
179 rw [h1, h2, h3]
180
181/-- spatialRadius is invariant under temporal coordinate ray. -/