CanonicalRemainderSecondVariationZero
plain-language theorem explainer
For any incidence-consistent 3D triangulation, the nonlinear Regge remainder (full action minus flat value minus the canonical quadratic Hessian form) has vanishing second directional derivative at the flat potential, in every vertex-potential direction. Downstream Hessian-identification theorems cite this Prop as their target. It is a pure Prop definition packaging a second-derivative-at-zero statement along rays.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation. Write $R_H(\xi)$ for the Regge action remainder after subtracting the flat value and $\tfrac12$ the quadratic form of a candidate Hessian $H$, and take $H$ to be the canonical dual-weight graph Laplacian. The claim is: for every vertex potential $\xi$, the map $t \mapsto R_H(t\xi)$ has second derivative $0$ at $t=0$.
background
The module packages nonlinear second-variation and cubic-remainder targets for the discrete Regge action on a 3D triangulation, keeping the heavy Cayley–Menger/arccos chain-rule work behind named input structures until that expansion is fully formalized.
The remainder $R_H(\xi)$ is the full Regge action at vertex potential $\xi$, minus its value at the zero (flat) potential, minus $\tfrac12$ times the quadratic form of a candidate Hessian matrix $H$. The canonical choice of $H$ is the graph Laplacian built from incidence dual edge weights. Directional probes use the ray $t\mapsto t\xi$ through the flat configuration.
Second variation along a ray is expressed by HasSecondDerivAt: the first derivative of $f$ itself has derivative equal to a prescribed value at a point. Here the prescribed second derivative is zero at the origin.
proof idea
No proof body: this is a Prop-valued definition. It expands to a universal quantifier over vertex potentials $\xi$, asserting that the scalar path $t \mapsto R_{H_{\mathrm{can}}}(t\xi)$ has second derivative $0$ at $t=0$, with $H_{\mathrm{can}}$ the canonical dual-weight Laplacian. Downstream theorems discharge the Prop by supplying analytic hypotheses (directional Hessian identity, line differentiability, flatness, or identical vanishing of the remainder).
why it matters
This is the standing target for the nonlinear Hessian program: once the remainder’s second variation vanishes at flat space, the canonical graph Laplacian is identified as the true quadratic part of the Regge action, and higher-order (cubic) remainder control can proceed.
It is consumed by a family of discharge theorems in ReggeActionNonlinearHessianProof, including versions from nonlinear directional Hessian plus action-line differentiability, from derivative-identity targets, from flat configurations with linearization or first-order tangency, and from the strong case where the remainder vanishes identically. Those results close the second-variation half of the module’s stated program (second variation and cubic remainder of the nonlinear Regge action).
In the broader Recognition geometry stack this pins the discrete curvature quadratic form used when matching continuum limits and forcing-chain geometric structure (spatial $D=3$, eight-tick discrete time) to a concrete triangulation Hessian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.