`RealNullGeodesic`

definition

show as: view math explainer →

module: IndisputableMonolith.Relativity.Geometry.MetricUnification
domain: Relativity
line: 130 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.Geometry.MetricUnification on GitHub at line 130.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 127        (deriv (fun lam' => path lam' ν) lam))) < 0
 128
 129/-- A null geodesic using real Christoffel symbols. -/
 130structure RealNullGeodesic (g : MetricTensor) extends RealGeodesic g where
 131  null_condition : ∀ lam : ℝ,
 132    Finset.sum Finset.univ (fun μ =>
 133      Finset.sum Finset.univ (fun ν =>
 134        g.g (path lam) (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
 135        (deriv (fun lam' => path lam' μ) lam) *
 136        (deriv (fun lam' => path lam' ν) lam))) = 0
 137
 138/-- A spacelike geodesic: path with positive interval, using real Christoffel. -/
 139structure SpacelikeGeodesic (g : MetricTensor) extends RealGeodesic g where
 140  spacelike_condition : ∀ lam : ℝ,
 141    0 < Finset.sum Finset.univ (fun μ =>
 142      Finset.sum Finset.univ (fun ν =>
 143        g.g (path lam) (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
 144        (deriv (fun lam' => path lam' μ) lam) *
 145        (deriv (fun lam' => path lam' ν) lam)))
 146
 147/-- Proof that `RealGeodesic` uses the real Christoffel symbols from `Curvature.christoffel`,
 148    not the scaffold `Connection.christoffel_from_metric`. -/
 149theorem geodesic_uses_real_christoffel (g : MetricTensor) (geo : RealGeodesic g)
 150    (lam : ℝ) (μ : Fin 4) :
 151    deriv (deriv (fun lam' => geo.path lam' μ)) lam +
 152    Finset.sum Finset.univ (fun ρ =>
 153      Finset.sum Finset.univ (fun σ =>
 154        christoffel g (geo.path lam) μ ρ σ *
 155        (deriv (fun lam' => geo.path lam' ρ) lam) *
 156        (deriv (fun lam' => geo.path lam' σ) lam))) = 0 :=
 157  geo.geodesic_equation lam μ
 158
 159/-- Straight lines are geodesics of Minkowski spacetime (using real Christoffel). -/
 160theorem minkowski_straight_line_geodesic (x₀ v : Fin 4 → ℝ) :

papers checked against this theorem

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