spatialRadius_coordRay_ne_zero

proof body

Tactic-mode proof.

 242  rw [spatialRadius_ne_zero_iff]
 243  have hr_pos : 0 < spatialRadius x := spatialRadius_pos_of_ne_zero x hx
 244  have hr_sq : spatialRadius x ^ 2 = spatialNormSq x := by
 245    unfold spatialRadius; rw [Real.sq_sqrt (spatialNormSq_nonneg x)]
 246  have h_s_lo : -(spatialRadius x / 2) < s := (abs_lt.mp hs).1
 247  have h_s_hi : s < spatialRadius x / 2 := (abs_lt.mp hs).2
 248  have h_x1_le : x 1 ^ 2 ≤ spatialRadius x ^ 2 := hr_sq ▸ sq_le_spatialNormSq_1 x
 249  have h_x2_le : x 2 ^ 2 ≤ spatialRadius x ^ 2 := hr_sq ▸ sq_le_spatialNormSq_2 x
 250  have h_x3_le : x 3 ^ 2 ≤ spatialRadius x ^ 2 := hr_sq ▸ sq_le_spatialNormSq_3 x
 251  -- Case split on ν using its underlying ℕ.
 252  obtain ⟨k, hk⟩ := ν
 253  match k, hk with
 254  | 0, _ =>
 255    rw [show ((⟨0, by decide⟩ : Fin 4) = (0 : Fin 4)) from rfl,
 256        spatialNormSq_coordRay_temporal]
 257    exact (spatialRadius_ne_zero_iff x).mp hx
 258  | 1, _ =>
 259    rw [show ((⟨1, by decide⟩ : Fin 4) = (1 : Fin 4)) from rfl,
 260        spatialNormSq_coordRay_spatial_1]
 261    intro h_zero
 262    have h_sq1 : (x 1 + s) ^ 2 = 0 := by
 263      nlinarith [sq_nonneg (x 1 + s), sq_nonneg (x 2), sq_nonneg (x 3)]
 264    have h_sq2 : x 2 ^ 2 = 0 := by
 265      nlinarith [sq_nonneg (x 1 + s), sq_nonneg (x 2), sq_nonneg (x 3)]
 266    have h_sq3 : x 3 ^ 2 = 0 := by
 267      nlinarith [sq_nonneg (x 1 + s), sq_nonneg (x 2), sq_nonneg (x 3)]
 268    have h_eq1 : x 1 + s = 0 := sq_eq_zero_iff.mp h_sq1
 269    have h_eq2 : x 2 = 0 := sq_eq_zero_iff.mp h_sq2
 270    have h_eq3 : x 3 = 0 := sq_eq_zero_iff.mp h_sq3
 271    have h_sn_eq : spatialNormSq x = s ^ 2 := by
 272      show x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2 = s ^ 2
 273      have h_x1 : x 1 = -s := by linarith
 274      rw [h_x1, h_eq2, h_eq3]; ring
 275    have h_r_sq_eq_s_sq : spatialRadius x ^ 2 = s ^ 2 := by rw [hr_sq, h_sn_eq]
 276    -- r > 0 and r² = s², so r = √(s²) = |s|. Then |s| < r/2 = |s|/2 contradicts |s| ≥ 0 ∧ r > 0.
 277    have h_r_eq_abs : spatialRadius x = |s| := by
 278      have h_pos : 0 ≤ spatialRadius x := le_of_lt hr_pos
 279      have h_abs_pos : 0 ≤ |s| := abs_nonneg s
 280      have h_eq : Real.sqrt (spatialRadius x ^ 2) = Real.sqrt (s ^ 2) := by
 281        rw [h_r_sq_eq_s_sq]
 282      rw [Real.sqrt_sq h_pos] at h_eq
 283      rw [show s ^ 2 = |s| ^ 2 from (sq_abs s).symm, Real.sqrt_sq h_abs_pos] at h_eq
 284      exact h_eq
 285    rw [h_r_eq_abs] at hs
 286    linarith [abs_nonneg s]
 287  | 2, _ =>
 288    rw [show ((⟨2, by decide⟩ : Fin 4) = (2 : Fin 4)) from rfl,
 289        spatialNormSq_coordRay_spatial_2]
 290    intro h_zero
 291    have h_sq1 : x 1 ^ 2 = 0 := by
 292      nlinarith [sq_nonneg (x 1), sq_nonneg (x 2 + s), sq_nonneg (x 3)]
 293    have h_sq2 : (x 2 + s) ^ 2 = 0 := by
 294      nlinarith [sq_nonneg (x 1), sq_nonneg (x 2 + s), sq_nonneg (x 3)]
 295    have h_sq3 : x 3 ^ 2 = 0 := by
 296      nlinarith [sq_nonneg (x 1), sq_nonneg (x 2 + s), sq_nonneg (x 3)]
 297    have h_eq1 : x 1 = 0 := sq_eq_zero_iff.mp h_sq1
 298    have h_eq2 : x 2 + s = 0 := sq_eq_zero_iff.mp h_sq2
 299    have h_eq3 : x 3 = 0 := sq_eq_zero_iff.mp h_sq3
 300    have h_sn_eq : spatialNormSq x = s ^ 2 := by
 301      show x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2 = s ^ 2
 302      have h_x2 : x 2 = -s := by linarith
 303      rw [h_eq1, h_x2, h_eq3]; ring
 304    have h_r_sq_eq_s_sq : spatialRadius x ^ 2 = s ^ 2 := by rw [hr_sq, h_sn_eq]
 305    have h_r_eq_abs : spatialRadius x = |s| := by
 306      have h_pos : 0 ≤ spatialRadius x := le_of_lt hr_pos
 307      have h_abs_pos : 0 ≤ |s| := abs_nonneg s
 308      have h_eq : Real.sqrt (spatialRadius x ^ 2) = Real.sqrt (s ^ 2) := by
 309        rw [h_r_sq_eq_s_sq]
 310      rw [Real.sqrt_sq h_pos] at h_eq
 311      rw [show s ^ 2 = |s| ^ 2 from (sq_abs s).symm, Real.sqrt_sq h_abs_pos] at h_eq
 312      exact h_eq
 313    rw [h_r_eq_abs] at hs
 314    linarith [abs_nonneg s]
 315  | 3, _ =>
 316    rw [show ((⟨3, by decide⟩ : Fin 4) = (3 : Fin 4)) from rfl,
 317        spatialNormSq_coordRay_spatial_3]
 318    intro h_zero
 319    have h_sq1 : x 1 ^ 2 = 0 := by
 320      nlinarith [sq_nonneg (x 1), sq_nonneg (x 2), sq_nonneg (x 3 + s)]
 321    have h_sq2 : x 2 ^ 2 = 0 := by
 322-- ... 25 more lines elided ...