hingeLineDeriv_differentiableAt_zero
plain-language theorem explainer
Along a straight ray of vertex potentials, the first t-derivative of the conformally deformed hinge measure on any edge is differentiable at t=0. Cited by the hinge-deficit second-line differentiability lemmas that feed the nonlinear Regge Hessian. Proof reduces the line derivative by chain rule to a pure exponential c√ℓ₀ e^{ct}, then discharges differentiability by fun_prop.
Claim. Let $K$ be an incidence-consistent 3D triangulation, $\xi$ a real potential on its vertices, and $e$ any edge. The map $t\mapsto$ (first $s$-derivative at $s=t$ of the hinge measure of $e$ under the conformal deformation driven by $s\xi$) is differentiable as a real function at $t=0$.
background
In Regge calculus the discrete gravitational action is built from hinge measures times angular deficits. A vertex potential $\xi$ generates a conformal deformation: each edge length scales by an exponential of the average of $\xi$ on its two endpoints. The first $t$-derivative of that deformed hinge measure, evaluated along the ray $s\mapsto s\xi$, is the hinge line derivative appearing in the signature.
This module isolates the remaining analytic step for the full nonlinear Regge Hessian: the second directional derivative of the action at the flat potential must equal the canonical incidence Hessian. Differentiability of the first line derivative at the origin is the prerequisite that lets one differentiate a second time.
Incidence consistency of $K$ supplies a well-defined global squared edge length for every edge, so the conformal factor is unambiguous.
proof idea
Unfold the hinge line derivative, the conformal hinge measure, and the line potential. Let $u,v$ be the endpoints of edge $e$ and set $c=(\xi_u+\xi_v)/2$. The deformed factor is $\sqrt{\ell_0(e)},\exp((s\xi_u+s\xi_v)/2)$.
Compute its $s$-derivative at arbitrary $t$ by elementary calculus: the linear map $s\mapsto(s\xi_u+s\xi_v)/2$ has derivative $c$ (sum of two hasDerivAt product rules, divided by 2); compose with Real.hasDerivAt_exp; multiply by the constant square root. Algebra simplifies the result to $\sqrt{\ell_0(e)},c,e^{tc}$.
Rewrite the line-derivative function in that closed form, then invoke fun_prop to obtain differentiability at $0$.
why it matters
Both parent theorems in this module quote the result as the first component of a pair. hingeDeficitSecondLineDifferentiability_of_deficit packages it with a separate deficit second-derivative hypothesis; hingeDeficitSecondLineDifferentiabilityAtZero_of_flatConfiguration does the same under a flat-configuration assumption. Those targets are exactly the analytic input needed so that the second chain-rule calculation yields ReggeActionSecondVariationInput and identifies the nonlinear directional Hessian with the canonical incidence form.
The module doc is explicit: once that calculation is supplied, the existing second-variation interface follows immediately. The lemma is pure discrete-geometry bookkeeping inside the Regge stack; it does not invoke the J-cost, the forcing chain T5–T8, or the phi ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.