spatialNormSq_coordRay_spatial_1

formal source

 199
 200/-- Helper: closed form of `spatialNormSq (coordRay x j s)` when `j` is a fixed
 201    spatial index. The sum changes only at index `j`, where `x j` becomes `x j + s`. -/
 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
 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
 210private lemma spatialNormSq_coordRay_spatial_2 (x : Fin 4 → ℝ) (s : ℝ) :
 211    spatialNormSq (coordRay x 2 s) = x 1 ^ 2 + (x 2 + s) ^ 2 + x 3 ^ 2 := by
 212  unfold spatialNormSq coordRay basisVec
 213  rw [if_neg (by decide : (1 : Fin 4) ≠ 2),
 214      if_pos (rfl : (2 : Fin 4) = 2),
 215      if_neg (by decide : (3 : Fin 4) ≠ 2)]
 216  ring
 217
 218private lemma spatialNormSq_coordRay_spatial_3 (x : Fin 4 → ℝ) (s : ℝ) :
 219    spatialNormSq (coordRay x 3 s) = x 1 ^ 2 + x 2 ^ 2 + (x 3 + s) ^ 2 := by
 220  unfold spatialNormSq coordRay basisVec
 221  rw [if_neg (by decide : (1 : Fin 4) ≠ 3),
 222      if_neg (by decide : (2 : Fin 4) ≠ 3),
 223      if_pos (rfl : (3 : Fin 4) = 3)]
 224  ring
 225
 226/-- `spatialRadius` stays nonzero under sufficiently small coordinate perturbations.
 227
 228    Quantitative version: if `r = spatialRadius x ≠ 0` and `|s| < r/2`, then the
 229    perturbed point `coordRay x ν s = x + s · e_ν` still has nonzero spatial radius.
 230
 231    Proof: case-split on `ν ∈ {0,1,2,3}`.
 232    - `ν = 0`: temporal direction, `spatialRadius (coordRay x 0 s) = spatialRadius x` (proved).