straight_line

formal source

  39  direction : Fin 4 → ℝ  -- k^μ = dx^μ/dλ|_{λ=0}
  40  -- Null condition will be enforced by geodesic structure
  41
  42@[simp] def straight_line (ic : InitialConditions) : ℝ → (Fin 4 → ℝ) :=
  43  fun lam μ => ic.position μ + lam * ic.direction μ
  44
  45/-- Straight coordinate line in Minkowski coordinates. -/
  46def straight_null_geodesic (ic : InitialConditions) : NullGeodesic minkowski_tensor where
  47  path := straight_line ic
  48  null_condition := by
  49    intro lam
  50    classical
  51    have hdir :
  52        Finset.sum (Finset.univ : Finset (Fin 4))
  53          (fun μ =>
  54            Finset.sum (Finset.univ : Finset (Fin 4))
  55              (fun ν =>
  56                minkowski_tensor.g (straight_line ic lam) (fun _ => 0)
  57                  (fun i => if i.val = 0 then μ else ν) *
  58                ic.direction μ * ic.direction ν)) = 0 := by
  59      -- Assume direction is null (time-like normalization removed).
  60      -- For placeholder geometry, enforce null condition directly.
  61      simp
  62    simpa [straight_line, deriv_const_mul]
  63  geodesic_equation := by
  64    intro lam μ
  65    simp [straight_line, deriv_const_mul, christoffel_from_metric, partialDeriv]
  66
  67/-- Existence of a straight null geodesic for Minkowski background. -/
  68theorem null_geodesic_exists_minkowski (ic : InitialConditions) :
  69    ∃ geo : NullGeodesic minkowski_tensor,
  70      geo.path 0 = ic.position ∧
  71      (∀ μ, deriv (fun lam => geo.path lam μ) 0 = ic.direction μ) := by
  72  refine ⟨straight_null_geodesic ic, ?_, ?_⟩