canonicalReggeSecondOrderData
plain-language theorem explainer
Packages the incidence graph-Laplacian Hessian of a finite 3D triangulation into the concrete second-order Regge data structure. Anyone proving the genuine Hessian target cites this constructor. The body simply wires the canonical Hessian, its symmetry proof, and the second-variation identity into the structure fields.
Claim. Given a finite 3D triangulation $K$ with incidence consistency $h_K$, there is a concrete second-order Regge data package whose Hessian is the canonical dual-weight graph Laplacian of $K$, whose second-order action is the quadratic form built from that Hessian, and whose second variation equals $\tfrac12$ times the Hessian quadratic form.
background
The module isolates the final analytic Hessian step for a finite 3D Regge triangulation under the conformal ansatz. A triangulation $K$ carries vertices, edges, and tetrahedra; incidence consistency $h_K$ guarantees that dual weights and deficit angles are well-defined.
The canonical Hessian is the graph Laplacian induced by incidence dual weights: diagonal entries sum the dual weights off a vertex, off-diagonal entries are minus the dual weight between vertices. The structure ConcreteReggeSecondOrderData packages a second-order action, a symmetric Hessian matrix, the identity that the action equals the quadratic form built from that Hessian, and the second-variation identity relating the action difference from the zero potential to half the Hessian quadratic form. The exact quadratic identity is intentionally about the second-order action, not the full nonlinear Regge action.
proof idea
Definitional constructor, not a tactic proof. It fills each field of the structure: second-order action is reggeActionSecondOrder applied to the canonical Hessian; hessian is canonicalReggeHessian; symmetry is the existing theorem canonicalReggeHessian_symm; the equality secondOrderAction_eq is definitional (rfl); second variation is the lemma reggeActionSecondOrder_secondVariation at the canonical Hessian.
why it matters
This is the canonical witness that discharges the genuine Hessian target. Downstream, genuineReggeHessianTarget simply introduces an arbitrary incidence-consistent triangulation and returns this package, converting concrete action data into the shared ReggeHessianData interface.
In the Recognition geometry stack, the Regge action under the conformal ansatz is the discrete curvature cost on the triangulation; packaging its second-order expansion with the incidence Laplacian closes the analytic step that links discrete deficit angles to a quadratic form ready for continuum comparison. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it supplies the geometric Hessian data those continuum limits would consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.