weightedDeficitDerivativeStationary_of_secondSchlaefliAlongLine
plain-language theorem explainer
From the second-order Schläfli identity along a conformal line at a flat configuration, the length-weighted sum of deficit first derivatives is stationary at the flat point. Anyone wiring the nonlinear Regge Hessian chain cites this one-way bridge between the two target Props. The proof rewrites an already-computed HasDerivAt identity against the Schläfli cancellation sum.
Claim. Let $K$ be an incidence-consistent 3D triangulation equipped with a flat analytic configuration. Suppose that for every vertex potential $\xi$, the second-order Schläfli sum along the conformal line vanishes at the flat point: $\sum_e\bigl(\ell_e'(0)\,\delta_e'(0)+\ell_e(0)\,\delta_e''(0)\bigr)=0$. Then for every such $\xi$, the map $t\mapsto\sum_e \ell_e(t)\,\delta_e'(t)$ has derivative zero at $t=0$.
background
This module isolates the remaining hard calculation for the full nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. The endpoint is not a new physical assumption; it is the exact close of a second chain-rule calculation that, once supplied, discharges ReggeActionSecondVariationInput.
A flat configuration packages three facts: arccos endpoints stay off ${\pm 1}$, all deficit angles vanish at the base point, and the nonlinear action is smooth enough for Taylor theory. Conformal lines are one-parameter families of vertex potentials $t\mapsto$ linePotential$(\xi,t)$ through that flat base.
Two target Props sit on that line. The second-order Schläfli target asserts that, after flatness kills the bare deficit term in the product rule, the mixed hinge/deficit first-derivative sum cancels the length-weighted second deficit derivative. The weighted-deficit stationarity target asks instead that $t\mapsto\sum_e\ell_e(t),\delta_e'(t)$ have vanishing derivative at $t=0$. An upstream lemma already computes that derivative and identifies it with the Schläfli sum.
proof idea
Short term-mode proof. Fix an arbitrary vertex potential $\xi$. Invoke weightedDeficitDerivative_hasDerivAt_secondSchlaefliSum, which supplies
HasDerivAt (t ↦ ∑_e ℓ_e(t) δ'_e(t)) (Schläfli-sum(ξ)) 0.
Rewrite the derivative value by the hypothesis SecondSchlaefliAlongLineTarget at $\xi$, which forces that sum to zero. The rewritten HasDerivAt is exactly the stationarity target at $\xi$.
why it matters
This is one half of the local equivalence
weightedDeficitDerivativeStationaryTarget_iff_secondSchlaefliAlongLine,
which the same module immediately assembles with the converse direction. That equivalence lets the nonlinear Hessian proof speak in whichever language is convenient: classical Schläfli cancellation along the conformal line, or stationarity of the weighted deficit-derivative sum at the flat point.
In the broader Recognition geometry stack this sits inside the second-variation chain that must match the canonical incidence Hessian at flat configurations. Closing that match is the module's stated endpoint for the full nonlinear Regge action. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; those enter only when the geometric Hessian is later tied to the RS action and constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.