straight_line
plain-language theorem explainer
straight_line parametrizes the coordinate path of a null geodesic in flat Minkowski spacetime as a linear function of the affine parameter. Researchers constructing explicit lightlike solutions in flat space reference it when building existence and verification theorems for null geodesics. It is realized as a direct functional definition that adds the scaled direction vector to the initial position componentwise.
Claim. Given initial conditions with starting position vector $x_0^μ$ and direction vector $k^μ$, the path is $x^μ(λ) = x_0^μ + λ k^μ$.
background
The NullGeodesics module implements paths satisfying the null condition $g_{μν} dx^μ/dλ dx^ν/dλ = 0$ for lightlike propagation, serving as the foundation for gravitational lensing and time-delay calculations. InitialConditions is the structure holding the starting position $x^μ(0)$ and initial tangent $k^μ = dx^μ/dλ|_{λ=0}$, with the null condition enforced at the geodesic level rather than here. This definition supplies the explicit linear solution in Minkowski coordinates that downstream constructions embed as the path component.
proof idea
The definition is a direct one-line functional expression that applies componentwise addition of the scaled direction to the initial position.
why it matters
This supplies the explicit path for straight null geodesics in Minkowski spacetime, which is invoked by the existence theorem null_geodesic_exists_minkowski and the verification minkowski_straight_line_is_geodesic. It forms the base case for light propagation in the flat-space limit, feeding the broader geodesic machinery that connects to the Recognition framework's treatment of null curves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.