WeightedDeficitDerivativeEventuallyZeroTarget
plain-language theorem explainer
For any conformal line through a flat 3D Regge configuration, the edge-sum of hinge measure times deficit-angle derivative is identically zero in a neighborhood of the origin. Analysts proving the nonlinear Regge Hessian and local J-cost correspondence cite this Prop as the strong near-flat Schläfli cancellation target. It is a pure definition packaging that eventual-equality statement.
Claim. Given a 3D triangulation $K$ with consistent incidence and a flat configuration, the target asserts: for every vertex potential direction $\xi$, the real function $t \mapsto \sum_e \ell_e(t\xi)\,\partial_t\delta_e(t\xi)$ is eventually equal (in a neighborhood of $t=0$) to the zero function, where $\ell_e$ is the conformal hinge measure (edge length under the vertex-conformal ansatz) and $\delta_e$ is the deficit angle along the line $t\mapsto t\xi$.
background
The module isolates the hard second-variation calculation for the full nonlinear Regge action: the second directional derivative of the action at the flat potential must match the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
A conformal line through the flat point is the path of vertex potentials $t\mapsto t\xi$. Along it, each edge carries a hinge measure equal to the conformal edge length $\sqrt{q_e},\exp((\xi_u+\xi_v)/2)$, and a deficit angle whose $t$-derivative is written as a one-variable derivative. The classical Schläfli identity says the weighted sum of those deficit derivatives vanishes; the present target asks for the same cancellation in a whole puncture-free neighborhood of $t=0$, not merely at the single flat point.
Upstream ingredients are exactly those pieces: the conformal hinge measure, the line potential, and the deficit line derivative. Flatness of the background configuration is recorded as a hypothesis so that the neighborhood is taken about a genuine zero-curvature base point.
proof idea
No proof: the declaration is a Prop-valued definition. It packages the filter statement that, for every direction $\xi$, the weighted deficit-derivative sum along the conformal line is eventually equal to the zero function in the neighborhood filter of $0\in\mathbb{R}$. Downstream theorems treat the resulting Prop as a named hypothesis to be discharged by a near-zero Schläfli cancellation argument.
why it matters
This target is the strong near-flat Schläfli form that the conformal-line calculation naturally produces. It is strictly more than a pure second-order Hessian identity needs, yet it is the clean interface used throughout the nonlinear chain.
Downstream, it feeds the local Hessian Taylor-input constructors, the nonlinear local correspondence theorem, the strongest true Regge-to-J-cost replacement, action-derivative tangency to the canonical quadratic, the product-rule form of the canonical Hessian, and the directional nonlinear Hessian itself. In the Recognition geometry stack those results close the gap between discrete Regge curvature and the continuum J-cost Hessian that sits behind the forcing chain (T5 J-uniqueness and the RCL). The module doc frames the whole file as the exact endpoint of the second chain-rule calculation rather than a new physical assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.