pith. machine review for the scientific record. sign in
def definition def or abbrev

straight_null_geodesic

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  46def straight_null_geodesic (ic : InitialConditions) : NullGeodesic minkowski_tensor where
  47  path := straight_line ic

proof body

Definition body.

  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. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.