SpacetimeCurve

formal source

  41/-! ## §1 Curves in Spacetime -/
  42
  43/-- A smooth curve in 4D spacetime, parameterized by λ. -/
  44structure SpacetimeCurve where
  45  path : ℝ → (Fin 4 → ℝ)
  46  tangent : ℝ → (Fin 4 → ℝ) := fun lam μ => deriv (fun l => path l μ) lam
  47
  48/-! ## §2 Parallel Transport Along a Curve -/
  49
  50/-- A vector field V along a curve γ is parallel-transported if
  51    DV^μ/dλ + Γ^μ_{αβ} (dγ^α/dλ) V^β = 0.
  52
  53    This is the defining ODE for parallel transport. -/
  54def ParallelTransported (g : MetricTensor) (γ : SpacetimeCurve)
  55    (V : ℝ → (Fin 4 → ℝ)) : Prop :=
  56  ∀ lam μ,
  57    deriv (fun l => V l μ) lam +
  58    Finset.univ.sum (fun α =>
  59      Finset.univ.sum (fun β =>
  60        christoffel g (γ.path lam) μ α β *
  61        γ.tangent lam α *
  62        V lam β)) = 0
  63
  64/-- Smoothness of a vector field along the affine parameter. -/
  65def SmoothField (V : ℝ → (Fin 4 → ℝ)) : Prop :=
  66  ∀ μ, Differentiable ℝ (fun l => V l μ)
  67
  68/-- Initial conditions for parallel transport: a vector at parameter λ₀. -/
  69structure ParallelTransportIC where
  70  lam0 : ℝ
  71  V0 : Fin 4 → ℝ
  72
  73/-- A parallel-transported vector field satisfying initial conditions. -/
  74structure ParallelTransportSolution (g : MetricTensor) (γ : SpacetimeCurve)