deriv_coordRay_i
plain-language theorem explainer
The i-th component of the coordinate ray from point x in four-dimensional space has derivative exactly 1 at parameter value zero. Workers setting up tangent vectors to coordinate lines or partial derivatives in Minkowski space cite this normalization result. The proof reduces the ray expression via its definition and the basis self-property then applies the derivative rules for a constant-plus-identity function.
Claim. For a vector $x$ in four-dimensional real space and index $i$, the derivative at $t=0$ of the $i$-th component of the line $x + t e_i$ equals 1, where $e_i$ is the standard basis vector with value 1 in position $i$.
background
The Derivatives module defines the coordinate ray as the affine line $x + t e_μ$ in $ℝ^4$, where $e_μ$ is the standard basis vector. The self-evaluation property states that the μ-component of $e_μ$ equals 1. This lemma belongs to the relativity calculus layer that imports tensor geometry and constructs differentiation operators atop the arithmetic foundations from ArithmeticFromLogic.
proof idea
A two-step tactic proof. simp first unfolds the ray application lemma, the basis self-value, and the multiplication identity to obtain a constant plus the identity function. rw then replaces the expression with the known derivative of a constant added to the identity map.
why it matters
This result supplies the unit normalization along each coordinate axis, a prerequisite for the partial derivative and Laplacian operators defined later in the same module. It anchors the calculus constructions that feed into spacetime geometry before the forcing chain or mass ladder is applied. No downstream uses are recorded yet; the lemma closes a basic gap in the derivative toolkit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.