canonicalQuadraticAlongLine_hasSecondDerivAt_zero
plain-language theorem explainer
Along any conformal line through the flat vertex potential, the canonical quadratic piece of the Regge action has second derivative at the origin equal to the quadratic form of the canonical incidence Hessian. Remainder-vanishing and product-rule tangency arguments in the nonlinear Hessian chain cite this identity. The proof is a definitional rewrite plus the general Hessian-along-line second-derivative lemma.
Claim. Let $K$ be an incidence-consistent 3D triangulation and $\xi$ a vertex potential. Write $H$ for the canonical Regge Hessian of $K$ and $Q_H$ for its quadratic form. The real map $t \mapsto \tfrac12 Q_H(t\xi)$ has second derivative at $t=0$ equal to $Q_H(\xi)$.
background
This module isolates the remaining hard step for the full nonlinear Regge action: the second directional derivative of the action at the flat potential must equal the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
The canonical Regge Hessian $H$ is the graph-Laplacian matrix built from incidence dual weights on the triangulation. Its quadratic form $Q_H(\eta)=\sum_{i,j}H_{ij}\eta_i\eta_j$ is the second-order model of the action. The line potential $t\mapsto t\xi$ is the straight conformal ray through the flat configuration in direction $\xi$. The canonical quadratic along that line is defined by $t\mapsto\tfrac12 Q_H(t\xi)$.
HasSecondDerivAt f d2 x means the first derivative of $f$ itself has derivative $d2$ at $x$. The upstream lemma hessianQuadratic_along_line_hasSecondDerivAt_zero already proves the same second-derivative claim for an arbitrary Hessian matrix; the present result specialises it to the canonical incidence Hessian.
proof idea
One-line specialisation. Unfold canonicalQuadraticAlongLine to the explicit map $t\mapsto\tfrac12 Q_H(\mathrm{linePotential}(K,\xi,t))$. After that change of goal, simpa applies the general lemma hessianQuadratic_along_line_hasSecondDerivAt_zero at the matrix canonicalReggeHessian K hK and direction $\xi$. No new calculus is performed here.
why it matters
This is the quadratic half of the nonlinear Hessian endpoint. Downstream, productRuleTangencyToQuadratic_of_productRuleDerivativeCanonicalHessian invokes it directly to obtain first-order tangency of the product-rule expansion to the canonical quadratic. The two remainder-second-variation-zero theorems (with full and near-zero derivative identities) and nonlinearDirectionalHessian_of_remainder_identically_zero sit on the same chain: once the quadratic piece has the right second derivative and the remainder's second variation vanishes, the full nonlinear directional Hessian equals the canonical incidence Hessian.
In the Recognition geometry stack this closes the second-variation input for discrete gravity on incidence-consistent 3D triangulations, the setting in which the eight-tick / $D=3$ forcing (T7–T8) is realised combinatorially. It is not a new physical hypothesis; it is the exact calculus endpoint the module doc announces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.