hasDerivAt_deficit
plain-language theorem explainer
At every good amplitude, the Regge deficit of a fixed periodic edge along a plane-wave edge-length path is differentiable, with derivative equal to the explicit closed form deficitDeriv. Anyone assembling the first variation of the plane-wave Regge action cites this edgewise fact. The proof sums the per-tetrahedron angle-contribution derivatives and subtracts the constant 2π.
Claim. Fix a polarization matrix $E$, wavevector $k$, periodic edge $e$, and amplitude $t_0$ at which the path is good (all edge lengths positive; every tetrahedron nondegenerate with strictly interior dihedral cosines). Then $t \mapsto \delta_e\bigl(\ell(t)\bigr)$ is differentiable at $t_0$, and its derivative equals the explicit formula $\delta'_e(t_0)$ obtained by summing the closed-form angle-contribution derivatives over incident tetrahedra.
background
This module sits in Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol for the Regge TT continuum symbol: first-derivative structure at flat is imported from the derivative gate and never re-proved. The ambient geometry is the periodic Freudenthal torus: edges are positive-displacement periodic edges (base vertex plus one of seven cube displacements); tetrahedra are the six Freudenthal tets per cubic cell.
A plane-wave edge field $\ell(t)=\mathrm{planeWaveEdgeField}(E,k,t)$ deforms squared edge lengths by a polarized monochromatic mode. The goodness predicate PathGoodAt requires every edge value positive and, for every tet, positive Cayley–Menger volume proxy together with dihedral cosines strictly in $(-1,1)$. Under that hypothesis each local edge-angle contribution is differentiable.
The deficit of an edge is the usual Regge quantity $2\pi$ minus the sum of dihedral angle contributions from all incident tetrahedra. The sibling deficitDeriv packages the corresponding sum of contribution derivatives; contribDeriv is the per-tet summand already shown differentiable by hasDerivAt_contrib.
proof idea
For every periodic tetrahedron $\tau$, apply hasDerivAt_contrib at $(e,\tau,t_0)$, feeding the positivity and interior-cosine witnesses extracted from hgood. The family of contribution maps is therefore differentiable termwise with derivatives contribDeriv.
HasDerivAt.fun_sum lifts that to differentiability of the finite sum over all tets. Subtract the constant $2\pi$ via HasDerivAt.const_sub. Unfolding deficitOfField and deficitDeriv identifies the resulting derivative with the claimed closed form, so the goal follows.
why it matters
Edgewise deficit differentiability is the missing local input to the profile derivative theorem hasDerivAt_planeWaveActionProfile, which writes $S'(t)=\sum_e\bigl[(l'_e/(2\sqrt{l_e}))\delta_e+\sqrt{l_e},\delta'_e\bigr]$ in closed form at every good amplitude. That identity is what lets the pathwise Schläfli kill delete the entire $\sum_e\sqrt{l_e},\delta'_e$ group near flat and clear Gate A2(a)–(b) (vanishing first variation and arccos-free second variation at $t=0$).
It is also reused by hasDerivAt_reducedFirstVariation_flat, where only the $L'_e(0)\cdot\delta'_e(0)$ product survives once flat deficits vanish. In the broader Recognition gravity lane this is pure continuum-Regge analysis on the eight-tick / $D=3$ lattice geometry, not a new forcing-chain step; it closes the derivative gate needed before the TT symbol can be read off the two-jet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.