 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).
 233    - `ν ∈ {1,2,3}`: only the `ν`-th spatial component changes by `s`, so
 234      `spatialNormSq (coordRay x ν s) = ‖x‖² + 2 s · x_ν + s²`. Using `|x_ν| ≤ r`
 235      and `|s| < r/2`, the polynomial lower bound `(r - |s|)² ≤ ‖x‖² + 2 s x_ν + s²`
 236      gives `spatialNormSq > 0` and hence `spatialRadius ≠ 0`.
 237
 238    Closes one of the §XXIII.B′ Mathlib calculus axioms. -/
 239theorem spatialRadius_coordRay_ne_zero (x : Fin 4 → ℝ) (ν : Fin 4) (s : ℝ)
 240    (hx : spatialRadius x ≠ 0) (hs : |s| < spatialRadius x / 2) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.