geodesic_unique
plain-language theorem explainer
Null geodesics are uniquely determined by shared initial position and direction in the Recognition Science relativity scaffolding. Workers on gravitational lensing and light deflection would invoke this uniqueness when tracing photon paths from initial data. The argument reduces the geodesic equation to a second-order linear ODE whose explicit solution is the straight line fixed by the supplied initial conditions.
Claim. Let $g$ be a metric tensor, $ic$ initial conditions consisting of position $x_0^μ$ and direction $k^μ$, and let $γ_1, γ_2$ be two null geodesics for $g$. If $γ_1(0) = γ_2(0) = x_0$ and $˙γ_1(0)^μ = ˙γ_2(0)^μ = k^μ$ for each component $μ$, then $γ_1(λ)^μ = γ_2(λ)^μ$ for all affine parameter $λ$ and index $μ$.
background
The module implements null geodesics for light propagation: paths satisfy the null condition $g_{μν} ˙x^μ ˙x^ν = 0$ together with the geodesic equation. InitialConditions is the structure supplying position $x^μ(0)$ and direction $k^μ = dx^μ/dλ|_{λ=0}$. NullGeodesic bundles a path function with both the null condition and the second-order geodesic equation involving Christoffel symbols. Upstream results supply the MetricTensor interface and the definition christoffel_from_metric that builds connection coefficients from metric derivatives and partialDeriv.
proof idea
Fix arbitrary affine parameter value and component index. Simplify each geodesic equation via christoffel_from_metric and partialDeriv to obtain a linear second-order ODE. Apply the lemma second_order_linear_solution to recover the explicit straight-line form $x^μ(λ) = x^μ(0) + λ k^μ$ for each path. Direct substitution of the shared initial data then shows the two paths coincide.
why it matters
This uniqueness result supports computation of light propagation and gravitational lensing deflection angles in the Recognition framework, as stated in the module documentation. It closes the local uniqueness step for null geodesics before extension to curved metrics. The result aligns with the T8 spatial dimension and the overall forcing chain by ensuring deterministic light paths from initial data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.