nonlinearDirectionalHessian_of_remainder_identically_zero
plain-language theorem explainer
If the nonlinear remainder of the 3D Regge action vanishes identically against the canonical incidence Hessian, then the second directional derivative of the action along every conformal line at the flat potential equals that Hessian quadratic form. Cite this when discharging the nonlinear Hessian endpoint under a vanishing-remainder hypothesis. The proof splits the action along the line, drops the remainder, and transfers the known second derivative of the pure quadratic term across a constant shift.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Suppose that for every vertex potential $\xi$, the nonlinear Taylor remainder of the Regge action after subtracting its flat value and $\tfrac12$ times the canonical incidence-Hessian quadratic form is zero. Then for every $\xi$, the map $t \mapsto S(t\xi)$ has second derivative at $t=0$ equal to that same Hessian quadratic form evaluated on $\xi$.
background
This module isolates the remaining hard step for the full nonlinear Regge action: the second directional derivative at the flat potential must match the canonical incidence Hessian. The endpoint is not a new physical assumption; it is the exact close of the second chain-rule calculation, after which ReggeActionSecondVariationInput follows.
The concrete Regge action under the vertex-conformal ansatz is a sum over edges of hinge measure times deficit angle. The remainder after the flat value and a candidate quadratic Hessian term is reggeActionRemainder. The canonical Hessian is the graph Laplacian built from incidence dual weights. Along a conformal line $t\mapsto t\xi$, the action splits exactly into flat value plus canonical quadratic plus remainder term (the algebraic reduction actionAlongLine_canonical_split).
NonlinearReggeDirectionalHessianTheorem is the Prop that every such line has second derivative at zero equal to the canonical Hessian quadratic on $\xi$.
proof idea
Fix a direction $\xi$. Apply actionAlongLine_canonical_split to write the action along the line as flat value plus canonical quadratic plus remainder along the line. The hypothesis that the remainder vanishes for every potential, specialized along the line and simplified via canonicalRemainderAlongLine, kills the remainder, so the action equals a constant (the flat action) plus canonicalQuadraticAlongLine.
Invoke canonicalQuadraticAlongLine_hasSecondDerivAt_zero, which already supplies the second derivative of the pure quadratic piece at $t=0$. Lift across the additive constant with hasSecondDerivAt_const_add. Rewrite via the simplified action identity to conclude the second-derivative claim for the full nonlinear action along the line.
why it matters
In the Recognition geometry stack this is a clean discharge lemma for the nonlinear Regge Hessian endpoint: whenever the remainder against the canonical incidence Hessian is identically zero, the directional second-variation theorem holds with no further analysis. The module doc frames that theorem as the exact endpoint of the second chain-rule calculation needed before ReggeActionSecondVariationInput.
No downstream consumers are wired yet (used_by is empty), so the lemma presently sits as a proved interface branch alongside sibling routes that assume first-order tangency or near-zero linearization of the action derivative. It separates the algebraic remainder-vanishing case from the harder analytic expansion (product rule, Cayley-Menger/arccos, hinge derivatives, Schläfli cancellation). Within RS geometry this supports matching discrete curvature second variation to the incidence Laplacian that feeds continuum limits and forcing-chain geometry (spatial structure after T8), without touching mass ladders or coupling constants directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.