basisVec_self
plain-language theorem explainer
basisVec_self establishes that the diagonal component of the standard basis vector e_μ equals 1 for each index μ in four-dimensional spacetime. Researchers deriving coordinate derivatives or partials of quadratic forms cite it to simplify index evaluations. The proof is a direct one-line simplification using the definition of basisVec.
Claim. For each index $μ ∈ Fin 4$, the standard basis vector $e_μ : Fin 4 → ℝ$ defined by $e_μ(ν) = 1$ if $ν=μ$ and $0$ otherwise satisfies $e_μ(μ) = 1$.
background
The module develops differentiation tools for spacetime coordinates using standard basis vectors in four dimensions. The upstream definition states that basisVec μ is the function returning 1 precisely at input index μ and 0 elsewhere. This supplies the local evaluation rule needed for coordinate-ray derivatives and partial derivatives of squared coordinates.
proof idea
One-line wrapper that applies simp with the definition of basisVec, which substitutes the matching index to yield 1 immediately.
why it matters
This lemma feeds deriv_coordRay_i (showing the derivative of the i-th coordinate along the ray at 0 equals 1) and partialDeriv_v2_x_sq (closed form for ∂μ of x_i squared). It supplies the basic index-evaluation rule in the relativity calculus layer, supporting derivative computations in the Recognition Science framework without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.