hingeMeasureUnderConformal_hasDerivAt_line_zero
plain-language theorem explainer
Along a conformal line of vertex potentials, the hinge measure on any edge is differentiable at the flat point t=0, with derivative equal to the directional hinge derivative. Anyone assembling the first variation of the nonlinear Regge action on a 3D triangulation cites this. The proof is elementary real calculus: differentiate the edge-averaged potential, compose with exp, and scale by the fixed square-root edge length.
Claim. Let $K$ be an incidence-consistent 3D triangulation, $\eta$ a real potential on its vertices, and $e$ an edge. The scalar map $t\mapsto m_e(t\eta)$, sending $t$ to the hinge measure of $e$ under the conformal deformation generated by the line potential $t\eta$, is differentiable at $t=0$, and $$\frac{d}{dt}\big|_{t=0} m_e(t\eta)$$ equals the directional derivative of the hinge measure in the direction $\eta$.
background
This module develops the first variation of the full nonlinear Regge action on a 3D triangulation. The geometric target is vanishing of that variation at the flat conformal potential, via Schläfli cancellation plus zero deficit; the analytic work is to justify differentiating hinge contributions under conformal edge scaling.
A vertex potential $\eta$ generates a conformal deformation of edge lengths: each edge $e$ with endpoints $(u,v)$ is rescaled by a factor built from $\exp((\eta_u+\eta_v)/2)$ times a fixed square-root reference length from the incidence package. The line potential $t\mapsto t\eta$ is the straight path through the space of potentials, so $t=0$ is the undeformed (flat) configuration.
The hinge measure under that conformal family is the edge contribution that enters the Regge action. Its directional derivative at the origin is the candidate first-order coefficient used later in the global variation formula.
proof idea
Unfold the hinge measure, the directional derivative, and the line potential. Write $uv$ for the two endpoints of edge $e$. First show that $t\mapsto (t\eta_u+t\eta_v)/2$ has derivative $(\eta_u+\eta_v)/2$ at $0$, by adding two constant multiples of the identity and dividing by $2$. Compose with $\mathrm{Real.exp}$ via the chain rule and $\mathrm{exp}'=\mathrm{exp}$, using $\mathrm{exp}(0)=1$, to get the same derivative for the exponential factor. Finally multiply by the $t$-independent constant $\sqrt{\mathrm{globalSqEdge}(e)}$; the product rule for a constant factor finishes the claim after routine reassociation.
why it matters
This is a local analytic lemma in the first-variation pipeline for the nonlinear Regge action. Downstream, directionalFirstVariationFormula_of_deficitPackage packages the global directional first-variation identity once a deficit-angle derivative package is supplied; each edge term needs exactly this differentiability-at-zero fact. Separately, the nonlinear Hessian development equates the hinge line derivative at zero with this directional coefficient, so the present theorem is the bridge between pathwise calculus and the directional formula.
In the module's program, the geometric content is Schläfli cancellation at vanishing deficit; the present result discharges the pure calculus step that the conformal hinge measure is differentiable along lines, so the variation can be written edgewise before summing. It does not itself invoke the eight-tick or $D=3$ forcing chain; it sits in the classical Regge geometry layer that those landmarks later constrain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.