secondSchlaefliAlongLine_of_weightedStationary
plain-language theorem explainer
On a flat, incidence-consistent 3D triangulation, stationarity of the weighted deficit-derivative sum along every conformal line implies the second-order Schläfli identity along that line. Discrete-gravity and Regge-calculus workers cite it to convert a first-derivative vanishing hypothesis into the mixed hinge/deficit cancellation needed for the nonlinear Hessian. The proof is a short uniqueness argument from the already-established HasDerivAt calculation.
Claim. Let $K$ be an incidence-consistent 3D triangulation that is flat. Suppose that for every vertex potential $\xi$, the map $t \mapsto \sum_e \mu_e(\gamma_\xi(t))\,\partial_t\delta_e(\gamma_\xi(t))$ has derivative zero at $t=0$. Then for every such $\xi$, $\sum_e\bigl(\partial_t\mu_e\,\partial_t\delta_e + \mu_e\,\partial_t^2\delta_e\bigr)$ evaluated at $t=0$ vanishes.
background
This module isolates the hard second-variation calculation for the nonlinear Regge action: the second directional derivative of the action at a flat potential must equal the canonical incidence Hessian. The endpoint is not a new axiom; it is the chain-rule identity that, once proved, discharges ReggeActionSecondVariationInput.
A conformal line is the one-parameter family of edge lengths obtained by flowing a vertex potential $\xi$ through the exponential (conformal) deformation. Hinge measures $\mu_e$ and deficit angles $\delta_e$ are evaluated along that line. Flatness means all deficits vanish at $t=0$, which kills the pure deficit term in the second product rule.
WeightedDeficitDerivativeStationaryTarget asserts that the first $t$-derivative of $\sum_e \mu_e\partial_t\delta_e$ vanishes at the flat point. SecondSchlaefliAlongLineTarget is the algebraic identity that cancels one mixed hinge/deficit derivative against the length-weighted second deficit derivative. Upstream, weightedDeficitDerivative_hasDerivAt_secondSchlaefliSum already identifies the derivative of that weighted sum with the second-Schläfli expression.
proof idea
Term-mode proof, five lines. Fix an arbitrary vertex potential $\xi$. Invoke weightedDeficitDerivative_hasDerivAt_secondSchlaefliSum to obtain a HasDerivAt witness whose derivative value is exactly the second-Schläfli sum along the line. The stationarity hypothesis supplies another HasDerivAt witness for the same function with derivative value $0$. Uniqueness of derivatives forces the second-Schläfli sum to equal zero. A final simpa closes the goal.
why it matters
The result is one direction of the equivalence weightedDeficitDerivativeStationaryTarget_iff_secondSchlaefliAlongLine, and it is the stationarity leg used by secondProductRuleEqualsCanonicalHessian_of_weightedStationary_and_edgeStencil. That parent theorem, together with the eventually-zero variant, is the bridge from local geometric hypotheses to equality of the second product-rule expansion with the canonical incidence Hessian.
In the Recognition geometry stack this is the discrete Schläfli cancellation that lets the nonlinear Regge Hessian reduce to the incidence form already controlled by the forcing chain (T8 forces $D=3$, matching the triangulation dimension). Once both stationarity (or eventual vanishing) and the edge-stencil hypothesis are in hand, the module's stated endpoint follows and the second-variation input package closes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.