nonlinearDirectionalHessian_of_actionDerivativeFirstOrderTangency
plain-language theorem explainer
If the first derivative of the nonlinear Regge action along every conformal line is first-order tangent at zero to the canonical Hessian response, then the second directional derivative at the flat potential equals the incidence Hessian quadratic form. Discrete-gravity and Regge-calculus workers cite this to discharge the exact second-variation endpoint. The proof adds the linear Hessian derivative to the tangency hypothesis and rewrites by ring.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Suppose that for every vertex potential $\xi$, the map $t \mapsto \partial_t S(t\xi) - t\, Q_H(\xi)$ has derivative $0$ at $t=0$, where $S$ is the nonlinear Regge action along the conformal line and $Q_H$ is the quadratic form of the canonical incidence Hessian. Then for every $\xi$, $S$ has second derivative $Q_H(\xi)$ at $t=0$.
background
This module isolates the hard endpoint of the nonlinear Regge second-variation calculation: at the flat potential, the second directional derivative of the full action must match the canonical incidence Hessian. The action along a conformal line, actionAlongLine, restricts the nonlinear Regge action to the one-parameter family of vertex potentials $t\mapsto$ flat $+ t\xi$.
The canonical Regge Hessian is the graph-Laplacian matrix built from incidence dual weights: diagonal row-sums of dual weights minus the off-diagonal dual weight. Its quadratic form $Q_H(\xi)$ is the candidate second variation. The target hypothesis (first-order tangency) asserts that $\partial_t S(t\xi) - t, Q_H(\xi)$ has derivative zero at $t=0$; unlike a full linearization-near-zero target, it still permits cubic and higher Regge remainders.
The conclusion is the exact second-directional-variation statement: $S(\cdot,\xi)$ has second derivative $Q_H(\xi)$ at zero. Once that holds, the existing second-variation input package for flat configurations follows immediately.
proof idea
Fix a direction $\xi$. Unfold the second-derivative-at predicate. Let $q = Q_H(\xi)$. The map $t\mapsto t, q$ has derivative $q$ at $0$ by the product rule on the identity (Mathlib hasDerivAt_id.mul_const). Add this derivative fact to the tangency hypothesis applied at $\xi$: the sum of $\partial_t S - t, q$ and $t, q$ has derivative $0+q$ at zero. Convert the sum back to $\partial_t S$ by a pointwise ring identity $(\partial_t S - t q) + t q = \partial_t S$, and finish the value identity by ring. No geometric expansion is performed here; the lemma is pure first-order calculus bookkeeping.
why it matters
In the Recognition geometry stack this is the bridge from the sharp first-order tangency interface to the exact nonlinear directional Hessian theorem. Downstream it feeds three closures: the upgrade from quadratic tangency to the full Hessian theorem; the vanishing of the canonical remainder's second variation under flatness plus tangency; and the constructor that packages flatness with tangency into ReggeActionSecondVariationInput.
That input is the module's stated endpoint: once the second chain-rule calculation supplies tangency, the second-variation package for the nonlinear Regge action is immediate. The result sits in the discrete-gravity layer that underwrites continuum limits and curvature matching in the broader RS geometry program (spatial dimension $D=3$ from the forcing chain, eight-tick discrete time). It does not itself expand Cayley-Menger or Schläfli identities; those live in the calculation that discharges the tangency hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.