minkowski_straight_line_is_geodesic
plain-language theorem explainer
Straight coordinate lines in Minkowski space are null geodesics whenever the initial four-velocity satisfies the lightlike condition. Workers on light propagation and gravitational lensing in flat spacetime cite this result to anchor explicit path constructions. The proof builds an InitialConditions record from the given position and direction, applies the straight_null_geodesic constructor, and confirms path identity by simplification.
Claim. Let $x_0^μ$ and $k^μ$ be four-vectors in Minkowski space satisfying $g_{μν}k^μk^ν=0$. Define the affine path $x^μ(λ)=x_0^μ+λk^μ$. Then there exists a null geodesic $γ$ with respect to the Minkowski metric such that $γ(λ)=x(λ)$ for every affine parameter $λ$.
background
The module implements null geodesics as structures carrying a path function together with the zero-interval condition $g_{μν}(dx^μ/dλ)(dx^ν/dλ)=0$, using the affine parameter λ. InitialConditions packages a starting four-position and four-direction; straight_line then produces the linear parametrization $x^μ(λ)=x_0^μ+λk^μ$. The straight_null_geodesic definition assembles these into a full NullGeodesic instance over the Minkowski tensor, enforcing the null condition by direct substitution into the metric. Upstream, inverse_metric supplies the contravariant components needed to state the null condition in the theorem hypothesis.
proof idea
The tactic proof first invokes classical reasoning, constructs an InitialConditions record from the supplied position and direction, then refines the goal to the pair consisting of straight_null_geodesic applied to that record together with a path-equality subgoal. The final simp step unfolds straight_null_geodesic, straight_line and the local path definition to discharge the equality by reflexivity.
why it matters
The result supplies the flat-space base case for null geodesics inside the Recognition Science relativity module, directly supporting explicit light-ray calculations that feed into lensing deflection and time-delay formulas. It closes the elementary construction step before any curvature is introduced, consistent with the module's stated purpose of providing the foundation for gravitational lensing and time delays. No downstream uses are recorded yet, leaving open its integration into larger geodesic-uniqueness or curved-space statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.