mixedHingeDeficitFromDeficitPackage_of_dirichlet
plain-language theorem explainer
If the mixed hinge-measure/deficit-derivative pairing equals the canonical graph Dirichlet energy on every vertex potential, then it equals the quadratic form of the canonical Regge Hessian. Anyone closing the nonlinear second-variation identity for 3D Regge calculus cites this bridge. The proof is a one-line rewrite plus the already-proved Hessian-quadratic/Dirichlet equality.
Claim. Let $K$ be an incidence-consistent 3D triangulation and $D$ a deficit-angle directional-derivative package on $K$. If for every vertex potential $\xi$ one has $\sum_e m'_e(\xi)\,\delta'_e(\xi)=E_{\mathrm{Dir}}(K,\xi)$ (Dirichlet energy form of the mixed target), then $\sum_e m'_e(\xi)\,\delta'_e(\xi)=Q_{H_{\mathrm{can}}}(\xi)$ (Hessian-quadratic form of the mixed target).
background
This module isolates the remaining hard step for the full nonlinear Regge action: the second directional derivative of the action at the flat potential must match the canonical incidence Hessian. The mixed target is the surviving cross term pairing hinge-measure directional derivatives with deficit-angle directional derivatives from a first-variation package $D$.
Two equivalent presentations of that target are in play. The deficit-package form asks that the mixed sum equal the quadratic form of the canonical Regge Hessian. The Dirichlet form asks the same sum equal the canonical graph Dirichlet energy on the incidence graph of $K$. Upstream work already identifies those two right-hand sides: the canonical Hessian quadratic equals the Dirichlet energy pointwise on vertex potentials.
The local setting is pure discrete geometry on incidence-consistent 3D triangulations; the Recognition forcing chain enters only indirectly via the ambient constants and dimension $D=3$ used to build the triangulation and Hessian infrastructure.
proof idea
Term/tactic hybrid, three steps. Introduce an arbitrary vertex potential $\xi$. Rewrite the mixed sum by the Dirichlet-target hypothesis, replacing it with the canonical Dirichlet energy. Finish by symmetry of the already-proved identity canonicalReggeHessian_quadratic_eq_dirichlet, which equates that energy to the Hessian quadratic form. No new analytic work; pure transport of right-hand sides.
why it matters
Closes one presentation bridge inside the nonlinear Regge Hessian proof interface. Downstream, mixedHingeDeficitFromDeficitPackage_of_edgeStencil composes this with the edge-stencil identification of Dirichlet energy, the form used on the canonical periodic Freudenthal branch. Once any of these mixed-target presentations is discharged, the existing second-variation input package follows and the second directional derivative at flat space equals the canonical incidence Hessian. That is the exact endpoint named in the module doc for the full nonlinear Regge chain-rule calculation. Framework landmarks touched only at the geometry layer (3D triangulation, incidence Hessian); no direct appeal to T5–T8 or the RCL here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.