coordRay
plain-language theorem explainer
The coordinate ray through point x along index μ is the affine line x + t e_μ in R^4. Researchers setting up directional derivatives in relativistic calculus cite this when parameterizing paths along the standard axes. The definition is a direct componentwise construction that adds the scaled basis vector to x.
Claim. The map sending t to the point x + t e_μ is given by (coordRay(x, μ, t))(ν) = x(ν) + t · e_μ(ν), where e_μ is the standard basis vector in R^4 that equals 1 at index μ and 0 elsewhere.
background
The module introduces the standard basis vector e_μ as the function that returns 1 at position μ and 0 at all other indices in Fin 4. The coordinate ray is built directly on this vector to produce an affine line in coordinate space. Upstream result basisVec supplies the explicit form: def basisVec (μ : Fin 4) : Fin 4 → ℝ := fun ν => if ν = μ then 1 else 0, quoted as the standard basis vector e_μ.
proof idea
This is a direct definition that constructs the ray by scaling basisVec μ by t and adding the result componentwise to the input vector x.
why it matters
The definition supplies the parameterization used by downstream lemmas such as coordRay_apply, coordRay_coordRay, deriv_add_lin, and deriv_coordRay_i that establish linearity and derivative properties along coordinate directions. It fills the basic geometric step needed for directional derivatives in the relativity calculus layer, supporting later calculations that connect to the Recognition Science forcing chain and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.