basisVec_ne
plain-language theorem explainer
The lemma states that the standard basis vector e_μ in four-dimensional space evaluates to zero at any index ν distinct from μ. Researchers computing coordinate derivatives or partials along rays in relativity would cite it to drop cross terms. The proof is a one-line simplification that unfolds the definition of the basis vector and applies the inequality hypothesis.
Claim. Let $e_μ$ denote the standard basis vector in $ℝ^4$ with components indexed by $μ,ν ∈ {0,1,2,3}$. Then $e_μ(ν) = 0$ whenever $ν ≠ μ$.
background
The module introduces the standard basis vector $e_μ$ as the function that equals 1 at index $μ$ and 0 elsewhere. This supplies the discrete Kronecker structure needed for coordinate calculus in four-dimensional spacetime. The lemma depends directly on that definition, which encodes the indicator behavior for each fixed $μ$.
proof idea
The term proof applies simp with the basis vector definition and the hypothesis $ν ≠ μ$. This triggers the if-then-else case split inside the definition, yielding zero immediately.
why it matters
The result feeds the derivative lemmas deriv_coordRay_j and partialDeriv_v2_x_sq, which simplify expressions for derivatives of coordinate-ray functions and squared components. It supplies the basic off-diagonal vanishing step required for index manipulations in the relativity calculus module. Within the Recognition framework it supports the four-dimensional index structure (Fin 4) used in derivative operations consistent with D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.