deficitDeriv
plain-language theorem explainer
Closed-form first derivative of the Regge deficit on edge e along a plane-wave amplitude path: minus the sum over all periodic tetrahedra of the matched dihedral-angle contributions. Gravity and discrete-geometry workers cite it when writing the first variation of the Regge action and when killing the √ℓ·δ' term via Schläfli. The body is a one-line sum of the already-defined contribution derivatives.
Claim. For a $3\times 3$ edge-length matrix $E$, wavevector $k$, periodic edge $e$, and amplitude parameter $t\in\mathbb{R}$, the deficit derivative is $\delta'_e(t)=-\sum_{\tau}\theta'_{\tau,f(e)}(t)$, where the sum runs over all periodic tetrahedra $\tau$ and each summand is the directional derivative of the dihedral angle in the local slot matched to $e$.
background
This module sits in the Regge TT continuum-symbol program (Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol). The ambient setting is a periodic cubic lattice with tetrahedra and edges; edge lengths are deformed by a plane-wave amplitude profile with matrix $E$ and wavevector $k$. At each good amplitude $t$ (positive edge values, nondegenerate tets, interior cosines), the Regge action profile $S(t)$ has an explicit first derivative built from edge-sqrt derivatives and deficit derivatives.
The deficit on an edge is $2\pi$ minus the sum of incident dihedral angles. Differentiating under that sum produces one angle derivative per incident tet; those matched contributions are packaged as contribDeriv. The present definition simply negates their total, giving the closed form $\delta'e(t)=-\sum\tau(\text{matched }\theta'_{\tau f}(t))$ quoted in the doc-comment.
Upstream derivative infrastructure (edge values, square-root edge lengths, slot angles) is already available from the derivative-gate and local-symbol modules; this def only assembles the deficit side.
proof idea
Pure definitional abbreviation: negate the finite sum, over all periodic tetrahedra $\tau$, of the contribution derivative of the dihedral angle matched to edge $e$ at amplitude $t$. No tactics, no lemmas applied in the body; the mathematical content lives in the sibling contribution derivative and in later theorems that differentiate under the sum or invoke Schläfli.
why it matters
Gate A2 needs an explicit $\delta'_e$ inside $S'(t)=\sum_e\bigl[(l'_e/(2\sqrt{l_e}))\cdot\delta_e+\sqrt{l_e}\cdot\delta'_e\bigr]$. The second group is killed pathwise by the tetrahedral Schläfli identity once deficits are written this way, so no second derivative of $\arccos$ enters the flat second variation. Downstream, the same closed form seeds the directional deficit package used for the first-variation formula and for mixed-hinge Hessian targets (canonical Hessian, Dirichlet form, edge stencil). In the broader RS gravity lane this is the discrete curvature derivative that lets the flat TT second variation reduce to a pure first-jet angle Jacobian contraction at $t=0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.