affine_reparametrization
plain-language theorem explainer
Affine reparametrization of a null geodesic yields another null geodesic under linear change of the affine parameter. Workers in gravitational lensing and light propagation in curved spacetime cite this when rescaling the parameter along photon paths. The proof proceeds by explicit construction of the reparametrized path structure and direct substitution into the null condition and geodesic equation.
Claim. Let $g$ be a metric tensor and let $x$ be a null geodesic for $g$. For real numbers $a,b$ with $a$ nonzero, define the reparametrization map by $s(t)=a t + b$. Then there exists a null geodesic $y$ such that $y(t)=x(s(t))$ for every real $t$.
background
A null geodesic consists of a path function from the reals into four-dimensional coordinates together with two properties: the null condition that the metric contraction of the two tangent vectors vanishes identically, and the geodesic equation that the second derivative plus the connection term vanishes. The module implements this structure to support calculations of light propagation, gravitational lensing deflection angles, and time delays. Upstream MetricTensor supplies the local bilinear form that appears inside the null-condition sum.
proof idea
The tactic proof opens with classical, introduces the linear map, then builds a fresh NullGeodesic record whose path is the original path composed with the map. It discharges the null-condition goal by simpa substitution of the original null condition evaluated at the shifted argument. The geodesic-equation goal is discharged identically by the same substitution. The final universal quantification over the parameter is closed by reflexivity.
why it matters
The result guarantees invariance of the null-geodesic property under affine reparametrizations, a prerequisite for consistent treatment of the affine parameter along light rays. It supplies a basic invariance lemma inside the null-geodesics module whose module documentation identifies it as foundation for lensing and time-delay computations. No downstream uses appear in the current dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.