canonicalRemainderSecondVariationZero_of_identically_zero
plain-language theorem explainer
If the nonlinear Regge remainder vanishes for every vertex potential when the Hessian is the canonical incidence Laplacian, then that remainder has vanishing second directional derivative along every ray through the flat configuration. Cite this when discharging the second-variation-zero interface for the nonlinear Regge Hessian. The argument is a short reduction: along each ray the remainder is the zero function, whose second derivative is zero by the constant-function derivative lemma.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Suppose that for every vertex potential $\xi$, the nonlinear Regge remainder (full Regge action minus its value at the zero potential minus half the quadratic form of the canonical incidence Hessian) equals zero. Then for every direction $\xi$, the map $t \mapsto$ remainder evaluated on the ray $t\xi$ has second derivative zero at $t=0$.
background
This module isolates the hard endpoint of the nonlinear Regge calculation: the second directional derivative of the full Regge action at the flat (zero) potential must match the canonical incidence Hessian. The remainder is defined by subtracting the constant term and a candidate quadratic form from the action, so vanishing second variation of the remainder is exactly the statement that the Hessian of the action is that candidate.
The canonical Hessian is the graph Laplacian built from incidence dual weights on the triangulation. Vertex potentials are real assignments to vertices; the line through the flat configuration in direction $\xi$ is the ray $t \mapsto t\xi$. The target proposition CanonicalRemainderSecondVariationZero asserts that, for every such direction, the remainder along that ray has second derivative zero at $t=0$ (via the local HasSecondDerivAt predicate).
The hypothesis here is stronger than a second-derivative claim: it assumes the remainder itself is identically zero as a function of the potential, not merely flat to second order at zero.
proof idea
Fix an arbitrary direction $\xi$. Unfold the second-derivative predicate so the goal is a derivative statement about $t \mapsto$ remainder of the ray $t\xi$. By the global vanishing hypothesis applied to every point on that ray, that univariate map equals the constant-zero function. Rewrite the goal under that equality, then invoke the standard fact that the constant-zero map has derivative zero at zero (applied once in the unfolded second-derivative packaging). No triangulation combinatorics or Hessian algebra is used.
why it matters
In the Recognition geometry stack, matching the nonlinear Regge action's second variation to the canonical incidence Laplacian is the remaining hard step before the second-variation input package closes. The module doc states that once that chain-rule calculation is supplied, ReggeActionSecondVariationInput follows immediately; this lemma is the trivial discharge path when the remainder is not merely $o(|\xi|^2)$ but identically zero.
It sits among the sibling targets for directional Hessian identification (linearization near zero, first-order tangency, nonlinear directional Hessian). With no downstream uses yet recorded, it is a proved interface lemma ready for the full nonlinear Hessian theorem rather than a leaf of a finished chain. Framework-wise it supports the discrete geometric side of the forcing story (spatial structure on triangulations) without touching the T5–T8 constant-forcing landmarks directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.