actionDerivativeProductRuleNearZero_of_factorDifferentiability
plain-language theorem explainer
On an incidence-consistent 3D triangulation, if hinge measures and deficit angles are differentiable along every potential line near the flat point, the derivative of the Regge action equals the finite product-rule sum over edges. Cited by anyone closing the nonlinear Regge Hessian chain. Proof applies the real product rule edgewise, then sums with HasDerivAt.sum.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Suppose that for every vertex potential $\xi$, both the conformal hinge measure $L_e$ and the deficit angle $\delta_e$ along the line through $\xi$ are differentiable for all sufficiently small $t$. Then near $t=0$, $\frac{d}{dt}\mathrm{Action}_K(\xi_t)=\sum_e\bigl(L_e'(\xi_t)\,\delta_e(\xi_t)+L_e(\xi_t)\,\delta_e'(\xi_t)\bigr)$.
background
This module isolates the hard second-variation calculation for the nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. The Regge action along a line is the sum over edges of hinge measure times deficit angle under a conformal deformation of the vertex potential.
The product-rule target asserts that, near the flat point $t=0$, the derivative of that action equals the finite sum of hinge-derivative and deficit-derivative cross terms. The hypothesis supplies exactly the differentiability needed: for every direction $\xi$ and every edge $e$, both the hinge-measure line and the deficit-angle line are differentiable in a neighborhood of zero.
Upstream arithmetic (associativity and commutativity of multiplication) is used only to normalize the product-rule identity; the geometric content sits in the hinge and deficit factorizations already defined in the Regge-action concrete layer.
proof idea
Fix a direction $\xi$. Filter upwards from the differentiability hypothesis so that at the chosen $t$ near zero every edge factor is differentiable. For each edge, obtain HasDerivAt of the hinge line and of the deficit line, then apply the real product rule (HasDerivAt.mul), rewriting with mul_comm/mul_assoc to match the target cross-term shape.
Sum those edgewise derivative certificates with HasDerivAt.sum over the finite edge universe. A short funext/simp rewrites the summed function so that the sum sits outside the parameter, then HasDerivAt.deriv yields the claimed eventual equality of the action derivative with the product-rule expression.
why it matters
This is the pure calculus step that turns factorwise differentiability into the product-rule form of the first action derivative. The immediate parent is actionDerivativeProductRuleNearZero_of_flatConfiguration, which discharges the differentiability hypothesis from a flat-configuration assumption and thereby obtains the product-rule target unconditionally on flat backgrounds.
That parent sits on the path to the nonlinear directional Hessian equaling the canonical incidence Hessian (the module's stated endpoint). Once the product rule and the subsequent linearization/tangency targets are in hand, ReggeActionSecondVariationInput follows and the second-variation chain closes. No new physical assumption is introduced; the theorem is the exact finite-sum product rule needed for the Regge action on a triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.