NullGeodesic
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not construct or specialize any concrete metric tensor.
- Does not prove existence or uniqueness of solutions for given initial data.
- Does not address global properties such as geodesic completeness.
- Does not extend beyond the four-dimensional indexing used in the signature.
formal statement (Lean)
20structure NullGeodesic (g : MetricTensor) where
21 path : ℝ → (Fin 4 → ℝ)
22 null_condition : ∀ lam : ℝ,
23 Finset.sum (Finset.univ : Finset (Fin 4)) (fun μ =>
24 Finset.sum (Finset.univ : Finset (Fin 4)) (fun ν =>
25 g.g (path lam) (fun _ => 0) (fun i => if i.val = 0 then μ else ν) *
26 (deriv (fun lam' => path lam' μ) lam) *
27 (deriv (fun lam' => path lam' ν) lam))) = 0
28 geodesic_equation : ∀ lam μ,
29 deriv (deriv (fun lam' => path lam' μ)) lam +
30 Finset.sum (Finset.univ : Finset (Fin 4)) (fun ρ =>
31 Finset.sum (Finset.univ : Finset (Fin 4)) (fun σ =>
32 (christoffel_from_metric g).Γ (path lam) μ ρ σ *
33 (deriv (fun lam' => path lam' ρ) lam) *
34 (deriv (fun lam' => path lam' σ) lam))) = 0
35
36/-- Initial conditions for null geodesic. -/