MixedHingeDeficitDirichletTarget
plain-language theorem explainer
Defines the remaining mixed hinge-deficit identity with right-hand side written as the canonical graph Dirichlet energy on a 3D triangulation. Anyone closing the nonlinear Regge Hessian chain cites this Prop as the energy-form target. The body is a single universal quantification equating a weighted edge sum of hinge-measure and deficit directional derivatives to that energy.
Claim. For an incidence-consistent 3D triangulation $K$ and a deficit-angle directional-derivative package $D$, the mixed target in Dirichlet form asserts: for every vertex potential $\xi$, $\sum_e (\partial_\xi m_e)\,(\partial_\xi\delta_e) = E_{\mathrm{Dir}}(K,\xi)$, where $m_e$ is the hinge measure, $\delta_e$ the deficit angle on edge $e$, and $E_{\mathrm{Dir}}$ is the canonical graph Dirichlet energy built from the incidence dual weights.
background
The 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 match the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
The right-hand side here is the explicit graph Dirichlet energy associated to the canonical incidence weights, with the usual $1/2$ factor compensating double-counting of oriented vertex pairs. The left-hand side packages the first-variation data: a deficit-angle directional-derivative package supplies, for each edge, the derivative of the deficit along the line of potentials generated by $\xi$, while the hinge-measure directional derivative is the companion edge weight from the first-variation module.
Because the canonical Hessian quadratic form has already been identified with this Dirichlet energy, rewriting the mixed target in energy form is bookkeeping rather than a new geometric claim; it simply makes the remaining identity match the energy language used downstream.
proof idea
Definitional, not a proved theorem. The Prop is the universal statement that for every vertex potential the edge sum of (hinge-measure directional derivative times deficit directional derivative) equals the canonical Dirichlet energy. No tactics or lemmas are applied in the body; discharge happens in the two wrapper theorems that take this target as hypothesis or conclusion.
why it matters
This is the energy-form restatement of the mixed hinge-deficit target inside the nonlinear Regge Hessian proof interface. Downstream, mixedHingeDeficitDirichlet_of_edgeStencil derives it from an edge-stencil form of the mixed target plus equality of the canonical Dirichlet energy with that stencil, and mixedHingeDeficitFromDeficitPackage_of_dirichlet converts it back into the deficit-package form of the mixed target. Together those steps feed the chain-rule endpoint that the second directional derivative at the flat potential equals the canonical incidence Hessian, which is the remaining hard calculation before the full nonlinear second-variation package closes. In the broader Recognition geometry stack this sits in the discrete gravity / Regge sector that realizes the forced $D=3$ spatial setting on triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.