Physlib.Relativity.Tensors.RealTensor.Vector.Causality.LightLike

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Matteo Cipollina, Joseph Tooby-Smith
-/
module

public import Physlib.Relativity.Tensors.RealTensor.Vector.Causality.Basic

Properties of light like vectors

              @[expose] public sectionlemma lightLike_iff_norm_sq_zero {d : ℕ} (p : Vector d) :
    causalCharacter p = CausalCharacter.lightLike ↔ ⟪p, p⟫ₘ = 0 := byd:ℕp:Vector d⊢ p.causalCharacter = CausalCharacter.lightLike ↔ (minkowskiProduct p) p = 0
  simp only [causalCharacter]d:ℕp:Vector d⊢ (if (minkowskiProduct p) p = 0 then CausalCharacter.lightLike
    else if 0 < (minkowskiProduct p) p then CausalCharacter.timeLike else CausalCharacter.spaceLike) =
    CausalCharacter.lightLike ↔
  (minkowskiProduct p) p = 0
  split_ifs with h h2posd:ℕp:Vector dh:(minkowskiProduct p) p = 0⊢ CausalCharacter.lightLike = CausalCharacter.lightLike ↔ (minkowskiProduct p) p = 0posd:ℕp:Vector dh:¬(minkowskiProduct p) p = 0h2:0 < (minkowskiProduct p) p⊢ False ↔ (minkowskiProduct p) p = 0negd:ℕp:Vector dh:¬(minkowskiProduct p) p = 0h2:¬0 < (minkowskiProduct p) p⊢ False ↔ (minkowskiProduct p) p = 0 <;>posd:ℕp:Vector dh:(minkowskiProduct p) p = 0⊢ CausalCharacter.lightLike = CausalCharacter.lightLike ↔ (minkowskiProduct p) p = 0posd:ℕp:Vector dh:¬(minkowskiProduct p) p = 0h2:0 < (minkowskiProduct p) p⊢ False ↔ (minkowskiProduct p) p = 0negd:ℕp:Vector dh:¬(minkowskiProduct p) p = 0h2:¬0 < (minkowskiProduct p) p⊢ False ↔ (minkowskiProduct p) p = 0 simp_allAll goals completed! 🐙  -- Zero vector has zero Minkowski norm squared
@[simp]
lemma causalCharacter_zero {d : ℕ} : causalCharacter (0 : Vector d) =
    CausalCharacter.lightLike := byd:ℕ⊢ causalCharacter 0 = CausalCharacter.lightLike
  simp [causalCharacter]All goals completed! 🐙

Causally preceding is reflexive

@[simp]
lemma causallyPrecedes_refl {d : ℕ} (p : Vector d) : causallyPrecedes p p := byd:ℕp:Vector d⊢ p.causallyPrecedes p
  simp [causallyPrecedes, pastLightConeBoundary]All goals completed! 🐙

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


