hingeDeficitSecondLineDifferentiabilityAtZero_of_flatConfiguration
plain-language theorem explainer
On any incidence-consistent 3D triangulation that is flat, both the hinge-measure line derivative and the deficit line derivative are differentiable at the zero conformal parameter, for every vertex potential and every edge. Geometric analysts working the second variation of nonlinear Regge action cite this as the product-rule differentiability gate at the flat point. The proof is a one-line packaging of two prior differentiability lemmas.
Claim. Let $K$ be a 3D triangulation with consistent incidence, and suppose $K$ admits a flat analytic configuration. Then for every vertex potential $\xi$ and every edge $e$, the maps $t \mapsto$ (hinge-measure line derivative of $\xi$ at $e$ along $t$) and $t \mapsto$ (deficit line derivative of $\xi$ at $e$ along $t$) are both differentiable at $t = 0$.
background
The module isolates the hard second-chain-rule step for the nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. Once that calculation is in place, the existing second-variation input interface follows immediately.
A flat configuration packages three facts: arccos endpoints stay off ${\pm 1}$ at the base point, all hinge deficits vanish (flatness), and the nonlinear action is smooth enough for Taylor theory. The target proposition here is the sufficient differentiability condition needed to differentiate the product-rule expression once more at that flat point: for every potential $\xi$ and edge $e$, both the hinge line derivative and the deficit line derivative must be differentiable at $t=0$.
Upstream, hinge-line differentiability at zero is already proved without flatness (by unfolding the conformal hinge measure and the line potential). Deficit-line differentiability at zero needs the flat configuration and is supplied by a sibling lemma that unfolds the deficit line derivative under that hypothesis.
proof idea
Term-mode packaging. Introduce an arbitrary vertex potential $\xi$ and edge $e$. Return the pair of facts:
hingeLineDeriv_differentiableAt_zero(always true on an incidence-consistent triangulation),deficitLineDeriv_differentiableAt_zero_of_flatConfiguration(uses the flat-configuration hypothesis).
No further calculation: the target is definitionally the universal quantification of that conjunction.
why it matters
This lemma is the differentiability gate for the product-rule second derivative of the nonlinear Regge action at the flat point. Downstream it feeds weightedDeficitDerivative_hasDerivAt_secondSchlaefliSum (HasDerivAt for the weighted deficit derivative as a second-Schläfli sum) and productRuleDerivativeCanonicalHessian_of_flat_secondProduct (product-rule derivative equals the canonical incidence Hessian once the second-product identity is known).
It also lands in the physical six-tetrahedron cubic Dirichlet instance, where the same gate discharges HasDerivAt statements for the canonical periodic disp0 and disp-$d$ weighted deficit-derivative base sums at $N=5$. In the Recognition geometry stack this is part of closing the nonlinear Hessian identification that underwrites discrete curvature second variation in $D=3$ (forcing-chain T8), not a new physical assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.