basisVec
plain-language theorem explainer
The definition supplies the standard basis vector e_μ in four-dimensional spacetime, equal to 1 at index μ and 0 elsewhere. Workers deriving coordinate rays or partial derivatives in relativistic calculus cite this construction when building delta-function identities. It is supplied as a direct functional definition using a conditional expression on Fin 4 indices.
Claim. The standard basis vector $e_μ : ℝ^4 → ℝ$ is given by $e_μ(ν) = 1$ if $ν = μ$ and $0$ otherwise.
background
In the relativity calculus module, spacetime points are maps from Fin 4 to ℝ, with index 0 reserved for the temporal coordinate. The standard basis vector supplies the unit direction along each axis and is imported from the tensor geometry layer. It is used to form coordinate rays of the form x + t e_μ and to isolate components in derivative operators.
proof idea
The definition is introduced directly as a lambda expression that returns 1 precisely when the input index equals μ.
why it matters
This definition anchors the coordinate-ray and derivative lemmas that follow, including coordRay, basisVec_self, and partialDeriv_v2_spatialNormSq. It supplies the discrete Kronecker structure required for chain-rule reductions in four-dimensional spacetime. Within the Recognition framework it marks the passage from tensor geometry to explicit calculus in the relativity domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.