null_geodesic_exists_minkowski
plain-language theorem explainer
In Minkowski spacetime, any initial position and direction admit a straight null geodesic satisfying those data at affine parameter zero. Researchers computing light propagation or lensing angles would cite this existence result as the flat-space base case. The proof is a one-line term wrapper that supplies the explicit straight_null_geodesic construction and discharges the initial-condition equalities by simplification.
Claim. Given an initial position $x^0$ and direction $k^0$ in Minkowski spacetime, there exists a null geodesic path $x^0(λ)$ such that $x^0(0) = x^0$ and $dx^0/dλ|_{λ=0} = k^0$.
background
The module treats null geodesics for light rays, requiring paths whose interval vanishes under the metric. InitialConditions is the structure holding a four-vector position and a four-vector direction at affine parameter zero. NullGeodesic packages a path function together with the null-condition sum $g_{μν} dx^μ/dλ dx^ν/dλ = 0$ and the geodesic equation. straight_line defines the coordinate path $x^μ + λ k^μ$, while straight_null_geodesic assembles that path into a NullGeodesic instance over the Minkowski metric. minkowski_tensor supplies the flat metric η_{μν}.
proof idea
The term proof refines the existential by supplying straight_null_geodesic ic. Two simp calls then rewrite the path and derivative fields using the definitions of straight_null_geodesic and straight_line, discharging both conjuncts.
why it matters
The result supplies the Minkowski null-geodesic existence statement required by the module's light-propagation foundation. It anchors downstream calculations of deflection angles and time delays. Within the Recognition Science setting it provides the flat-space limit against which curvature corrections are compared.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.