reggeHessianData_of_secondOrder
plain-language theorem explainer
Packages concrete second-order Regge data on a finite 3D triangulation into the shared Hessian interface. Anyone proving existence of a genuine Regge Hessian cites this conversion. The construction is a field-by-field structure fill: second-order action, Hessian matrix, symmetry, and second-variation identity, with the flat first-variation flag set to true.
Claim. Given an incidence-consistent triangulation $K$ in 3D and a concrete second-order data package $D$ (second-order action, symmetric Hessian matrix, and quadratic second-variation identity), form a Regge Hessian data package whose action is $D$'s second-order action, whose Hessian and symmetry come from $D$, whose flat first-variation flag is true, and whose second-variation identity is that of $D$.
background
The module isolates the final analytic Hessian step for a finite 3D Regge triangulation. Under a conformal ansatz on vertex potentials, one builds a concrete action package and proves its second variation; this definition turns that package into the existing shared Hessian interface.
ConcreteReggeSecondOrderData holds a second-order action (equal to the canonical second-order Regge action built from an incidence Hessian), a symmetric bilinear Hessian on vertices, and the exact quadratic identity: the second-order action relative to the zero potential equals half the Hessian quadratic form. The exact identity is intentionally about the second-order action, not the full nonlinear Regge action.
ReggeHessianData is the shared interface expected downstream: an action functional, a Hessian, symmetry, a flat first-variation flag, and a second-variation statement. Spatial dimension $D=3$ is the forced setting (T8) in which the triangulation lives.
proof idea
Pure structure construction, not a proof. Map fields of the concrete package into ReggeHessianData: action becomes the second-order action; Hessian and Hessian symmetry are copied; second variation is copied; the flat first-variation field is filled with the proposition True. No lemmas are applied.
why it matters
This is the adapter that lets a concrete second-order construction discharge the existing Hessian interface. Downstream, genuine_regge_hessian_of_concrete uses it: given a target that supplies nonempty concrete second-order data for every incidence-consistent triangulation, it returns nonempty ReggeHessianData by applying this conversion.
In the Recognition geometry stack this closes the last packaging step between explicit conformal second-order analysis (deficits, dihedral derivatives, incidence Hessian) and the abstract Hessian interface used for genuine Regge Hessian existence. It sits in the $D=3$ forced spatial setting (T8) of the forcing chain. It does not itself prove positivity, continuum limits, or full nonlinear first-variation vanishing; it only packages what the concrete data already proved at second order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.