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)
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`. -/
depends on (11)
Lean names referenced from this declaration's body.
-
christoffel
in IndisputableMonolith.Action.EulerLagrange
decl_use
-
MetricTensor
in IndisputableMonolith.Foundation.Hamiltonian
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
christoffel_from_metric
in IndisputableMonolith.Gravity.Connection
decl_use
-
MetricTensor
in IndisputableMonolith.Gravity.Connection
decl_use
-
MetricTensor
in IndisputableMonolith.Meta.Homogenization
decl_use
-
that
in IndisputableMonolith.NumberTheory.PhiLadderLattice
decl_use
-
christoffel_from_metric
in IndisputableMonolith.Relativity.Geometry.Connection
decl_use
-
christoffel
in IndisputableMonolith.Relativity.Geometry.Curvature
decl_use
-
MetricTensor
in IndisputableMonolith.Relativity.Geometry.Metric
decl_use
-
RealGeodesic
in IndisputableMonolith.Relativity.Geometry.MetricUnification
decl_use