coordRay_apply
plain-language theorem explainer
The lemma gives the explicit component form of the affine ray x + t e_μ in R^4: its νth coordinate equals x_ν plus t times the Kronecker delta δ_μν. Derivative lemmas throughout the relativity calculus module invoke it to evaluate ray components before applying chain-rule steps. The proof reduces immediately to reflexivity once the definitions of the ray and the basis vector are unfolded.
Claim. The ν-component of the coordinate ray satisfies $(x + t e_μ)_ν = x_ν + t δ_{μν}$, where $e_μ$ denotes the standard basis vector in $ℝ^4$ that equals 1 at index μ and 0 elsewhere.
background
The module defines the standard basis vector e_μ as the function on Fin 4 that returns 1 precisely when the index equals μ. The coordinate ray is the affine line obtained by adding the scalar multiple t e_μ to a starting point x in R^4. These objects supply the concrete parametrization used for directional derivatives in the relativity calculus layer.
proof idea
The proof is a one-line wrapper that applies reflexivity directly to the definition of coordRay, which substitutes the expression built from basisVec.
why it matters
The lemma supplies the unfolding step required by the seven downstream derivative results in the same module, including deriv_coordRay_i, partialDeriv_v2_x_sq, and secondDeriv_radialInv. It therefore supports the explicit partial-derivative formulas needed for radial functions in the relativity calculus. No direct connection to the T0-T8 forcing chain appears here; the result remains internal to the Minkowski-space derivative layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.