hingeLineDeriv
plain-language theorem explainer
Conformal hinge-length derivative along the ray through the flat vertex potential in direction ξ. Cited by anyone assembling the product rule for the nonlinear Regge action along a conformal line. Defined as the ordinary one-variable derivative of the conformal edge length under the line potential; no closed-form evaluation is claimed here.
Claim. For a 3D triangulation $K$ with consistent incidence, vertex potential $\xi$, edge $e$, and parameter $t\in\mathbb{R}$, the hinge-line derivative is $\frac{d}{ds}\big|_{s=t}\ell_e(s\xi)$, where $\ell_e(\eta)=\sqrt{g_e}\,\exp((\eta_u+\eta_v)/2)$ is the conformal hinge measure (edge length) under the vertex-conformal ansatz.
background
In 3D Regge calculus the action sums hinge measure times deficit angle over edges. Under the vertex-conformal ansatz the hinge measure on edge $e$ with endpoints $u,v$ is $\ell_e(\xi)=\sqrt{g_e},\exp((\xi_u+\xi_v)/2)$, with $g_e$ the background squared length from the incidence data.
The line potential through the flat configuration in direction $\xi$ is $s\mapsto s\xi$. Differentiating the action along this line requires differentiating both the measure factor and the deficit factor; this definition isolates the measure factor as a one-variable real function of the line parameter.
The surrounding module isolates the remaining hard calculation for the full nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. Once that chain-rule work is supplied, the existing second-variation input package follows immediately.
proof idea
Pure definition, not a proved claim. It packages $$\mathrm{deriv}\bigl(s\mapsto \ell_e(s\xi)\bigr)(t)$$ so later lemmas can name the object, prove differentiability at $t=0$, identify its value at zero with the first-variation directional hinge-measure derivative, and form the second derivative by differentiating once more.
why it matters
Feeds the product-rule analysis of the action derivative near zero, the second-line differentiability target at the flat point, the identification of the value at zero with the first-variation directional derivative, and the definition of the second hinge-length derivative along the line. Those objects are intermediate steps toward proving that the nonlinear directional Hessian equals the canonical incidence Hessian, the module endpoint.
In the Recognition Science geometry layer this closes part of the second-variation chain for the Regge action under conformal deformations. That discrete curvature analysis sits in the $D=3$ spatial setting forced by the T8 step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.