spatialNormSq_coordRay_spatial_1
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not treat perturbations along the time axis or spatial indices 2 and 3.
- Does not supply inequalities, bounds, or stability estimates.
- Applies only to the Euclidean spatial norm, not the full Minkowski metric.
formal statement (Lean)
202private lemma spatialNormSq_coordRay_spatial_1 (x : Fin 4 → ℝ) (s : ℝ) :
203 spatialNormSq (coordRay x 1 s) = (x 1 + s) ^ 2 + x 2 ^ 2 + x 3 ^ 2 := by
proof body
Term-mode proof.
204 unfold spatialNormSq coordRay basisVec
205 rw [if_pos (rfl : (1 : Fin 4) = 1),
206 if_neg (by decide : (2 : Fin 4) ≠ 1),
207 if_neg (by decide : (3 : Fin 4) ≠ 1)]
208 ring
209