reggeActionSecondVariationInput_of_flat_actionDerivativeLinearization
plain-language theorem explainer
Given an incidence-consistent flat 3D triangulation and the first-derivative linearization of the Regge action along conformal lines near zero, this builds the second-variation input package for the nonlinear Regge action. Cite it when wiring the linearization hypothesis into the second-variation API. The body is a two-step composition: linearization yields the directional Hessian theorem, which yields the input structure.
Claim. For an incidence-consistent 3D triangulation $K$ that is flat, if the derivative of the Regge action along every conformal line is eventually equal near $t=0$ to $t$ times the canonical Hessian quadratic form, then one obtains a second-variation input package for the nonlinear Regge action at that flat configuration.
background
The module isolates the remaining hard calculation for the full nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. Once that calculation is supplied, the existing second-variation input follows immediately.
A flat configuration is a discrete geometry at the zero-curvature point of the Regge potential. The action along a conformal line restricts the full nonlinear Regge action to a one-parameter family of vertex potentials scaled by $t\in\mathbb{R}$. The linearization target asserts that, near $t=0$, $$\partial_t,S(t\xi);=;t,Q_{H}(\xi)$$ eventually in a neighborhood of zero, where $Q_H$ is the quadratic form of the canonical Regge Hessian. That statement is stronger than a bare derivative-at-zero claim and is exactly what recovers the nonlinear directional Hessian.
The second-variation input structure packages a certificate that the canonical Hessian governs the second variation of the action at the flat point.
proof idea
One-line composition of two existing constructors. First apply the theorem that turns the action-derivative linearization-near-zero hypothesis into the nonlinear directional Hessian theorem (the second derivative of the action along each conformal line equals twice the canonical Hessian quadratic). Then feed that Hessian certificate, together with flatness, into the constructor that builds the second-variation input from a nonlinear Hessian theorem.
why it matters
Convenience bridge at the end of the nonlinear Regge Hessian proof interface. The module endpoint is that the second directional derivative at the flat potential equals the canonical incidence Hessian; once the linearization calculation (product rule, Cayley-Menger/arccos derivative, hinge derivative, Schlaefli cancellation) is done, this definition discharges the second-variation input with no further work.
No downstream consumers are wired yet, so it is the ready handoff for any result that needs the second-variation package from the linearization hypothesis rather than from a raw Hessian certificate. In the Recognition geometry stack this supports discrete gravity and Regge second-variation analysis on 3D triangulations, consistent with the forced spatial dimension $D=3$ (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.