 233/-! ## §5 Certificate -/
 234
 235/-- Parallel transport certificate for a metric. -/
 236structure ParallelTransportCert (g : MetricTensor) : Prop where
 237  flat_trivial : ∀ (γ : SpacetimeCurve) (V : ℝ → (Fin 4 → ℝ)),
 238    g = minkowski_tensor → ParallelTransported g γ V →
 239    ∀ lam μ, deriv (fun l => V l μ) lam = 0
 240  inner_product_preserved : ∀ γ, ParallelTransportPreservesInnerProduct g γ
 241
 242/-- The parallel transport certificate holds for Minkowski. -/
 243theorem parallel_transport_cert_minkowski :
 244    ParallelTransportCert minkowski_tensor where
 245  flat_trivial := fun γ V h_eq h_pt => by
 246    simpa [h_eq] using parallel_transport_flat γ V h_pt
 247  inner_product_preserved := minkowski_preserves_inner
 248
 249end -- noncomputable section
 250
 251end Geometry
 252end Relativity
 253end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.