deficitLineSecondDeriv
plain-language theorem explainer
Defines the second derivative of a hinge deficit angle along a fixed conformal deformation of vertex potentials, as the ordinary derivative of the first-line deficit derivative. Geometry and Regge-calculus arguments cite it when assembling the second product rule for the nonlinear Regge action. The body is a one-line wrapper around Mathlib `deriv`.
Claim. For a 3D triangulation $K$, a vertex potential $\xi$, an edge $e$, and a real parameter $t$, the second deficit derivative along the conformal line is $\frac{d}{ds}\big|_{s=t}$ of the first deficit-line derivative at $s$.
background
The module isolates the hard second-chain-rule 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.
A conformal line is the one-parameter family of vertex potentials obtained by scaling $\xi$ with a real parameter $t$. Along that path, each edge carries a deficit angle (the angular defect at the hinge). The first deficit-line derivative is the $t$-derivative of that deficit; the present definition is simply its second $t$-derivative.
Downstream product-rule expressions differentiate both hinge lengths and deficits. After flatness kills the bare deficit term at $t=0$, second-order Schläfli identities relate weighted second deficit derivatives to mixed hinge/deficit terms, which is why this scalar appears throughout the Hessian calculation.
proof idea
Pure definitional wrapper: apply Mathlib deriv to the univariate map $s \mapsto$ first deficit-line derivative of edge $e$ at $s$, evaluated at the given $t$. No lemmas are invoked; differentiability obligations are discharged later at use sites that assume or prove HasDerivAt for the first derivative.
why it matters
Feeds the second product-rule derivative of the Regge action (hinge-second times deficit plus hinge-first times deficit-second, summed over edges). That expression is the exact finite-sum form obtained after differentiating hinge and deficit factors along the conformal line.
Parent targets include the product-rule HasDerivAt theorem for the second product, the second-Schläfli-along-line interface (which cancels mixed hinge/deficit terms against length-weighted second deficit derivatives after flatness), and the bridge theorem equating the second product rule to the canonical Hessian once second Schläfli and mixed targets hold. Concrete six-tetrahedron cubic Dirichlet instances reuse the same second-deficit summands for periodic Freudenthal tori.
In the Recognition geometry stack this is bookkeeping for the nonlinear Hessian endpoint, not a new physical assumption: it names the second deficit factor so the chain-rule calculation can be stated edgewise and discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.