mixedHingeDeficitDirichlet_of_edgeStencil
plain-language theorem explainer
From the edge-stencil form of the mixed hinge-deficit identity and the equality of canonical Dirichlet energy with that stencil, one obtains the Dirichlet-energy form of the same mixed target. Anyone wiring a deficit-angle package into the nonlinear Regge Hessian cites this bridge. The argument is a pointwise double rewrite along an arbitrary vertex potential.
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$ the mixed sum $\sum_e (\partial_\xi m_e)\,(\partial_\xi\delta_e)$ equals the canonical edge-stencil Dirichlet energy, and that this edge-stencil energy equals the canonical graph Dirichlet energy. Then the same mixed sum equals the canonical Dirichlet energy for every $\xi$.
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 hinge-deficit identity is the cross term that appears after differentiating hinge measures against deficit angles along a conformal line of vertex potentials.
Two presentations of that identity are kept side by side. The edge-stencil form equates the mixed sum to the concrete periodic edge stencil (the form natural on the Freudenthal branch). The Dirichlet form equates the same sum to the abstract graph Dirichlet energy already known to equal the canonical Hessian quadratic. A separate target records that those two right-hand sides agree pointwise on vertex potentials.
Upstream, a deficit-angle directional-derivative package supplies the maps $\xi\mapsto\partial_\xi\delta_e$ together with the HasDerivAt witnesses along each conformal line. The hinge-measure directional derivatives come from the first-variation layer.
proof idea
Fix an arbitrary vertex potential $\xi$. Apply the edge-stencil hypothesis at $\xi$ to replace the mixed sum by the canonical edge-stencil Dirichlet energy. Then apply the Dirichlet-equals-edge-stencil hypothesis at $\xi$ to rewrite that energy as the canonical Dirichlet energy. The resulting equality is exactly the Dirichlet form of the mixed target at $\xi$. No further analytic work is required; the proof is a two-step rewrite.
why it matters
The immediate consumer is mixedHingeDeficitFromDeficitPackage_of_edgeStencil, which lifts the Dirichlet form into the full mixed-hinge-deficit-from-package target used by the nonlinear Hessian assembly. That assembly is the endpoint of the second chain-rule calculation advertised in the module doc: once the mixed identity is in Dirichlet form, ReggeActionSecondVariationInput follows and the second directional derivative at the flat potential equals the canonical incidence Hessian.
In the broader Recognition geometry stack this closes a presentation gap rather than a physical assumption: the edge stencil is the computable object on periodic triangulations, while the Dirichlet energy is the object already matched to the Hessian quadratic. Bridging them keeps the nonlinear proof independent of which energy presentation a later branch prefers. Spatial dimension $D=3$ is ambient via the triangulation type, consistent with the T8 forcing of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.