NonlinearReggeDirectionalHessianTheorem
plain-language theorem explainer
Exact second-directional-variation claim for the full nonlinear Regge action on an incidence-consistent 3D triangulation: along every vertex-potential ray, the second derivative of the action at the flat point equals the canonical incidence-Hessian quadratic form. Cubic-Taylor and remainder-second-variation constructors cite this proposition as the hard endpoint of the chain-rule calculation. It is packaged as a Prop definition, not a proved theorem; discharging it is the remaining analytic step in the module.
Claim. For every incidence-consistent 3D triangulation $K$ and every vertex potential $\xi$, the scalar map $t \mapsto S_K(t\xi)$ (nonlinear Regge action along the line through the flat configuration in direction $\xi$) has second derivative at $t=0$ equal to the quadratic form of the canonical incidence Hessian of $K$ evaluated on $\xi$.
background
The module isolates the remaining hard calculation for the full nonlinear Regge action on a 3D triangulation: the second directional derivative of the action at the flat potential must match the canonical incidence Hessian. The local setting is discrete gravity in the Regge calculus, with edge lengths (or vertex potentials) as configuration variables and deficit angles supplying curvature.
The canonical Hessian is the graph-Laplacian matrix induced by incidence dual weights on the triangulation: diagonal entries sum the dual weights out of a vertex, off-diagonal entries are minus the dual weight between the pair. The action along a line is the restriction of the nonlinear Regge action to the one-parameter family through the flat configuration in a fixed vertex-potential direction. Second-derivative-at-a-point is the standard real-analysis predicate that the first derivative exists nearby and is itself differentiable at the base point with the stated value.
Upstream, the concrete Hessian construction and the second-variation infrastructure (action along a line, second-derivative predicate) are already in place. The module doc states that this proposition is not a new physical assumption; it is the exact endpoint of the second chain-rule expansion (geometric product rule, Cayley-Menger/arccos derivatives, hinge derivatives, and Schlaefli cancellation) near the flat point.
proof idea
No proof body: the declaration is a definition of a proposition. It packages the universal claim that every vertex potential yields a second derivative of the action-along-line at zero equal to the canonical Hessian quadratic form. Downstream lemmas treat an inhabitant of this Prop as a hypothesis and rewrite it into second-variation inputs, remainder vanishings, and cubic-Taylor packages by one-line coercion or composition with differentiability side conditions.
why it matters
This is the named hard endpoint of the nonlinear Regge second-variation chain. Once inhabited, the existing second-variation input for the Regge action follows immediately, and the cubic remainder is controlled by $O(|\xi|^3)$.
Downstream constructors use it heavily: remainder second-variation input from flat configuration plus this claim; canonical remainder line quadratic Taylor zero from flat first variation and this claim; cubic remainder input and local Hessian-Taylor input bundles from this claim plus the cubic Taylor theorem; and several same-module rewrites that turn the directional Hessian into canonical Hessian second variation at zero or into vanishing of the canonical remainder second variation (given action-line differentiability).
In the broader Recognition geometry stack this pins the discrete Einstein-Hilbert second variation to the incidence Laplacian on 3D triangulations, consistent with the forcing of $D=3$ and the eight-tick octave. The open work is the analytic discharge of the chain-rule expansion that the module doc identifies as still outstanding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.