deriv_coordRay_j
plain-language theorem explainer
The declaration shows that the j-component of a coordinate ray along direction i has vanishing derivative at the base point whenever the indices differ. Researchers computing partial derivatives or Laplacians in four-dimensional spacetime models would cite it to drop cross terms. The term-mode proof reduces the ray expression to a constant via basis orthogonality and arithmetic identities, then applies the constant-function derivative rule.
Claim. For any point $x$ in four-dimensional Euclidean space and distinct indices $i,j$, the derivative at parameter value zero of the $j$-th component of the straight-line ray from $x$ in the $i$-th coordinate direction equals zero.
background
The module develops coordinate calculus for relativity using the standard basis vectors $e_μ$ in four dimensions. A coordinate ray from base point $x$ along index $i$ is the parametrized line $x + t e_i$. The $j$-component of this ray is therefore constant when $j ≠ i$. Upstream arithmetic lemmas establish that addition by zero and multiplication by zero leave expressions unchanged, allowing reduction to a constant function whose derivative vanishes identically.
proof idea
The term proof first rewrites the ray component using its explicit definition and the off-diagonal vanishing property of basis vectors. It then applies the arithmetic identities for addition and multiplication by zero to obtain the constant function whose value is the $j$-th coordinate of $x$. The final step invokes the rule that the derivative of any constant function is zero.
why it matters
The result supplies an elementary building block for derivative calculations inside the relativity calculus module, supporting later constructions such as the functional derivative of the squared spatial norm. It fits the Recognition Science pattern of working in four-dimensional coordinate space (one time plus three spatial dimensions) and relies on the same arithmetic foundations that appear throughout the forcing chain. No downstream theorems are yet recorded, leaving its precise placement in larger derivative identities open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.