lemma lightlike_eq_spatial_norm_of_eq_time {d : ℕ} {v w : Vector d}
    (hv : causalCharacter v = .lightLike) (hw : causalCharacter w = .lightLike)
    (h_time : timeComponent v = timeComponent w) :
    ⟪spatialPart v, spatialPart v⟫_ℝ = ⟪spatialPart w, spatialPart w⟫_ℝ := byd:ℕv:Vector dw:Vector dhv:v.causalCharacter = CausalCharacter.lightLikehw:w.causalCharacter = CausalCharacter.lightLikeh_time:v.timeComponent = w.timeComponent⊢ ⟪v.spatialPart, v.spatialPart⟫_ℝ = ⟪w.spatialPart, w.spatialPart⟫_ℝ
  rw [lightLike_iff_norm_sq_zero,d:ℕv:Vector dw:Vector dhv:(minkowskiProduct v) v = 0hw:(minkowskiProduct w) w = 0h_time:v.timeComponent = w.timeComponent⊢ ⟪v.spatialPart, v.spatialPart⟫_ℝ = ⟪w.spatialPart, w.spatialPart⟫_ℝd:ℕv:Vector dw:Vector dhv:v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i) = 0hw:w (Sum.inl 0) * w (Sum.inl 0) - ∑ i, w (Sum.inr i) * w (Sum.inr i) = 0h_time:v.timeComponent = w.timeComponent⊢ ⟪v.spatialPart, v.spatialPart⟫_ℝ = ⟪w.spatialPart, w.spatialPart⟫_ℝ minkowskiProduct_toCoordd:ℕv:Vector dw:Vector dhv:v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i) = 0hw:w (Sum.inl 0) * w (Sum.inl 0) - ∑ i, w (Sum.inr i) * w (Sum.inr i) = 0h_time:v.timeComponent = w.timeComponent⊢ ⟪v.spatialPart, v.spatialPart⟫_ℝ = ⟪w.spatialPart, w.spatialPart⟫_ℝd:ℕv:Vector dw:Vector dhv:v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i) = 0hw:w (Sum.inl 0) * w (Sum.inl 0) - ∑ i, w (Sum.inr i) * w (Sum.inr i) = 0h_time:v.timeComponent = w.timeComponent⊢ ⟪v.spatialPart, v.spatialPart⟫_ℝ = ⟪w.spatialPart, w.spatialPart⟫_ℝ] at hv hwd:ℕv:Vector dw:Vector dhv:v (Sum.inl 0) * v (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i) = 0hw:w (Sum.inl 0) * w (Sum.inl 0) - ∑ i, w (Sum.inr i) * w (Sum.inr i) = 0h_time:v.timeComponent = w.timeComponent⊢ ⟪v.spatialPart, v.spatialPart⟫_ℝ = ⟪w.spatialPart, w.spatialPart⟫_ℝ
  rw [show v (Sum.inl 0) = w (Sum.inl 0) from h_timed:ℕv:Vector dw:Vector dhv:w (Sum.inl 0) * w (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i) = 0hw:w (Sum.inl 0) * w (Sum.inl 0) - ∑ i, w (Sum.inr i) * w (Sum.inr i) = 0h_time:v.timeComponent = w.timeComponent⊢ ⟪v.spatialPart, v.spatialPart⟫_ℝ = ⟪w.spatialPart, w.spatialPart⟫_ℝd:ℕv:Vector dw:Vector dhv:w (Sum.inl 0) * w (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i) = 0hw:w (Sum.inl 0) * w (Sum.inl 0) - ∑ i, w (Sum.inr i) * w (Sum.inr i) = 0h_time:v.timeComponent = w.timeComponent⊢ ⟪v.spatialPart, v.spatialPart⟫_ℝ = ⟪w.spatialPart, w.spatialPart⟫_ℝ] at hvd:ℕv:Vector dw:Vector dhv:w (Sum.inl 0) * w (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i) = 0hw:w (Sum.inl 0) * w (Sum.inl 0) - ∑ i, w (Sum.inr i) * w (Sum.inr i) = 0h_time:v.timeComponent = w.timeComponent⊢ ⟪v.spatialPart, v.spatialPart⟫_ℝ = ⟪w.spatialPart, w.spatialPart⟫_ℝ
  simp only [PiLp.inner_apply, spatialPart, RCLike.inner_apply, conj_trivial]d:ℕv:Vector dw:Vector dhv:w (Sum.inl 0) * w (Sum.inl 0) - ∑ i, v (Sum.inr i) * v (Sum.inr i) = 0hw:w (Sum.inl 0) * w (Sum.inl 0) - ∑ i, w (Sum.inr i) * w (Sum.inr i) = 0h_time:v.timeComponent = w.timeComponent⊢ ∑ x, v (Sum.inr x) * v (Sum.inr x) = ∑ x, w (Sum.inr x) * w (Sum.inr x)
  linarithAll goals completed! 🐙

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

set_option linter.unusedVariables false in


-- `unusedArguments` (newly flagged under v4.32.0): the lightlike hypotheses are
-- part of the intended interface but not needed by the current proof.
@[nolint unusedArguments]
lemma lightlike_spatial_parallel_implies_proportional {d : ℕ} {v w : Vector d}
    (hv : causalCharacter v = .lightLike) (hw : causalCharacter w = .lightLike)
    (h_spatial_parallel : ∃ (r : ℝ), v = r • w) :
    ∃ (r : ℝ), |v (Sum.inl 0)| = |r| * |w (Sum.inl 0)| := byd:ℕv:Vector dw:Vector dhv:v.causalCharacter = CausalCharacter.lightLikehw:w.causalCharacter = CausalCharacter.lightLikeh_spatial_parallel:∃ r, v = r • w⊢ ∃ r, |v (Sum.inl 0)| = |r| * |w (Sum.inl 0)|
  rcases h_spatial_parallel with ⟨r, hr⟩d:ℕv:Vector dw:Vector dhv:v.causalCharacter = CausalCharacter.lightLikehw:w.causalCharacter = CausalCharacter.lightLiker:ℝhr:v = r • w⊢ ∃ r, |v (Sum.inl 0)| = |r| * |w (Sum.inl 0)|
  refine ⟨r, ?_⟩d:ℕv:Vector dw:Vector dhv:v.causalCharacter = CausalCharacter.lightLikehw:w.causalCharacter = CausalCharacter.lightLiker:ℝhr:v = r • w⊢ |v (Sum.inl 0)| = |r| * |w (Sum.inl 0)|
  rw [hrd:ℕv:Vector dw:Vector dhv:v.causalCharacter = CausalCharacter.lightLikehw:w.causalCharacter = CausalCharacter.lightLiker:ℝhr:v = r • w⊢ |(r • w) (Sum.inl 0)| = |r| * |w (Sum.inl 0)|d:ℕv:Vector dw:Vector dhv:v.causalCharacter = CausalCharacter.lightLikehw:w.causalCharacter = CausalCharacter.lightLiker:ℝhr:v = r • w⊢ |(r • w) (Sum.inl 0)| = |r| * |w (Sum.inl 0)|]d:ℕv:Vector dw:Vector dhv:v.causalCharacter = CausalCharacter.lightLikehw:w.causalCharacter = CausalCharacter.lightLiker:ℝhr:v = r • w⊢ |(r • w) (Sum.inl 0)| = |r| * |w (Sum.inl 0)|
  simp [abs_mul]All goals completed! 🐙