ParallelTransportSolution

formal source

  71  V0 : Fin 4 → ℝ
  72
  73/-- A parallel-transported vector field satisfying initial conditions. -/
  74structure ParallelTransportSolution (g : MetricTensor) (γ : SpacetimeCurve)
  75    (ic : ParallelTransportIC) where
  76  V : ℝ → (Fin 4 → ℝ)
  77  is_parallel : ParallelTransported g γ V
  78  initial_condition : V ic.lam0 = ic.V0
  79
  80/-! ## §3 Properties of Parallel Transport -/
  81
  82/-- In flat Minkowski spacetime, parallel transport is trivial:
  83    the Christoffel symbols vanish, so DV/dλ = dV/dλ = 0,
  84    meaning V is constant along any curve. -/
  85theorem parallel_transport_flat (γ : SpacetimeCurve)
  86    (V : ℝ → (Fin 4 → ℝ))
  87    (h_pt : ParallelTransported minkowski_tensor γ V) :
  88    ∀ lam μ, deriv (fun l => V l μ) lam = 0 := by
  89  intro lam μ
  90  have h := h_pt lam μ
  91  simp only [minkowski_christoffel_zero_proper, zero_mul, Finset.sum_const_zero, add_zero] at h
  92  exact h
  93
  94/-- Parallel transport preserves the metric inner product.
  95    If V, W are parallel-transported along γ, then g(V,W) is constant.
  96
  97    g_{μν} V^μ W^ν = const along γ
  98
  99    This is a consequence of metric compatibility ∇g = 0. -/
 100def ParallelTransportPreservesInnerProduct (g : MetricTensor) (γ : SpacetimeCurve) : Prop :=
 101  ∀ V W : ℝ → (Fin 4 → ℝ),
 102    SmoothField V →
 103    SmoothField W →
 104    ParallelTransported g γ V →