straight_null_geodesic
plain-language theorem explainer
The definition supplies a straight coordinate path in Minkowski spacetime from initial position and null direction vectors. Researchers modeling light propagation or flat-space lensing limits cite it as the explicit base case. The construction assigns the path field directly to the straight_line function and discharges the null and geodesic conditions by simplification.
Claim. Given initial conditions consisting of a position $x^0$ and a null direction $k^μ$ with $η_{μν} k^μ k^ν = 0$, the straight null geodesic is the affine curve $γ(λ) = x(0) + λ k$ in Minkowski spacetime.
background
Null geodesics describe light-like paths satisfying $g_{μν} dx^μ dx^ν = 0$ along the curve. The NullGeodesic structure packages a path function together with a null_condition that contracts the metric on the first derivatives and a geodesic_equation that sets the second covariant derivative to zero. InitialConditions supplies the starting four-vector position and the initial tangent direction.
proof idea
One-line wrapper that sets the path field to straight_line ic. The null_condition is discharged by assuming the direction satisfies the null relation and applying simp on the double sum. The geodesic_equation reduces directly because the Minkowski Christoffel symbols vanish and the second derivative of a linear path is zero.
why it matters
This definition supplies the explicit Minkowski straight-line null geodesic used by null_geodesic_exists_minkowski and minkowski_straight_line_is_geodesic. It fills the flat-space base case for light propagation in the Recognition framework, consistent with the eight-tick octave and D = 3 spatial dimensions. It supports downstream calculations of lensing deflection and time delays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.