CanonicalHessianSecondVariationAtZero
plain-language theorem explainer
For any incidence-consistent 3D triangulation, the nonlinear Regge action restricted to every conformal line through the flat potential has second derivative at the origin equal to the quadratic form of the canonical incidence Hessian. Geometers working the Phase-D second-variation program cite this Prop as the named target. It is a pure definition of that analytic claim, not a proved theorem.
Claim. Let $K$ be a 3D triangulation with consistent incidence data. Write $S_K$ for the nonlinear Regge action and $H_K$ for the canonical incidence Hessian (graph Laplacian from dual edge weights). For every vertex potential $\xi$, the map $t \mapsto S_K(\phi_0 + t\xi)$ (conformal line through the flat potential $\phi_0$) is twice differentiable at $t=0$ with second derivative equal to the Hessian quadratic form $H_K(\xi,\xi)$.
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 complete. Analytic obligations sit in named input structures rather than unfinished expansions.
The canonical Regge Hessian is the graph-Laplacian matrix induced by incidence dual weights: diagonal entries sum dual weights out of a vertex, off-diagonal entries are minus the dual weight. The quadratic form of that matrix is the candidate second variation at flat space.
actionAlongLine restricts the nonlinear action to the one-parameter family of potentials obtained by adding a real multiple of a fixed vertex potential $\xi$ to the flat configuration. HasSecondDerivAt is the standard real-analysis predicate that a real function has a prescribed second derivative at a point. The present definition asserts that predicate for every direction $\xi$, with value equal to the Hessian quadratic form at $t=0$.
proof idea
Definitional, not a proof. The body is the universal quantification over vertex potentials $\xi$ of the second-derivative-at-zero statement for actionAlongLine with value hessianQuadratic of canonicalReggeHessian. No tactics or lemmas are applied; downstream theorems discharge or package this Prop.
why it matters
This Prop is the Phase-D second-variation target for the full nonlinear action. ReggeActionSecondVariationInput stores it as the field canonical_secondVariation, and the constructor reggeActionSecondVariationInput_of_directionalSecondVariation wraps a proof of it into that structure. The conditional theorem reggeAction_secondVariation_eq_canonicalHessian then simply projects the field out, giving the second-variation identity once the named input is supplied.
On the proof side, canonicalHessianSecondVariation_of_nonlinearDirectionalHessian shows that any proof of the nonlinear directional Hessian theorem immediately yields this Prop (identity coercion). In the broader Recognition geometry stack, matching the second variation of the nonlinear action to the canonical incidence Hessian is the discrete analogue of recovering the linearized Einstein operator from the Regge action at flat space, a prerequisite for stability and continuum-limit arguments on the triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.