hasDerivAt_linePotential
plain-language theorem explainer
Along any real ray through a vertex potential ξ on a 3D triangulation, the line map s ↦ s·ξ is differentiable with derivative exactly ξ at every parameter. First-variation and cubic-remainder arguments that restrict the Regge action to lines cite this fact. The proof rewrites the line as scalar multiplication and applies the constant-smul rule to the identity map.
Claim. For every 3D triangulation $K$, every vertex potential $\xi$ on $K$, and every real $t$, the map $s \mapsto$ (line potential of $\xi$ at $s$) has derivative $\xi$ at $t$. Equivalently, $s \mapsto s\cdot\xi$ is differentiable at $t$ with derivative $\xi$.
background
The module isolates the analytic cubic Taylor bound for the nonlinear Regge remainder once the Hessian is known. Work takes place in the finite-dimensional space of vertex potentials on a fixed 3D triangulation $K$.
The line potential through a direction $\xi$ is the ray $s \mapsto s\cdot\xi$ in vertex-potential space (pointwise $i \mapsto s,\xi(i)$). An upstream identity records that this coincides with scalar multiplication: line potential equals $t\cdot\xi$ at every $t$. Differentiability is the ordinary real-variable HasDerivAt notion on that ray.
No flatness, incidence, or curvature hypotheses enter; the statement is pure linear algebra of the potential space.
proof idea
Rewrite the line map via the identity that line potential equals scalar multiplication by $s$, using function extensionality. The resulting map $s \mapsto s\cdot\xi$ is the identity on $\mathbb{R}$ scaled by the constant vector $\xi$. Apply the library rule that the identity has derivative $1$ and constant-smul preserves derivatives, then simplify.
why it matters
This private lemma is the differentiability step for the line-restricted canonical remainder. Downstream, canonicalRemainderLine_hasDerivAt_zero_of_remainderFirstVar uses it to conclude that the remainder along the ray has derivative zero at the origin whenever the free-space first variation vanishes at zero. That vanishing is an input to the cubic Taylor bound for the nonlinear Regge remainder after the Hessian identification, the module's stated goal. In the broader Recognition geometry stack it is bookkeeping on the potential space, not a forcing-chain landmark, but it closes the first-order jet data needed before the third-order remainder estimate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.