InitialConditions
plain-language theorem explainer
InitialConditions records the starting position and initial tangent vector for a null geodesic in four-dimensional spacetime. Researchers modeling light propagation or gravitational lensing cite this record when supplying boundary data to geodesic solvers. The declaration is a pure structure definition with two fields of type Fin 4 → ℝ and carries no proof obligations.
Claim. An initial condition for a null geodesic consists of a position map $x^μ(0) : Fin 4 → ℝ$ and a direction map $k^μ = dx^μ/dλ|_{λ=0} : Fin 4 → ℝ$.
background
The module implements null geodesics satisfying the lightlike condition $g_{μν} dx^μ/dλ dx^ν/dλ = 0$. InitialConditions supplies the two pieces of data required to start integration of the geodesic equation: the coordinate position at affine parameter zero and the initial four-velocity components. The structure is used directly by straight_line and straight_null_geodesic to construct explicit solutions in Minkowski space.
proof idea
This is a structure definition that introduces the record type with fields position and direction. No lemmas or tactics are invoked.
why it matters
The structure serves as the input type for null_geodesic_exists_minkowski and geodesic_unique. It therefore anchors the existence and uniqueness results for straight null geodesics in flat spacetime, which in turn support light-propagation calculations in the Recognition framework. The module doc-comment states that these geodesics form the foundation for gravitational lensing deflection angles and time delays.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.