coordRay_zero
plain-language theorem explainer
The lemma states that the coordinate ray x + t e_μ returns exactly to the base point x when the parameter t vanishes. Workers on directional derivatives and radial functions in Minkowski space cite it to reduce evaluations at the ray origin. The proof is a one-line term-mode application of function extensionality followed by unfolding the ray definition.
Claim. For any point $x : ℝ^4$ and coordinate index $μ$, the ray $γ(t) = x + t e_μ$ satisfies $γ(0) = x$.
background
The module supplies calculus tools for directional derivatives along coordinate rays in 4D Minkowski space. The ray is introduced as the map sending parameter t to the vector whose ν-component is x_ν plus t times the μ-component of the standard basis vector. This supplies the local parametrization used throughout the subsequent differentiability statements for radialInv and spatialRadius.
proof idea
One-line term proof: apply funext to obtain an equality of functions, then simplify using the explicit definition of the ray.
why it matters
The fact is invoked by twelve downstream results that establish differentiability of radialInv, spatialRadius, and their partial derivatives along rays. It supplies the base case needed to evaluate those functions at the origin of each coordinate ray before applying the quotient and chain rules in partialDeriv_v2_radialInv and related statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.