NullGeodesic
plain-language theorem explainer
NullGeodesic encodes a curve in four-dimensional spacetime whose tangent satisfies the null condition with respect to a given metric and obeys the geodesic equation built from the associated Christoffel symbols. Workers modeling photon trajectories and gravitational lensing cite the structure when formulating initial-value problems for lightlike paths. The declaration is a direct structure definition that assembles the path map together with the two pointwise physical requirements.
Claim. A null geodesic relative to metric tensor $g$ is a map $x:ℝ→ℝ^4$ such that for every affine parameter $λ$ the contraction $g_{μν}(x(λ)) (dx^μ/dλ)(dx^ν/dλ)=0$ holds and the geodesic equation $d²x^μ/dλ² + Γ^μ_{ρσ}(x(λ)) (dx^ρ/dλ)(dx^σ/dλ)=0$ is satisfied componentwise, where the Christoffel symbols $Γ$ are obtained from $g$ via the standard construction.
background
The module treats null geodesics as the trajectories of light, requiring both vanishing interval length and parallel transport of the tangent vector. MetricTensor supplies the local bilinear form $g$ at each spacetime point; christoffel_from_metric assembles the connection coefficients from $g$ and its first derivatives. Upstream results include the non-sealed metric interface in Foundation.Hamiltonian and the Christoffel definition in Gravity.Connection, both of which are instantiated here without additional sealing assumptions.
proof idea
The declaration is a structure definition. It directly specifies the path function together with the null_condition (double sum over indices of $g_{μν}ẋ^μẋ^ν$) and the geodesic_equation (second derivative plus Christoffel contraction). No lemmas or tactics are invoked; the body is empty because the object is introduced by definition rather than by proof.
why it matters
NullGeodesic is the basic object for all later results in the module. It is instantiated by straight_null_geodesic and null_geodesic_exists_minkowski to produce explicit Minkowski solutions, and it supplies the input type for affine_reparametrization and geodesic_unique. The structure therefore anchors the Recognition Science treatment of light propagation, enabling downstream calculations of deflection angles and time delays while remaining compatible with the metric interface inherited from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.