hingeMeasureDirectionalDeriv
plain-language theorem explainer
Closed-form directional derivative of conformal hinge length at the flat vertex potential: for edge e it is the Euclidean hinge length times the average of the potential on the two endpoints. First-variation and Hessian arguments for the nonlinear Regge action cite this scalar as the candidate derivative value. The body is a pure definitional formula, not a proved identity.
Claim. Given a 3D triangulation $K$ with incidence consistency, a vertex potential $\eta$, and an edge $e$ with endpoints $u,v$, the directional derivative of the conformal hinge measure at the flat potential equals $\sqrt{\ell_e^{2}}\,(\eta(u)+\eta(v))/2$, where $\ell_e^{2}$ is the global squared length of $e$.
background
This module targets the first variation of the full nonlinear Regge action on a 3D triangulation. The geometric engine is Schläfli cancellation together with vanishing deficit at the flat conformal potential; the analytic work is to differentiate hinge lengths and dihedral angles along conformal deformations and assemble the global sum.
A vertex potential $\eta$ is a real assignment to vertices. The line potential $t\mapsto$ flat $+,t\eta$ is the one-parameter conformal family through the flat background. Hinge measure is the edge length (square root of the global squared edge length from the incidence package). Under a conformal deformation the length scales by the average exponential of the endpoint potentials; linearizing at the flat point yields the average of $\eta$ on the two endpoints times the background length.
Incidence consistency supplies a coherent global squared-edge function and the edge-to-vertex incidence used to read the two endpoints of $e$.
proof idea
Definitional, not a theorem. Read the two endpoints of edge $e$ from the triangulation incidence map, take the square root of the global squared edge length (background hinge length), and multiply by the arithmetic mean of $\eta$ at those endpoints. No lemmas are applied; the expression is the closed form that later HasDerivAt proofs identify as the actual derivative of the conformal hinge measure along the line potential at $t=0$.
why it matters
This scalar is the hinge contribution in every directional first-variation identity for the nonlinear Regge action. Downstream, hingeMeasureUnderConformal_hasDerivAt_line_zero proves that the conformal hinge measure along the line potential is differentiable at zero with this exact derivative. That fact feeds ReggeActionDirectionalFirstVariationFormula and ReggeActionFirstVariationFormula, which package the full first-variation formula (hinge terms plus deficit/angle terms after Schläfli).
The same quantity is reused in the nonlinear Hessian development: hingeLineDeriv_zero_eq_directional equates the line derivative at zero to this definition, and mixed hinge-deficit Hessian targets build on that identification. In the module's program, the first variation must vanish at the flat potential; this definition isolates the hinge half of that calculation so the angle half can cancel via Schläfli and zero deficit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.