differentiableAt_coordRay_i_sq
plain-language theorem explainer
The result establishes differentiability at t=0 of the squared i-th component of the coordinate ray x + t e_μ. Analysts working on relativistic derivatives would cite it when building higher-order differentiability for norms. The proof is a one-line application of the power rule for differentiable functions to the already-established differentiability of the linear component.
Claim. For $x : ℝ^4$ and indices $μ, i$, the map $t ↦ ((x + t e_μ)_i)^2$ is differentiable at $t=0$.
background
The module develops derivative tools for coordinate rays in four-dimensional space, where the standard basis vector $e_μ$ is used to define the ray. The definition of coordRay is the affine shift $x + t · basisVec μ$. The upstream theorem differentiableAt_coordRay_i shows each component is differentiable at the origin by splitting into constant and linear terms via add and mul rules.
proof idea
It is a one-line wrapper that invokes DifferentiableAt.pow on the output of differentiableAt_coordRay_i with exponent 2.
why it matters
It is invoked by differentiableAt_coordRay_spatialNormSq to prove differentiability of the spatial norm squared along the ray. This supports the calculus infrastructure in the relativity module, which connects to the forcing chain steps T5-T8 for deriving spatial dimensions. The doc-comment positions it as supplying the closed form for the partial of $x_i^2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.