hingeLineSecondDeriv
plain-language theorem explainer
Defines the second derivative of conformal hinge length along a fixed conformal line in an incidence-consistent 3D triangulation, as the ordinary one-variable derivative of the first hinge-line derivative. Anyone assembling the nonlinear Regge product-rule Hessian cites this quantity. The body is a one-line wrapper around Mathlib's deriv applied to the first hinge-line derivative.
Claim. For an incidence-consistent 3D triangulation $K$, a vertex potential $\xi$, an edge $e$, and a real parameter $t$, write $\ell_e(s)$ for the conformal hinge measure of $e$ under the line potential of $\xi$ at scale $s$. The second hinge-line derivative at $t$ is $$\frac{d}{ds}\Big|_{s=t}\Bigl(\frac{d}{du}\Big|_{u=s}\ell_e(u)\Bigr).$$
background
The module isolates the remaining hard step for the full nonlinear Regge action: the second directional derivative of the action at the flat potential must match the canonical incidence Hessian. Once that chain-rule calculation is in place, the existing second-variation input package follows immediately.
A conformal line is the one-parameter family of vertex potentials obtained by scaling a fixed potential $\xi$ by a real parameter $s$. Along that line one tracks two geometric quantities per edge $e$: the conformal hinge measure (length/area factor of the hinge) and the angular deficit $2\pi - \sum\theta$ at that hinge. The first hinge-line derivative is already defined as the ordinary derivative of the hinge measure under the line potential; the present definition simply differentiates that map once more in the line parameter.
Upstream, the deficit-line derivative is the parallel construction for the deficit angle. Both enter the product rule for the Regge action, which is a sum over edges of (hinge measure)$\times$(deficit).
proof idea
Pure definitional wrapper: apply Mathlib's one-variable deriv to the already-defined first hinge-line derivative, evaluated at the real parameter $t$. No geometric content is computed here; the remaining cofactor and arccos work is deferred to targets that expand this expression near the flat point.
why it matters
This quantity is the second-derivative factor in the product-rule expansion of the nonlinear Regge action along a conformal line. It is summed, edgewise, against the deficit (and paired with the mixed first-derivative term) inside the second product-rule derivative. That expression is then the left-hand side of the theorem equating the second product rule to the canonical incidence Hessian, once second Schläfli and mixed hinge-deficit targets are supplied.
In the Recognition geometry stack this closes the analytic half of the continuum bridge from discrete Regge data to a quadratic form comparable with the Laplacian action on the simplicial ledger. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is pure 3D Regge calculus scaffolding for the Hessian identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.