nonlinearDirectionalHessian_of_actionDerivativeLinearizationNearZero
plain-language theorem explainer
If the first derivative of the nonlinear Regge action along every conformal line equals the canonical Hessian ray near the flat point, then the second directional derivative at zero is exactly that Hessian quadratic. Discrete-gravity and Regge-calculus workers cite it to close the nonlinear Hessian step. The proof is a short congruence: the model linear map has the right derivative at zero, and the linearization hypothesis transfers it.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Suppose that for every vertex potential $\xi$, the map $t \mapsto \partial_t S(K, t\xi)$ agrees in a neighborhood of $t=0$ with $t \mapsto t\, Q_K(\xi)$, where $Q_K$ is the quadratic form of the canonical incidence Hessian. Then for every $\xi$, the second derivative of $t \mapsto S(K, t\xi)$ at $t=0$ equals $Q_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 match the canonical incidence Hessian. The endpoint is not a new axiom; it is what the second chain-rule calculation must deliver so that ReggeActionSecondVariationInput follows at once.
The hypothesis is the exact first-derivative linearization left after the local geometric product rule, Cayley–Menger/arccos derivative, hinge derivative, and Schläfli cancellation near the flat point. It is stronger than a bare derivative-at-zero claim: the first derivative of the action along the line must be eventually equal (in the neighborhood filter at 0) to the ray $t \mapsto t,Q_K(\xi)$.
The target is the sharp second-variation statement: HasSecondDerivAt means the first derivative map itself has derivative $Q_K(\xi)$ at 0. The canonical Hessian is the graph-Laplacian matrix built from incidence dual weights on the triangulation.
proof idea
Fix a vertex potential $\xi$. Unfold the second-derivative predicate to a first-derivative claim on $t \mapsto \partial_t S$. Build the model map $t \mapsto t,Q_K(\xi)$; its derivative at 0 is $Q_K(\xi)$ by the product rule on the identity (via hasDerivAt_id and mul_const). The linearization hypothesis supplies eventual equality of the true first-derivative map with that model near 0, so congr_of_eventuallyEq transfers the derivative and finishes.
why it matters
This is the bridge from the expanded first-derivative linearization to the exact nonlinear directional Hessian. Downstream it feeds canonicalRemainderSecondVariationZero_of_actionDerivativeLinearizationNearZero_and_flat (remainder second variation vanishes on flat configurations once linearization holds) and the constructor reggeActionSecondVariationInput_of_flat_actionDerivativeLinearization, which packages the second-variation input used by the broader Regge second-variation API.
In the Recognition geometry stack this closes the nonlinear half of the discrete Einstein–Hilbert second variation on 3D triangulations: once the geometric expansions near flatness yield the linearization target, the Hessian identity is automatic rather than an extra postulate. It sits under the discrete-geometry side of the framework (Regge action, incidence Hessian), not the T0–T8 forcing chain itself, but it is the calculation that makes the nonlinear action match the canonical quadratic form used in curvature and stability arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.