reggeActionSecondOrder
plain-language theorem explainer
Defines the quadratic second-order truncation of the concrete 3D Regge action: value at the zero vertex potential plus half the Hessian quadratic form in a candidate matrix H. Anyone proving exact second-variation identities or packaging ConcreteReggeSecondOrderData cites this. The body is a one-line arithmetic definition, not a derived equality.
Claim. For an incidence-consistent finite 3D triangulation $K$, a candidate Hessian matrix $H$ on vertex pairs, and a vertex potential $\xi$, the second-order Regge truncation is $$S^{(2)}(K,H,\xi) := S_{\mathrm{Regge}}(K,0) + \tfrac12\, Q_H(\xi),$$ where $S_{\mathrm{Regge}}(K,0)$ is the full conformal Regge action at the zero potential and $Q_H$ is the quadratic form associated to $H$.
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 with an incidence-consistency hypothesis so dihedral angles, hinge measures, and deficit angles are well-defined. The full nonlinear Regge action sums local deficit contributions over hinges after a conformal rescaling of squared edge lengths by a vertex potential.
Exact second-variation statements are definitionally clean only for a quadratic truncation, not for the full nonlinear action. The candidate Hessian $H$ is an arbitrary symmetric real matrix on vertex indices; the associated quadratic form is the usual $\frac12$ bilinear pairing against the potential. Upstream cost algebra ($H(x)=J(x)+1$) and bridge constants appear in the broader RS stack but are not parameters of this definition.
Sibling objects in the same file include the full reggeAction, a nonlinear Taylor remainder, and a Taylor decomposition that relates the three.
proof idea
Pure definition: evaluate the full conformal Regge action at the zero vertex potential, add one-half the Hessian quadratic form of the candidate matrix $H$ on the potential $\xi$, and return that real number. No lemmas are applied; there is no tactic proof.
why it matters
This is the object for which exact quadratic second-variation identities hold by unfolding, as in the sibling theorem that the second-order action minus its value at zero equals half the Hessian quadratic. The structure ConcreteReggeSecondOrderData packages a second-order action, a Hessian, symmetry, and the equality that the action equals this truncation; the canonical instance fills the action field with this definition at the incidence Hessian.
Downstream gravity work on the physical six-tetrahedron cubic Dirichlet instance uses those packages in periodic edge-stencil comparison certificates and spacing-refinement convergence into the Track 1.B second-order continuum wrapper. In the RS geometry chain this is the concrete bridge from discrete Regge calculus on a 3D triangulation (forced $D=3$ in the forcing chain) to a Hessian interface usable by continuum comparison, without yet claiming the nonlinear remainder vanishes or that the continuum normalization estimate is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.