parallel_transport_flat

formal source

  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 →
 105    ParallelTransported g γ W →
 106    ∀ lam,
 107      deriv (fun l =>
 108        Finset.univ.sum (fun μ =>
 109          Finset.univ.sum (fun ν =>
 110            g.g (γ.path l) (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
 111            V l μ * W l ν))) lam = 0
 112
 113/-- For Minkowski, inner product preservation holds: g(V,W) is constant
 114    along any curve when V, W are parallel-transported (both constant in flat space).
 115