MixedHingeDeficitCanonicalHessianTarget
plain-language theorem explainer
After second-order Schläfli cancellation along a conformal line, the remaining mixed hinge–deficit product at the flat point is required to equal the canonical incidence Hessian quadratic form. Anyone proving the nonlinear Regge second variation cites this as the exact residual identity. It is a pure Prop packaging that identity for a fixed incidence-consistent 3D triangulation.
Claim. For an incidence-consistent 3D triangulation $K$, the following holds: for every vertex potential $\xi$, $$\sum_e \bigl(\partial_t\ell_e(0)\,\partial_t\delta_e(0)\bigr) = \xi^{\mathsf T} H_{\mathrm{can}}(K)\,\xi,$$ where $\partial_t\ell_e$ is the $t$-derivative of conformal hinge length along the line through $\xi$, $\partial_t\delta_e$ is the $t$-derivative of the deficit angle, and $H_{\mathrm{can}}$ is the canonical dual-weight graph Laplacian Hessian.
background
The module isolates the hard endpoint of the nonlinear Regge calculation: the second directional derivative of the conformal Regge action at the flat potential must equal the canonical incidence Hessian. After the second-order Schläfli identity cancels pure deficit and pure hinge second derivatives, a mixed product of first derivatives remains.
Conformal hinge length and deficit angle are evaluated along the one-parameter line of vertex potentials $t\mapsto$ linePotential$(\xi,t)$. Their $t$-derivatives at $t=0$ are the hinge and deficit line derivatives. The canonical Regge Hessian is the graph-Laplacian matrix built from incidence dual weights: diagonal sums of dual weights minus off-diagonal dual weights. The associated quadratic form is the double sum $H_{ij}\xi_i\xi_j$.
This definition packages the claim that the edge-sum of those mixed first-derivative products equals that quadratic form for every $\xi$.
proof idea
No proof body: this is a Prop-valued definition. It simply asserts equality between the edge-sum of hinge-line and deficit-line first derivatives at $t=0$ and the quadratic form of the canonical dual-weight Hessian. Downstream lemmas discharge it from a deficit-angle directional package plus an edge-stencil identity, or from a mixed-from-package target.
why it matters
This is the residual identity after second-order Schläfli cancellation in the nonlinear Regge Hessian chain. The parent theorem secondProductRuleEqualsCanonicalHessian_of_secondSchlaefli_and_mixed takes a flat configuration, a second-Schläfli-along-line hypothesis, and this mixed target, and concludes that the second product rule equals the canonical Hessian. Two constructors feed it: one from a deficit directional package, and one from an edge-stencil plus Dirichlet–stencil agreement. Closing this Prop is the last geometric step before ReggeActionSecondVariationInput follows in the module's forcing path toward the full nonlinear second variation at the flat point (the continuum limit of which is the linearized Einstein–Hilbert Hessian in $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.