reggeActionSecondVariationInput_of_nonlinearDirectionalHessian
plain-language theorem explainer
Packages a full nonlinear directional-Hessian hypothesis at a flat 3D triangulation into the second-variation input bundle used by the Regge action interface. Cite it when the hard chain-rule calculation is already in hand and only the packaging step remains. The body is a one-line composition of two existing constructors.
Claim. Let $K$ be an incidence-consistent 3D triangulation with a flat configuration. Suppose that for every vertex potential $\xi$, the map $t \mapsto S(K,\,q_0 + t\xi)$ (Regge action along the line) has second derivative at $t=0$ equal to the quadratic form of the canonical incidence Hessian on $\xi$. Then the standard second-variation input structure for $(K,\text{flat})$ is inhabited.
background
This module isolates the remaining hard step for the full nonlinear Regge action: at a flat potential, the second directional derivative must match the canonical incidence Hessian. The module doc states that this is not a new assumption but the exact endpoint of the second chain-rule calculation; once supplied, the existing second-variation input follows immediately.
NonlinearReggeDirectionalHessianTheorem is the Prop that for every vertex potential $\xi$, actionAlongLine has second derivative at $0$ equal to hessianQuadratic of canonicalReggeHessian on $\xi$. A flat configuration is the background edge-length (or deficit) data at which linearization is taken. The target type ReggeActionSecondVariationInput is the packaged hypothesis bundle consumed by the second-variation theory in the imported ReggeActionSecondVariation module.
Sibling lemmas split the work into a directional second-variation form and a bridge from the nonlinear theorem to that form (canonicalHessianSecondVariation_of_nonlinearDirectionalHessian).
proof idea
Pure packaging definition, not a calculation. It applies reggeActionSecondVariationInput_of_directionalSecondVariation to the flat data, feeding it the directional second-variation witness produced by canonicalHessianSecondVariation_of_nonlinearDirectionalHessian from the nonlinear Hessian hypothesis. No new analytic work occurs here; the composition just aligns the nonlinear theorem's shape with the input structure expected downstream.
why it matters
In the Recognition geometry stack this is the glue between the hard nonlinear Regge calculation and the reusable second-variation interface. The module frames the nonlinear directional Hessian as the exact endpoint of the chain-rule expansion (local geometric product rule, Cayley-Menger/arccos and hinge derivatives, Schläfli cancellation) near the flat point. Once that endpoint is proved, this definition discharges ReggeActionSecondVariationInput with no further hypotheses.
No downstream consumers are wired yet (used_by is empty), so its role is infrastructural: it keeps the nonlinear proof obligation cleanly separated from the second-variation API. It does not itself touch the forcing chain (T0-T8), RCL, or the $\varphi$-ladder; it sits in discrete gravity geometry that those constants later calibrate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.