weightedDeficitDerivativeStationaryTarget_iff_secondSchlaefliAlongLine
plain-language theorem explainer
On any incidence-consistent flat 3D triangulation, the stationarity form of the weighted deficit-derivative sum along a conformal line is equivalent to the second-order Schläfli identity along that line. Anyone proving the nonlinear Regge Hessian or specializing to periodic six-tet cubes cites this bridge. The proof is a pure Iff packaging of the two already-proved directions.
Claim. Let $K$ be a 3D triangulation that is incidence-consistent and flat. Then the following are equivalent: (i) for every vertex potential $\xi$, the map $t \mapsto \sum_e \ell_e(t)\,\partial_t\delta_e(t)$ has derivative zero at $t=0$; (ii) for every $\xi$, $\sum_e\bigl(\partial_t\ell_e(0)\,\partial_t\delta_e(0)+\ell_e(0)\,\partial_t^2\delta_e(0)\bigr)=0$, where $\ell_e$ and $\delta_e$ are hinge measure and deficit angle along the conformal line through $\xi$.
background
The module isolates the hard second-variation calculation for the nonlinear Regge action: at a flat potential the second directional derivative must match the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
Two equivalent target propositions are used. The stationarity form asks that the weighted sum $\sum_e \ell_e(t),\partial_t\delta_e(t)$ (hinge measure times deficit-line derivative under the conformal deformation) have vanishing derivative at the flat point $t=0$. The second-order Schläfli form, after flatness kills the bare $\delta_e(0)$ term in the product rule, asserts that the mixed hinge/deficit first derivatives plus the length-weighted second deficit derivatives sum to zero along every conformal line.
Both targets are stated for an arbitrary incidence-consistent triangulation $K$ equipped with a flat configuration; the conformal line is the standard one-parameter family of vertex potentials through a direction $\xi$.
proof idea
Term-mode Iff constructor. The forward direction applies secondSchlaefliAlongLine_of_weightedStationary; the reverse applies weightedDeficitDerivativeStationary_of_secondSchlaefliAlongLine. No new calculation is performed here: the two one-sided lemmas already convert stationarity of the weighted deficit-derivative sum into the second-order Schläfli cancellation and back.
why it matters
This equivalence is the clean interface between the analytic stationarity statement one wants to prove geometrically (differentiate Schläfli cancellation through the conformal line) and the algebraic second-order Schläfli identity needed for the nonlinear Regge Hessian. Downstream, the periodic six-tet cubic Dirichlet instance specializes it to canonicalPeriodicWeightedDeficitDerivativeStationaryTarget_iff_secondSchlaefli, so the same bridge feeds the concrete gravity lattice used for physical checks. In the broader Recognition geometry stack it sits inside the second-variation chain that forces the flat-point Hessian of the Regge action to equal the incidence form, a prerequisite for discrete curvature matching continuum Einstein–Hilbert behaviour on the triangulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.