mixedHingeDeficitFromDeficitPackage_of_edgeStencil
plain-language theorem explainer
On an incidence-consistent 3D triangulation, if the mixed hinge/deficit pairing equals the canonical edge-stencil Dirichlet energy and that stencil matches the abstract Dirichlet energy, then the pairing equals the quadratic form of the canonical Regge Hessian. Discrete-gravity and Regge-calculus workers cite this when routing the nonlinear second variation through the concrete periodic Freudenthal branch. The proof is a two-step term composition through the Dirichlet intermediate.
Claim. Let $K$ be an incidence-consistent 3D triangulation and let $D$ be a directional-derivative package for deficit angles on $K$. Suppose that for every vertex potential $\xi$, $\sum_e (\partial_\xi \mu_e)\, D.(\partial\delta)_e(\xi)$ equals the canonical edge-stencil Dirichlet energy of $\xi$, and that the abstract canonical Dirichlet energy coincides with that edge stencil. Then for every $\xi$ the same mixed sum equals the quadratic form of the canonical Regge Hessian on $\xi$.
background
This module isolates the hard endpoint of the nonlinear Regge second-variation calculation: the second directional derivative of the Regge action at the flat potential must recover the canonical incidence Hessian. The mixed hinge/deficit pairing is the surviving cross term after the first-variation Schläfli cancellation.
A DeficitAngleDirectionalDerivativePackage packages, for each edge, a directional derivative of the deficit angle along conformal lines of vertex potentials, with a HasDerivAt witness. The edge-stencil target asserts that the mixed sum of hinge-measure derivatives times those deficit derivatives equals the concrete periodic edge-stencil Dirichlet energy. The companion hypothesis CanonicalDirichletEqualsEdgeStencilTarget identifies that stencil with the abstract canonical Dirichlet energy already known to match the Hessian quadratic form.
The deficit-package target strips opaque deriv wrappers and states the identification directly in terms of D.deficitDeriv and hessianQuadratic (canonicalReggeHessian K hK).
proof idea
Term-mode composition of two prior lemmas. First apply mixedHingeDeficitDirichlet_of_edgeStencil to the edge-stencil hypothesis and the Dirichlet-equals-stencil hypothesis; that yields the Dirichlet-energy form of the mixed target. Feed the result into mixedHingeDeficitFromDeficitPackage_of_dirichlet, which rewrites the Dirichlet energy as the canonical Hessian quadratic and discharges the deficit-package target. No new analytic work occurs at this node.
why it matters
This is a routing lemma on the path from the concrete Freudenthal edge stencil to the full nonlinear Hessian theorem. Its sole downstream consumer is mixedHingeDeficitCanonicalHessian_of_edgeStencil, which lifts the deficit-package form to the opaque-deriv canonical-Hessian target used by the second-variation interface.
In the Recognition Geometry stack the goal is that the second directional derivative of the Regge action at flat space equal the canonical incidence Hessian, so that ReggeActionSecondVariationInput follows without a new assumption. The module doc states this is "the exact endpoint of the second chain-rule calculation." The present theorem closes the edge-stencil branch of that chain for the mixed hinge/deficit term, keeping the nonlinear Hessian proof interface free of stencil-specific bookkeeping.
It sits in the discrete-geometry layer that supports continuum limits and curvature matching; it does not itself invoke the forcing chain T0–T8, but inherits $D=3$ triangulations from that geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.