coordRay_coordRay
plain-language theorem explainer
The lemma establishes additivity of successive displacements along a fixed coordinate direction in R^4. Analysts constructing directional derivatives via rays in Minkowski space cite it to justify combining parameters without re-deriving the path. The proof is a one-line term that applies function extensionality, unfolds the ray definition, and normalizes the arithmetic.
Claim. Let $x : Fin 4 → ℝ$, $μ : Fin 4$, and $s, t : ℝ$. Then the map obtained by first displacing $x$ along direction $μ$ by parameter $s$ and then along the same direction by $t$ equals the single displacement of $x$ along $μ$ by $s + t$.
background
The module supplies calculus primitives for relativity using the standard basis vectors $e_μ$. The upstream definition of coordRay constructs the ray explicitly as the function $ν ↦ x_ν + t · (basisVec μ ν)$, which adds a multiple of the μ-component while leaving other coordinates unchanged. This supports directional derivatives by restricting functions to these straight-line paths in coordinate space. The module doc identifies the setting as operations built on the standard basis $e_μ$.
proof idea
One-line term proof: apply funext to obtain pointwise equality on the output coordinate ν, simplify using the definition of coordRay, then normalize the resulting linear expression with ring.
why it matters
The identity guarantees that the parametrization of coordinate rays is a group homomorphism from (ℝ, +) into displacements, a prerequisite for consistent first- and second-order derivatives along those rays. It supplies the algebraic foundation used by sibling lemmas such as partialDeriv_v2 and secondDeriv. Within the Recognition framework it remains a low-level calculus fact that does not yet invoke the J-cost or phi-ladder structures appearing in upstream mass derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.