reggeActionSecondVariationInput_of_flat_actionDerivativeTangency
plain-language theorem explainer
From first-order tangency of the action derivative to the canonical Hessian line along every conformal direction, one obtains the full second-variation input package at a flat configuration. Anyone assembling the nonlinear Regge Hessian interface cites this packaging step. The body is a two-step composition: tangency implies the directional Hessian theorem, which then feeds the existing flat-to-second-variation constructor.
Claim. Let $K$ be an incidence-consistent 3D triangulation that is flat. Suppose that for every vertex potential $\xi$, the map $t \mapsto \partial_t S(t\xi) - t\,Q_{\mathrm{can}}(\xi)$ has derivative zero at $t=0$, where $Q_{\mathrm{can}}$ is the canonical incidence Hessian quadratic form. Then the named second-variation input for the full nonlinear Regge action at that flat configuration is available.
background
The module isolates the remaining hard step for the nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. Once that identity is in hand, the structure ReggeActionSecondVariationInput (canonical second variation at zero on a flat configuration) follows at once.
The hypothesis used here is first-order tangency of the action derivative: along each conformal line $t\mapsto t\xi$, the first derivative of the action minus $t$ times the canonical Hessian quadratic is itself differentiable at $t=0$ with derivative zero. Unlike a full linearization-near-zero target, this permits cubic and higher Regge terms; only the first-order contact with the Hessian line is required.
Upstream, that tangency proposition already implies the nonlinear directional Hessian theorem (second derivative of the action along each line equals the canonical quadratic). A sibling constructor then turns any such Hessian theorem, together with flatness, into the second-variation input structure.
proof idea
One-line composition of two existing constructors. First apply the theorem that first-order action-derivative tangency yields the nonlinear directional Hessian theorem. Pass that Hessian witness, with the given flat configuration, into the constructor that builds ReggeActionSecondVariationInput from a nonlinear Hessian theorem. No new analytic work occurs at this layer.
why it matters
This is the packaging bridge from the sharp tangency target (the module's preferred Hessian endpoint, allowing higher-order Regge remainders) down to the named second-variation input consumed by the rest of the Regge calculus. The immediate parent is the further constructor that starts from tangency-to-quadratic and routes through this definition. In the Recognition geometry stack it closes the interface between the hard chain-rule calculation at flat configurations and the second-variation infrastructure used for stability and continuum limits of the discrete action. It does not itself prove the tangency identity; it records that once tangency is supplied, the second-variation package is free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.