hingeLineDeriv_zero_eq_directional
plain-language theorem explainer
At the flat point, the line derivative of the conformal hinge measure equals the first-variation directional derivative of that measure. Anyone assembling the nonlinear Regge Hessian along a conformal ray cites this identification. The proof unfolds the line-derivative definition and reads off the derivative from the known HasDerivAt fact at parameter zero.
Claim. Let $K$ be an incidence-consistent 3D triangulation, $\xi$ a vertex potential, and $e$ an edge. Write $\ell_e(t)$ for the conformal hinge measure of $e$ along the ray $t\mapsto t\xi$ through the flat potential. Then $\ell_e'(0)$ equals the directional derivative of the hinge measure at the flat potential in the direction $\xi$.
background
The module isolates the remaining hard step for the full nonlinear Regge action: the second directional derivative 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.
Under the vertex-conformal ansatz the 3D Regge hinge measure on an edge is the conformal edge length: $\sqrt{q_e},\exp((\xi_u+\xi_v)/2)$, where $q_e$ is the squared reference length. The line through the flat potential in direction $\xi$ is the ray $t\mapsto t\xi$ on vertices. The first-variation module already records the directional derivative of that hinge length at the flat point, namely $\sqrt{q_e},(\xi_u+\xi_v)/2$, and proves that the conformal hinge measure along the ray has derivative equal to that quantity at $t=0$.
The local object hingeLineDeriv is the ordinary real derivative, in the line parameter, of the conformal hinge measure. This lemma simply pins that derivative at zero to the already-named directional derivative.
proof idea
Unfold the definition of the line derivative so the goal is an equality of real derivatives at $0$. Invoke the first-variation theorem that the map $t\mapsto$ conformal hinge measure along the ray has a derivative at $0$ equal to the directional hinge derivative. A one-step convert aligns the function expressions (the two modules each carry a local copy of the line potential). Conclude by reading off .deriv from the HasDerivAt witness.
why it matters
The nonlinear Hessian program needs every first-order hinge factor along a conformal line to match its first-variation counterpart before second derivatives and mixed deficit terms can be assembled. This lemma supplies that match at the evaluation point $t=0$.
It is consumed by mixedHingeDeficitCanonicalHessian_of_deficitPackage, which turns a deficit-angle directional-derivative package plus a mixed-hinge target into the canonical mixed hinge-deficit Hessian target. That target is part of the chain-rule endpoint advertised in the module doc: second directional derivative of the nonlinear Regge action at the flat potential equals the canonical incidence Hessian.
In the broader Recognition geometry stack this is pure discrete GR bookkeeping (Regge calculus on a 3D triangulation under conformal vertex potentials), not a forcing-chain landmark. It closes a definitional seam between the first-variation and nonlinear-Hessian modules so the Hessian proof can stay free of ad-hoc first-order rewrites.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.