NullGeodesic
plain-language theorem explainer
NullGeodesic defines a curve whose tangent satisfies the lightlike condition with respect to a metric tensor and obeys the geodesic equation built from the associated Christoffel symbols. Researchers formalizing photon paths or lensing in curved spacetime cite this structure when they need an explicit object obeying both constraints simultaneously. The definition assembles the path map and the two differential conditions directly from the imported MetricTensor and christoffel_from_metric without further lemmas.
Claim. A null geodesic relative to a metric tensor $g$ is a map $x:ℝ→ℝ^4$ such that $g_{μν}(x(λ)) (dx^μ/dλ)(dx^ν/dλ)=0$ for every affine parameter $λ$, and the second-order equation $d²x^μ/dλ² + Γ^μ_{ρσ}(x(λ)) (dx^ρ/dλ)(dx^σ/dλ)=0$ holds, where the Christoffel symbols $Γ$ are those constructed from $g$.
background
The module supplies the mathematical object for lightlike curves in four-dimensional spacetime. MetricTensor (from Foundation.Hamiltonian and Relativity.Geometry) supplies the local bilinear form $g$ at each point. christoffel_from_metric (from Gravity.Connection and Relativity.Geometry.Connection) produces the connection coefficients $Γ^ρ_{μν}$ from the metric and its first derivatives. The module doc states the purpose is to implement null geodesics for light propagation with $g_{μν} dx^μ dx^ν =0$ and the geodesic equation, forming the basis for lensing and time-delay calculations.
proof idea
The declaration is a structure definition that directly encodes the path together with the two required conditions; no tactics or lemmas are applied.
why it matters
NullGeodesic is the central type in the module and is instantiated by straight_null_geodesic and null_geodesic_exists_minkowski; it is the input to affine_reparametrization and geodesic_unique. It supplies the concrete object needed for light propagation inside the Recognition Science relativity layer once the metric and connection have been fixed upstream. The structure therefore closes the interface between the general MetricTensor and the concrete null-path theorems used for deflection-angle computations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.