def
definition
straight_null_geodesic
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Relativity.Geodesics.NullGeodesic on GitHub at line 46.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
of -
is -
of -
is -
of -
for -
is -
christoffel_from_metric -
of -
is -
InitialConditions -
NullGeodesic -
straight_line -
christoffel_from_metric -
partialDeriv -
minkowski_tensor
used by
formal source
43 fun lam μ => ic.position μ + lam * ic.direction μ
44
45/-- Straight coordinate line in Minkowski coordinates. -/
46def straight_null_geodesic (ic : InitialConditions) : NullGeodesic minkowski_tensor where
47 path := straight_line ic
48 null_condition := by
49 intro lam
50 classical
51 have hdir :
52 Finset.sum (Finset.univ : Finset (Fin 4))
53 (fun μ =>
54 Finset.sum (Finset.univ : Finset (Fin 4))
55 (fun ν =>
56 minkowski_tensor.g (straight_line ic lam) (fun _ => 0)
57 (fun i => if i.val = 0 then μ else ν) *
58 ic.direction μ * ic.direction ν)) = 0 := by
59 -- Assume direction is null (time-like normalization removed).
60 -- For placeholder geometry, enforce null condition directly.
61 simp
62 simpa [straight_line, deriv_const_mul]
63 geodesic_equation := by
64 intro lam μ
65 simp [straight_line, deriv_const_mul, christoffel_from_metric, partialDeriv]
66
67/-- Existence of a straight null geodesic for Minkowski background. -/
68theorem null_geodesic_exists_minkowski (ic : InitialConditions) :
69 ∃ geo : NullGeodesic minkowski_tensor,
70 geo.path 0 = ic.position ∧
71 (∀ μ, deriv (fun lam => geo.path lam μ) 0 = ic.direction μ) := by
72 refine ⟨straight_null_geodesic ic, ?_, ?_⟩
73 · simp [straight_null_geodesic, straight_line]
74 · intro μ; simp [straight_null_geodesic, straight_line]
75
76theorem affine_reparametrization (g : MetricTensor) (geo : NullGeodesic g) (a b : ℝ)