reggeActionRemainder_secondVariation_zero
plain-language theorem explainer
Along every straight line of vertex potentials through the flat configuration, the nonlinear remainder of the Regge action has vanishing second derivative at the origin, once a named analytic input package is supplied. Discrete-gravity and Regge-calculus workers cite this when isolating the cubic Taylor remainder from the quadratic Hessian term. The proof is a one-line field projection from that input structure.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation. Suppose the remainder second-variation input package for $K$ holds. Then for every vertex potential $\xi$, the real map $t \mapsto$ (Regge-action remainder of the canonical Hessian evaluated on the line potential of $\xi$ at $t$) has second derivative equal to $0$ at $t=0$.
background
The module packages second-variation and cubic-remainder targets for the nonlinear Regge action in a form usable before the full Cayley-Menger/arccos chain-rule expansion is finished. Analytic obligations that still depend on that expansion live in named input structures rather than as free-standing theorems.
CanonicalRemainderSecondVariationZero asserts that the canonical nonlinear remainder has zero second variation at the flat potential: for every vertex potential $\xi$, the scalar path $t \mapsto$ remainder along the line potential of $\xi$ admits a second derivative at $t=0$ equal to zero. The companion input structure ReggeActionRemainderSecondVariationInput simply packages that proposition as a hypothesis field, parallel to the first-variation module imported upstream.
Line potentials are the straight affine paths in the space of vertex potentials through the zero (flat) configuration; the Hessian quadratic form and the remainder are the second-order and higher-order pieces of the Regge action along those paths.
proof idea
One-line term-mode wrapper. The hypothesis is an inhabitant of the input structure whose sole field is exactly the target proposition CanonicalRemainderSecondVariationZero. The proof projects that field and returns it.
why it matters
In the Recognition geometry stack this isolates the cubic (and higher) Taylor remainder of the nonlinear Regge action from the quadratic Hessian contribution at flat space. The module doc frames the target as the usable interface while the large Cayley-Menger/arccos expansion remains incomplete; discharging the input structure later closes that analytic gap without rewriting downstream consumers.
No downstream theorems currently depend on this declaration (used_by is empty), so it is a leaf interface rather than a link in a longer proved chain. It sits beside the sibling second-variation equality with the canonical Hessian and the local cubic bound for the same remainder. Framework-wise it supports the discrete-geometry side of the forcing picture (spatial dimension and triangulation structure) without yet touching T5-T8 constants or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.