weightedDeficitDerivativeStationary_of_eventuallyZero
plain-language theorem explainer
If the weighted deficit-derivative sum along every conformal line is eventually zero near the flat point, then that sum is stationary there (derivative zero at t=0). Cited by second-variation and Schläfli-bridge lemmas that need the stationary form of the second-order Schläfli target. Proof: congruence of HasDerivAt with the constant-zero derivative via eventuallyEq.
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 h_e(t)\,\delta'_e(t)$ (hinge measure times deficit line-derivative along the conformal line through $\xi$) is eventually equal to the zero function in a neighbourhood of $t=0$. Then for every $\xi$ that map has derivative $0$ at $t=0$.
background
This module isolates the hard endpoint of the nonlinear Regge second variation: the second directional derivative of the action at the flat potential must match the canonical incidence Hessian. Intermediate targets package pieces of that chain-rule calculation as Props.
WeightedDeficitDerivativeEventuallyZeroTarget asserts a strong near-flat Schläfli form: for every vertex potential $\xi$, the weighted sum $\sum_e h_e(t),\delta'_e(t)$ along the conformal line equals zero eventually in a puncture-free neighbourhood of the flat point $t=0$. WeightedDeficitDerivativeStationaryTarget is the weaker stationarity form needed downstream: that same sum has derivative zero at $t=0$ (i.e. HasDerivAt with value $0$).
Classically, Schläfli gives $\sum_{e\in\tau}\ell_e,d\theta_{e,\tau}=0$ per tetrahedron; summed over the complex this cancels the $\sum h\delta'$ contribution in the first variation, leaving $V(t)=\sum h\delta'=0$. The eventually-zero target is the analytic packaging of that cancellation near flatness.
proof idea
Term-mode, one short argument per potential $\xi$. The constant function $t\mapsto 0$ has derivative $0$ at $0$ by hasDerivAt_const. The hypothesis supplies EventuallyEq of the weighted deficit-derivative sum with that constant zero function in a neighbourhood of $0$. HasDerivAt.congr_of_eventuallyEq transfers the derivative, yielding stationarity at the flat point. No triangulation geometry is reopened; the step is pure real calculus on the already-formed scalar sum.
why it matters
Closes the gap from the strong near-flat Schläfli cancellation to the stationary target that second-variation consumers actually call. Downstream: secondProductRuleEqualsCanonicalHessian_of_eventuallyZero_and_edgeStencil feeds the eventually-zero hypothesis into the product-rule equals canonical Hessian path; weightedDeficitDerivativeStationary_of_conformalSchlaefliAlongLine and weightedDeficitDerivativeStationary_of_nearZeroExpansion_and_local reduce stronger geometric Schläfli packages to stationarity by routing through this lemma; the gravity instance canonicalPeriodicWeightedDeficitDerivativeStationaryTarget_of_eventuallyZero lifts the same pattern to the six-tet cubic Dirichlet setting.
In the module's program this is not a new physical assumption: it is the calculus bridge that lets a proved eventually-zero Schläfli identity discharge WeightedDeficitDerivativeStationaryTarget and thereby unlock the nonlinear directional Hessian equals canonical incidence Hessian endpoint. Framework-wise it sits in the Regge geometry layer supporting discrete curvature and the path toward the forced $D=3$ spatial structure, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.