spatialNormSq_coordRay_spatial_1
plain-language theorem explainer
This lemma supplies the closed-form expansion of the squared spatial norm after a shift along the first spatial coordinate axis. Analysts deriving bounds on coordinate perturbations in relativistic settings invoke it to simplify norm calculations under linear displacements. The proof unfolds the three core definitions then reduces the expression by case analysis on basis components followed by ring simplification.
Claim. For any map $x : Fin 4 → ℝ$ and scalar $s ∈ ℝ$, the squared spatial norm of the perturbed point $x + s e_1$ equals $(x_1 + s)^2 + x_2^2 + x_3^2$.
background
The module defines the standard basis vector $e_μ$ by $e_μ(ν) = 1$ if $ν = μ$ and 0 otherwise. The coordinate ray is the affine line $x + t e_μ$. The spatial norm squared extracts the sum of squares of the three spatial components, discarding the time slot at index 0.
proof idea
Unfold spatialNormSq, coordRay and basisVec. Rewrite the first component via if_pos (equality at index 1) and the remaining two via if_neg (inequality at indices 2 and 3). Finish with the ring tactic.
why it matters
The lemma is invoked inside the proof of spatialRadius_coordRay_ne_zero, which shows that sufficiently small spatial shifts preserve nonzero radius. It supplies the explicit algebraic identity needed to handle the spatial case in the case split on direction index, closing a computational step in the derivatives layer of the relativity calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.