canonicalQuadraticAlongLine_hasDerivAt
plain-language theorem explainer
Along the ray t·ξ in vertex-potential space, the canonical quadratic piece of the Regge action is differentiable, with derivative t times the Hessian quadratic form of ξ. Anyone proving the nonlinear directional Hessian equals the incidence Hessian cites this. The proof rewrites the line restriction as a pure multiple of t² and differentiates by the power rule.
Claim. Let $K$ be an incidence-consistent 3D triangulation and $\xi$ a vertex potential on $K$. Write $Q(t)$ for the canonical quadratic contribution to the Regge action along the ray $t\mapsto t\xi$. Then $Q$ is differentiable at every $t\in\mathbb{R}$, and $Q'(t)=t\,H(\xi)$, where $H$ is the quadratic form of the canonical Regge Hessian of $K$.
background
This module isolates the remaining hard step for the full nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. The module doc states that once that chain-rule calculation is supplied, the existing second-variation input package follows immediately.
The objects here are discrete. A triangulation $K$ carries an incidence structure; incidence consistency is the hypothesis that makes the canonical Regge Hessian well-defined. Vertex potentials are real assignments to vertices. The canonical Regge Hessian is the bilinear form built from that incidence data (imported from the concrete Regge-action layer). Its associated quadratic form $H(\xi)$ is the pure second-order piece of the action.
The sibling canonicalQuadraticAlongLine restricts that quadratic piece to the straight ray $t\xi$. The present theorem is the first-derivative fact for that restriction; the companion remainder along the same ray is handled separately in the split of the full action along the line.
proof idea
First identify the line restriction with an elementary quadratic: by unfolding canonicalQuadraticAlongLine and rewriting with hessianQuadratic_linePotential, one obtains
$Q(t)=(H(\xi)/2),t^2$
pointwise (the algebra is closed by ring). After rewriting the goal with that identity, differentiate $(c,t^2)$ via the power rule on the identity map: (hasDerivAt_id t).pow 2 scaled by the constant $H(\xi)/2. A final simpa with the usual multiplication identities (two_mul, mul_comm, mul_left_comm, mul_assoc`) rearranges $2c,t$ into $t,H(\xi)$.
why it matters
This is a small but necessary calculus step inside the nonlinear Regge Hessian program. Downstream, deriv_canonicalQuadraticAlongLine is the one-line extraction of the derivative value from the HasDerivAt witness, so every later argument that needs $Q'(t)=t,H(\xi)$ as an equality of reals routes through here.
In the broader Recognition geometry stack, matching the second directional derivative of the nonlinear action to the canonical incidence Hessian is the exact endpoint named by the module: it closes the second chain-rule calculation that turns the abstract second-variation interface into a proved statement. Without differentiability of the pure quadratic piece along rays, the directional Hessian comparison cannot even be stated in derivative form.
The result does not itself finish the nonlinear theorem; it only clears the quadratic summand. The remainder and the full action-along-line split still have to be fed into the directional-Hessian assembly lemmas sitting as siblings in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.