weightedDeficitDerivativeEventuallyZero_of_conformalSchlaefliAlongLine
plain-language theorem explainer
From the global conformal Schläfli identity (weighted hinge-measure times deficit-derivative sum vanishes for every line parameter) one obtains the local near-flat form: the same sum is eventually zero in a neighborhood of the flat point. Anyone reducing the nonlinear Regge second variation to Schläfli cancellation cites this bridge. The proof is a filter argument: identical vanishing implies eventual equality on the whole real line.
Claim. Let $K$ be an incidence-consistent 3D triangulation that is flat. Suppose that for every vertex potential $\xi$ and every real parameter $t$, $\sum_e h_e(\xi_t)\,\delta'_e(\xi_t)=0$, where $h_e$ is the conformal hinge measure and $\delta'_e$ is the deficit derivative along the conformal line through the flat potential in direction $\xi$. Then for every $\xi$ that weighted sum vanishes eventually in a neighborhood of $t=0$.
background
This module isolates the hard second-variation calculation for the nonlinear Regge action: the second directional derivative at the flat potential must equal the canonical incidence Hessian. The endpoint is not a new axiom; once the chain-rule work is in, the existing second-variation input package follows at once.
A conformal line is the one-parameter family of vertex potentials $\xi_t = t,\xi$ through the flat configuration. The hinge measure under the conformal ansatz is the edge length $h_e(\xi)=\sqrt{\ell_e^2},\exp((\xi_u+\xi_v)/2)$. The deficit-line derivative is the ordinary one-variable derivative of the deficit angle along that line.
The hypothesis is the strongest geometric Schläfli form: the weighted sum $\sum_e h_e,\delta'e$ vanishes identically for every $t$, not merely near zero. Classically this is $\sum{e\in\tau}\ell_e,d\theta_{e,\tau}=0$ applied at each tetrahedron and each $t$, which cancels the $\sum h,\delta'$ term in the first variation and forces $V(t)=\sum h,\delta'=0$. The conclusion weakens that identity to an eventual-equality statement in the filter of neighborhoods of the flat point $t=0$.
proof idea
Fix a direction $\xi$. The hypothesis supplies, for every $t$, that the weighted sum equals zero. By function extensionality the map $t\mapsto\sum_e h_e(\xi_t),\delta'_e(\xi_t)$ is the zero function on all of $\mathbb{R}$. Eventual equality in the neighborhood filter of $0$ is then immediate: take the whole real line as the witnessing neighborhood (it belongs to every neighborhood filter) and the identity holds pointwise. No differentiation or local expansion is used; the argument is pure filter bookkeeping from global vanishing to local vanishing.
why it matters
The immediate parent is the stationary form of the same weighted sum: once the sum is eventually zero near the flat point, it is stationary there, which is the input needed for the nonlinear directional Hessian theorems in this module. Those theorems close the second chain-rule calculation that equates the second directional derivative of the Regge action at the flat potential with the canonical incidence Hessian.
In the broader Recognition geometry stack this is the Schläfli cancellation step that lets the first-variation remainder drop out, leaving only the hinge-length derivatives that feed the quadratic Hessian form. It sits downstream of the classical Schläfli differential identity and upstream of the full nonlinear Regge second-variation package. No open scaffolding remains on this arrow: the claim is proved and only packages a filter weakening of an already-assumed global identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.