ProductRuleDerivativeCanonicalHessianTarget
plain-language theorem explainer
Names the Prop that the product-rule first derivative of the conformal Regge action, as a function of the line parameter, has derivative at the flat point equal to the canonical incidence Hessian quadratic form. Geometric analysts closing the nonlinear second-variation chain cite it as the final derivative target. It is a pure Prop abbreviation, not a proved statement.
Claim. For an incidence-consistent 3D triangulation $K$ and every vertex conformal potential $\xi$, the map $t \mapsto$ (product-rule expression for the directional derivative of the Regge action along the conformal line through $\xi$) is differentiable at $t=0$ with derivative equal to the quadratic form of the canonical dual-weight graph Laplacian Hessian evaluated on $\xi$.
background
The module isolates the hard endpoint of the nonlinear Regge second-variation calculation: at the flat conformal potential, the second directional derivative of the full Regge action must match the canonical incidence Hessian. After one differentiation along a conformal line, the action derivative collapses to an exact finite sum (hinge-factor derivative times deficit plus hinge times deficit derivative). That sum is the product-rule expression used here.
Vertex potentials are real assignments on the triangulation vertices. The canonical Regge Hessian is the graph-Laplacian matrix built from incidence dual weights: diagonal row sums of dual weights, off-diagonal minus the dual weight. Its quadratic form is the double sum $H_{ij}\xi_i\xi_j$. The product-rule derivative is that hinge/deficit sum evaluated along the line potential $t\mapsto$ line through $\xi$.
The target asserts that this product-rule map in $t$ has derivative at $0$ equal to that quadratic form. It is an equivalent packaging of the geometric second-variation identity, not a new physical hypothesis.
proof idea
Definitional Prop only: the body is the universal quantification over vertex potentials $\xi$ of HasDerivAt for the product-rule derivative map at $t=0$, with value the canonical Hessian quadratic form on $\xi$. No tactics or lemmas are applied; discharge happens in the surrounding bridge theorems that assume second-product or edge-stencil packages and conclude this target.
why it matters
This is the equivalent final geometric derivative target in the nonlinear Regge Hessian interface. Downstream, several bridge lemmas take it as hypothesis or conclusion: productRuleDerivativeCanonicalHessian_of_secondProduct and the flat/weighted-stationary edge-stencil variants produce it from second-product or stencil packages; productRuleTangencyToQuadratic_of_productRuleDerivativeCanonicalHessian and actionDerivativeTangencyToQuadratic_of_flat_productRuleDerivativeCanonicalHessian consume it to reach action-derivative tangency to the canonical quadratic. Once those hold, the module doc states that ReggeActionSecondVariationInput follows immediately. In the broader RS geometry stack this closes the second chain-rule step that identifies the discrete second variation with the incidence Laplacian, the discrete stand-in for the continuum Hessian of the gravitational action on a 3D triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.