reggeActionSecondOrder_secondVariation
plain-language theorem explainer
Exact second-variation identity: the quadratic Regge truncation at a vertex potential minus its value at the zero potential equals half the Hessian quadratic form. Anyone packaging concrete second-order Regge data on a 3D triangulation cites this. Proof unfolds the second-order action, applies vanishing of the Hessian at zero potential, and closes by ring.
Claim. Let $K$ be an incidence-consistent finite 3D triangulation, $H$ a real bilinear form on the vertices of $K$, and $\xi$ a vertex potential. Then the second-order Regge action at $\xi$ minus the same action at the zero potential equals $\tfrac12$ times the Hessian quadratic form of $H$ evaluated on $\xi$.
background
The module isolates the final analytic Hessian step for a finite 3D Regge triangulation under the conformal ansatz. Edge lengths are deformed by a vertex potential; the Regge action (sum of deficit angles times hinge measures) is expanded, and the quadratic truncation is packaged so it can be fed into the existing ReggeHessianData interface.
The second-order action is the quadratic piece of that expansion. The Hessian quadratic form is the associated symmetric bilinear expression in the vertex potential. A companion lemma records that this quadratic form vanishes on the zero potential, which is the natural background for measuring second variation.
Upstream cost algebra supplies the shifted cost $H(x)=J(x)+1$, but the present identity is purely algebraic in the already-constructed Hessian quadratic and does not reopen the Recognition Composition Law.
proof idea
One short term-mode argument. Unfold the definition of the second-order Regge action. Invoke the sibling lemma that the Hessian quadratic form vanishes on the zero potential. Rewrite that vanishing into the goal and finish by ring arithmetic, which cancels the zero term and leaves half the Hessian quadratic on $\xi$.
why it matters
This is the exact second-variation clause required by the concrete Regge action package. Downstream, canonicalReggeSecondOrderData installs the second-order action and the canonical Hessian into a single data bundle for an incidence-consistent triangulation; that bundle is the bridge from discrete Regge calculus to the continuum Hessian interface used later in the geometry stack.
In the broader Recognition framework the identity sits inside the geometric forcing chain that eventually supports $D=3$ and the eight-tick discrete structure: a well-defined second variation of the Regge action is a prerequisite for matching discrete curvature to continuum Einstein-Hilbert behaviour. It does not itself force dimension or the golden ratio; it closes the analytic bookkeeping so those later steps can quote a clean quadratic form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.