differentiableAt_coordRay_i
plain-language theorem explainer
Coordinate rays in four-dimensional space have components that are differentiable at the parameter origin. Analysts deriving partial derivatives of quadratic forms or radial expressions along basis directions cite this to justify local smoothness in flat-space calculations. The argument reduces the claim to elementary facts about sums and products of differentiable functions after unfolding the ray definition.
Claim. Let $r(t) = x + t e_μ$ for $x ∈ ℝ⁴$ and standard basis vector $e_μ$. The map $t ↦ r(t)_i$ is differentiable at $t = 0$.
background
The Derivatives module develops differentiation along coordinate rays in four-dimensional space, where the standard basis vectors $e_μ$ supply the coordinate directions. A coordinate ray parametrizes the affine line obtained by displacing a point $x$ by parameter distance $t$ along direction $μ$. The local setting assumes the standard differentiable structure on ℝ⁴ and builds tensor calculus primitives from it.
proof idea
The proof simplifies the ray definition via the apply rule for the component map, then invokes the sum rule for differentiability. It chains the constant-function case with the product rule, using the known differentiability of the identity and constant functions at zero.
why it matters
This result is invoked directly by the squared-component differentiability theorem and the closed-form partial derivative for the square of a coordinate. Those in turn support radial derivative calculations elsewhere in the module. It supplies the basic smoothness fact required for coordinate-based computations consistent with the framework's derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.