reggeActionRemainderSecondVariationInput_of_flat_nonlinearHessian
plain-language theorem explainer
From a flat configuration and the nonlinear directional Hessian theorem on an incidence-consistent 3D triangulation, this builds the remainder second-variation input package (canonical remainder has vanishing second variation at the flat point). Cited by the cubic Taylor and remainder-closure layers. One-line structure constructor wrapping the canonical remainder vanishing lemma.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Given a flat analytic configuration on $K$ and the nonlinear directional Hessian theorem (for every vertex potential $\xi$, the second derivative of the Regge action along the line through $\xi$ at $0$ equals the canonical incidence Hessian quadratic form), one obtains the remainder second-variation input: the canonical remainder has vanishing second variation on $K$.
background
This module isolates the hard endpoint of the nonlinear Regge calculation: the second directional derivative of the full nonlinear action at the flat potential must match the canonical incidence Hessian. Once that holds, the existing second-variation input package follows at once.
A flat configuration packages three facts: arccos endpoints stay off $\pm 1$, all deficits vanish at the base point, and the nonlinear action is smooth enough for Taylor theory. The nonlinear directional Hessian theorem asserts that for every vertex potential $\xi$, $$\mathrm{HasSecondDerivAt},(\mathrm{actionAlongLine},\xi),(\mathrm{hessianQuadratic}(H_{\mathrm{can}}),\xi),0.$$
The target structure ReggeActionRemainderSecondVariationInput is a single-field package whose only obligation is CanonicalRemainderSecondVariationZero: the remainder after subtracting the canonical quadratic has vanishing second variation at the flat point.
proof idea
One-line structure constructor. The sole field remainder_secondVariation_zero is filled by applying canonicalRemainderSecondVariationZero_of_nonlinearHessian_and_flatConfiguration to the same triangulation, incidence hypothesis, flat configuration, and nonlinear Hessian theorem. That upstream theorem reduces the claim to the already-proved combination of the Hessian theorem with action-line differentiability near zero.
why it matters
This is the handoff from the nonlinear Hessian proof interface into the second-variation and cubic-Taylor layers. Downstream, reggeActionRemainderSecondVariationInput_of_flat_directionalHessian is a thin re-export of this constructor; nonlinearReggeLocalHessianTaylorInputs_of_hessian_and_taylor and the remainder-closure audit nonlinearReggeLocalHessianTaylorInputs_closed consume it to assemble the local Hessian/Taylor input package used by the nonlinear correspondence layer.
In the Recognition geometry stack this closes the second-variation side of the Regge remainder once the directional Hessian calculation is supplied, matching the module claim that the Hessian theorem is "the exact endpoint of the second chain-rule calculation" rather than a new assumption. It does not itself prove the Hessian identity; it packages the consequence for the remainder pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.