deficitAngle_hasDerivAt_from_localAngles
plain-language theorem explainer
Under a conformal line deformation of the vertex potential, the Regge deficit angle at any global edge is differentiable at the flat point t=0. The derivative is the sum of packaged local dihedral-angle derivatives over tetrahedra incident to that edge. First-variation arguments for the nonlinear Regge action cite this to lift local angle derivatives to the global deficit. The proof is a finite sum of local HasDerivAt facts, subtracted from the constant 2π.
Claim. Let $K$ be a 3D triangulation and let $A$ package directional derivatives of all local dihedral angles under the conformal ansatz. For any vertex potential $\eta$ and global edge $e$, the map $t \mapsto \delta_e(\xi_t)$ is differentiable at $t=0$, where $\xi_t$ is the line potential through $\eta$ and $\delta_e$ is the Regge deficit at $e$. The derivative equals the sum, over tetrahedra $\tau$ containing $e$, of the packaged local angle derivatives of $A$ (zero when $e$ misses $\tau$).
background
This module targets the vanishing of the first variation of the full nonlinear Regge action at the flat conformal potential. The geometric route is Schläfli cancellation plus zero deficit; the analytic work records exact derivative statements and the named local inputs until closed-form Schläfli identities are fully expanded.
The Regge deficit at a global edge $e$ is $\delta_e(\xi)=2\pi-\sum_\tau$ local deficit contributions of $\xi$ at $(e,\tau)$. Each local contribution is zero when the edge misses the tetrahedron and otherwise equals the corresponding dihedral angle under the conformal edge-length ansatz. Incidence is read from the triangulation's edge-in-tet map.
A LocalDihedralDirectionalDerivativePackage supplies, for every tetrahedron and local edge slot, a real coefficient angleDeriv together with the fact that the conformal dihedral angle along the line potential through $\eta$ has that derivative at $t=0$. The present theorem assembles those local facts into a derivative for the global deficit.
proof idea
Unfold the deficit as $2\pi$ minus the sum of local contributions, and unfold the claimed derivative as the matching sum of packaged angle derivatives (zero off incidence).
Apply HasDerivAt.sum over the finite set of tetrahedra, feeding the per-tetrahedron lemma that each local contribution is differentiable at $0$ with the packaged derivative. The constant map $t\mapsto 2\pi$ has derivative $0$. Subtract the two HasDerivAt facts, then convert: the function identity is a pointwise simp of the sum, and the derivative identity is a one-line ring normalization.
why it matters
This is the bridge from local dihedral derivatives to the global deficit derivative under the conformal line ansatz. Downstream it is consumed by deficitPackage_of_localAngles, which packages the deficit derivative data needed for the first variation of the Regge action.
In the module's program, the target is vanishing of that first variation at the flat conformal potential via Schläfli cancellation plus zero deficit. Differentiability of the deficit is an indispensable analytic step before the cancellation identity can be applied to the variation. The result sits in the geometry layer that supports discrete curvature and action principles feeding the broader Recognition chain; it does not itself invoke T5–T8 or the RCL, but supplies the 3D hinge calculus those continuum limits presuppose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.