Properties of light like vectors

theorem Lorentz.Vector.lightLike_iff_norm_sq_zero {d : ℕ} (p : Vector d) : p.causalCharacter = CausalCharacter.lightLike ↔ (minkowskiProduct p) p = 0

@[simp]

theorem Lorentz.Vector.causalCharacter_zero {d : ℕ} : causalCharacter 0 = CausalCharacter.lightLike

@[simp]

theorem Lorentz.Vector.causallyPrecedes_refl {d : ℕ} (p : Vector d) : p.causallyPrecedes p

Causally preceding is reflexive

theorem Lorentz.Vector.lightlike_eq_spatial_norm_of_eq_time {d : ℕ} {v w : Vector d} (hv : v.causalCharacter = CausalCharacter.lightLike) (hw : w.causalCharacter = CausalCharacter.lightLike) (h_time : v.timeComponent = w.timeComponent) : inner ℝ v.spatialPart v.spatialPart = inner ℝ w.spatialPart w.spatialPart

For two lightlike vectors with equal time components, their spatial parts have equal Euclidean norms

theorem Lorentz.Vector.lightlike_spatial_parallel_implies_proportional {d : ℕ} {v w : Vector d} (hv : v.causalCharacter = CausalCharacter.lightLike) (hw : w.causalCharacter = CausalCharacter.lightLike) (h_spatial_parallel : ∃ (r : ℝ), v = r • w) : ∃ (r : ℝ), |v (Sum.inl 0)| = |r| * |w (Sum.inl 0)|

If two lightlike vectors have parallel spatial components, their temporal components must also be proportional, which implies the entire vectors are proportional