weightedDeficitDerivative_hasDerivAt_secondSchlaefliSum
plain-language theorem explainer
At a flat, incidence-consistent 3D triangulation, the edge-sum of hinge measure times deficit first derivative along a conformal line of vertex potentials is differentiable at the origin, with derivative equal to the product-rule sum of hinge first derivatives and deficit second derivatives. Cited by anyone equating weighted-deficit stationarity to the second Schläfli identity along the line. Proof: product rule edgewise from flat second-line differentiability, then sum over edges.
Claim. Let $K$ be an incidence-consistent 3D triangulation in a flat configuration, and let $\xi$ be a vertex potential. The map $t\mapsto\sum_e m_e(\phi_{t\xi})\,\partial_t\delta_e(t)$ is differentiable at $t=0$, and its derivative equals $\sum_e\bigl(m_e'(0)\,\partial_t\delta_e(0)+m_e(\phi_0)\,\partial_t^2\delta_e(0)\bigr)$, where $m_e$ is hinge measure under the conformal deformation along $\xi$ and $\delta_e$ is the deficit along that line.
background
The module isolates the remaining hard calculation for the full nonlinear Regge action: the second directional derivative at a flat potential must equal the canonical incidence Hessian. Once that chain-rule identity is in hand, the existing second-variation input package follows immediately.
In Regge calculus, curvature is concentrated on hinges. The deficit angle measures the failure of the link to close flatly; the hinge measure weights that deficit in the discrete action. A conformal line of vertex potentials deforms edge lengths by exponential scaling from a base configuration. The weighted deficit derivative is the first variation of the action along that line, written as an edge sum of hinge measure times deficit first derivative.
Flatness supplies the smoothness needed at the origin: both hinge measures and deficit derivatives are twice differentiable along the line at $t=0$, which is the content of the upstream second-line differentiability result used here.
proof idea
Start from second-line differentiability of hinge-deficit pairs at zero under the flat configuration. For each edge, obtain HasDerivAt of the product (hinge measure along the conformal line) times (deficit first derivative) by the product rule: ContDiffAt of the hinge line gives differentiability of the measure with derivative the hinge line derivative, and the deficit first derivative is differentiable with derivative the deficit second derivative. Sum the edgewise derivatives with HasDerivAt.sum. A short funext/sum_apply rewrite identifies the summed function of $t$ with the sum of the edgewise functions, matching the target signature.
why it matters
This identity is the analytic step that equates two target interfaces in the nonlinear Hessian chain: weighted-deficit-derivative stationarity and the second Schläfli identity along the conformal line. The two immediate parents convert each target into the other by instantiating this derivative at $t=0$ for arbitrary vertex potentials.
Closing that equivalence is the remaining piece toward the nonlinear directional Hessian equaling the canonical incidence Hessian, the module's stated endpoint, after which ReggeActionSecondVariationInput follows. In the Recognition geometry stack this pins the second variation of the discrete action at flat space, the discrete counterpart of the Einstein-Hilbert second variation on a triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.