deriv_canonicalQuadraticAlongLine
plain-language theorem explainer
Along the ray through a vertex potential ξ on an incidence-consistent 3D triangulation, the derivative of the canonical quadratic Regge form equals t times the Hessian quadratic form of ξ. Cited when reducing first-order tangency of the nonlinear action to pure quadratic calculus. Proof is a one-line extraction of the derivative field from the matching HasDerivAt lemma.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation, $\xi$ a vertex potential on $K$, and $t\in\mathbb{R}$. Write $Q_K$ for the canonical quadratic form along the line through $\xi$, and $H_K$ for the quadratic form of the canonical Regge Hessian. Then $\frac{d}{dt} Q_K(t) = t\, H_K(\xi)$.
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 object differentiated here is the canonical quadratic piece of the action restricted to the real line $t\mapsto t\xi$ through a fixed vertex potential. Its second-variation partner is the canonical Regge Hessian built from the incidence data of $K$ (the concrete Hessian of the linearized Regge action). The scalar hessianQuadratic turns that bilinear form into the associated quadratic form on $\xi$.
The identity is the elementary calculus fact that if the quadratic along the line is proportional to $t^2$ times a fixed form on $\xi$, its first derivative is linear in $t$. It sits upstream of the first-order tangency targets that compare the true action derivative to this quadratic model.
proof idea
One-line term proof. The sibling lemma canonicalQuadraticAlongLine_hasDerivAt already supplies a HasDerivAt witness for the canonical quadratic along the line at the point $t$, with derivative value $t$ times the Hessian quadratic form on $\xi$. Projecting that witness with the .deriv field yields the bare deriv equality.
why it matters
Feeds directly into actionDerivativeFirstOrderTangency_of_quadraticTangency, which upgrades a tangency-to-quadratic hypothesis into the first-order action-derivative tangency target used by the nonlinear directional Hessian theorems in this module.
In the Recognition geometry stack this is bookkeeping on the quadratic model of the Regge action, not a new physical assumption. It clears the derivative side of the split actionAlongLine = quadratic + remainder, so later lemmas can isolate the remainder's first-order vanishing and conclude that the nonlinear second directional derivative at the flat potential recovers the canonical incidence Hessian. That is the exact endpoint named in the module doc for discharging ReggeActionSecondVariationInput.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.