ConcreteReggeSecondOrderData
plain-language theorem explainer
Packages second-order Regge data for an incidence-consistent finite 3D triangulation: a quadratic action functional, a symmetric Hessian on vertices, and the exact second-variation identity tying them together. Cited by anyone discharging the genuine Hessian target or converting into the shared ReggeHessianData interface. Pure structure definition; the identities are fields, not theorems proved here.
Claim. For an incidence-consistent finite 3D triangulation $K$, a concrete second-order Regge data package consists of a map $S^{(2)}$ from conformal vertex potentials to $\mathbb{R}$ and a symmetric matrix $H$ on the vertices such that $S^{(2)}$ equals the quadratic truncation built from $H$, and $S^{(2)}(\xi)-S^{(2)}(0)=\frac12\,\xi^{\top} H\xi$ holds for every vertex potential $\xi$.
background
This module isolates the final analytic Hessian step for a finite 3D Regge triangulation under the conformal ansatz. Vertex potentials are real assignments to the triangulation vertices; the zero potential is the flat base point. The Hessian quadratic form is the double sum $\sum_{i,j} H_{ij}\xi_i\xi_j$.
The second-order action is the quadratic truncation $S^{(2)}(\xi)=S(0)+\frac12,\xi^{\top} H\xi$, not the full nonlinear Regge action. As the upstream doc states, this is "the object for which exact quadratic second-variation statements are definitionally correct; the full nonlinear action needs a Taylor remainder theorem."
Incidence consistency of $K$ is the standing hypothesis that makes dihedral angles, deficit angles, and hinge measures well-defined on the triangulation.
proof idea
No proof body: this is a structure declaration. The five fields are the data and the two required identities (Hessian symmetry, and equality of the packaged action with the quadratic truncation, which immediately yields the second-variation formula). Inhabitants are built elsewhere by supplying a concrete symmetric Hessian and unfolding the definition of the second-order action.
why it matters
This structure is the concrete carrier that the module's Hessian closure story is about. Downstream, the canonical constructor fills it from the incidence Hessian; the conversion map turns any such package into the shared ReggeHessianData interface (with the second-order action, not the full nonlinear action); and GenuineReggeHessianTarget is exactly the proposition that every incidence-consistent triangulation admits a nonempty instance of this structure.
In the Recognition geometry stack this is the analytic hinge between discrete Regge calculus on a 3D complex and the Hessian data expected by later curvature and forcing arguments. It deliberately stops at second order, matching the module goal of isolating the Hessian step rather than claiming a full Taylor theorem for the nonlinear action.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.