secondProductRuleEqualsCanonicalHessian_of_eventuallyZero_and_edgeStencil
plain-language theorem explainer
At a flat 3D Regge triangulation, the second product-rule expression for the nonlinear action equals the canonical incidence Hessian quadratic form, once the weighted deficit derivative vanishes near zero and the mixed hinge/deficit term matches the edge stencil. Geometric analysts of discrete gravity cite it to close the second-variation identity. The proof chains a near-flat Schläfli stationarity lemma into a mixed-term edge-stencil identification, then applies the second-product-rule reduction.
Claim. Let $K$ be an incidence-consistent 3D triangulation that is flat. Suppose the weighted sum of hinge measures times deficit-line derivatives vanishes in a neighbourhood of $t=0$ along every conformal line, the mixed hinge/deficit directional form equals the canonical edge-stencil Dirichlet energy, and that edge stencil equals the abstract canonical Dirichlet energy. Then for every vertex potential $\xi$, the second product-rule derivative of the Regge action at the flat point equals the quadratic form of the canonical Regge Hessian on $\xi$.
background
This module isolates the hard second-order calculation for the nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. The endpoint is not a new axiom; it is the exact identity left after the second chain-rule expansion, from which ReggeActionSecondVariationInput follows.
The conclusion target states that reggeActionSecondProductRuleDerivative at $t=0$ equals hessianQuadratic of canonicalReggeHessian. One hypothesis is the strong near-flat Schläfli form: the weighted deficit-derivative sum is eventually zero in a puncture-free neighbourhood of the flat point along conformal lines. Another is the edge-stencil form of the mixed hinge/deficit target, meant for the periodic Freudenthal branch where the abstract Dirichlet energy has already been identified with the concrete edge stencil. The third equates that canonical Dirichlet energy with the edge stencil.
Upstream, a DeficitAngleDirectionalDerivativePackage packages directional derivatives of deficit angles whose cancellation field is the global Schläfli contribution in the conformal direction. Spatial dimension $D=3$ is the ambient setting forced by the Recognition forcing chain (T8).
proof idea
Term-mode composition of three lemmas. First, weightedDeficitDerivativeStationary_of_eventuallyZero weakens the neighbourhood-vanishing hypothesis to ordinary stationarity of the weighted deficit derivative at the flat point. Second, secondSchlaefliAlongLine_of_weightedStationary turns that stationarity into the second-order Schläfli identity along the conformal line (after flatness kills the explicit deficit-at-zero term). Third, mixedHingeDeficitCanonicalHessian_of_edgeStencil converts the mixed hinge/deficit edge-stencil hypothesis plus Dirichlet-equals-stencil into the mixed term equaling the canonical Hessian. The outer lemma secondProductRuleEqualsCanonicalHessian_of_secondSchlaefli_and_mixed assembles those two pieces into the final product-rule identity.
why it matters
This is a key discharge step in the nonlinear Regge Hessian interface: once the second product-rule expression equals the canonical Hessian, the full second directional derivative at flatness is identified with the incidence quadratic form. The sole recorded consumer is productRuleDerivativeCanonicalHessian_of_eventuallyZero_and_edgeStencil, which continues the same hypothesis package one layer closer to the complete second-variation input.
In the Recognition geometry stack this pins discrete curvature second variation to the canonical Dirichlet/edge-stencil energy on 3D triangulations, consistent with $D=3$ from the forcing chain. It does not itself invoke J-cost, $\varphi$, or the eight-tick octave; those enter elsewhere. The remaining open work sits in proving the eventually-zero Schläfli target and the mixed edge-stencil target on concrete triangulations, not in this reduction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.