MixedHingeDeficitEdgeStencilTarget
plain-language theorem explainer
The mixed hinge-deficit second-variation identity is restated as equality of a global edge sum against the concrete edge-stencil Dirichlet energy. Anyone proving the nonlinear Regge Hessian on the periodic Freudenthal branch cites this Prop as the edge-local form of the mixed target. It is a pure definition: the body is the quantified equality, not a proved statement.
Claim. For a 3D triangulation $K$ with consistent incidence and a deficit-angle directional-derivative package $D$, the following holds: for every vertex potential $\xi$, $\sum_e (\partial_\xi m_e)\,(\partial_\xi\delta_e) = E^{\mathrm{edge}}_{\mathrm{Dir}}(K,\xi)$, where the left-hand side is the mixed hinge-measure/deficit sum over global edges and the right-hand side is the canonical edge-stencil Dirichlet energy $\sum_e \sqrt{\ell_e^2}\,(\xi_{v_1(e)}-\xi_{v_2(e)})^2$.
background
The module isolates the hard second-variation step for the full nonlinear Regge action: at a flat potential the second directional derivative must match the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
A deficit-angle directional-derivative package supplies, for each edge, a map $\xi\mapsto\partial_\xi\delta_e$ together with the corresponding HasDerivAt certificates along the line potential. The hinge-measure directional derivative is the companion first variation of the hinge (area/length) weight. Their product, summed over edges, is the mixed second-variation contribution.
The right-hand side is the concrete edge-stencil Dirichlet energy already identified with the abstract incidence form on the canonical periodic Freudenthal branch: sum over global edges of $\sqrt{\ell_e^2}$ times the squared potential jump. Spatial dimension is the forced $D=3$ of the Recognition chain (T8).
proof idea
No proof: the declaration is a Prop-valued definition. Its body is exactly the universal quantification over vertex potentials of the equality between the mixed hinge-deficit edge sum and canonicalEdgeStencilDirichletEnergy. Downstream theorems take an inhabitant of this Prop as a named hypothesis and discharge the mixed target in edge-stencil form.
why it matters
This is the edge-stencil packaging of the mixed hinge-deficit target used throughout the nonlinear Hessian and correspondence chain. Parent results that consume it include the action-derivative tangency theorems (eventually-zero and weighted-stationary variants), the mixed hinge-deficit canonical Hessian and Dirichlet corollaries in the same module, the local Hessian Taylor-input constructors in ReggeActionCubicTaylorBound, and the local correspondence and strongest true Regge-to-$J$-cost replacement theorems in ReggeActionNonlinearCorrespondence.
In the Recognition geometry stack it is the form meant for the canonical periodic Freudenthal branch, where abstract Dirichlet energy has already been reduced to the concrete edge stencil. Closing this target (by a genuine second-variation calculation) is the remaining hard step named in the module doc before the full nonlinear Regge Hessian is available.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.