contribDeriv
plain-language theorem explainer
The edge–tetrahedron angle contribution derivative equals the closed-form slot angle derivative when the periodic edge occupies a local slot of the tet, and zero otherwise. Anyone building the first variation of the Regge action along a plane-wave path cites this as the incidence filter inside the deficit derivative. The body is a single match on the canonical edge–slot lookup.
Claim. Fix a polarization $E$, wavevector $k$, periodic edge $e$, periodic Freudenthal tetrahedron $\tau$, and amplitude $t\in\mathbb{R}$. If $e$ matches local slot $f$ of $\tau$ under the canonical edge–slot map, the contribution derivative is the closed-form slot angle derivative $\theta'_{\tau f}(t)=\sum_g v_{\tau g}\,\partial\theta_f/\partial a_g$ at the plane-wave squared-edge lengths; otherwise it is $0$.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program. The setting is a periodic Freudenthal triangulation of the $N\times N\times N$ torus: edges are positive-displacement periodic edges, and tetrahedra are the six Freudenthal tets in each cubic cell. Edge lengths are driven by a plane-wave field with polarization $E$ and wavevector $k$, parameterized by a real amplitude $t$.
A deficit on an edge is $2\pi$ minus the sum of dihedral angles of incident tets. Differentiating that sum needs an incidence filter: only tets that actually contain the edge contribute. The canonical edge–slot lookup returns some f when $e$ is the $f$-th local edge of $\tau$, else none. The sibling slot angle derivative is the chain-rule contraction $\theta'{\tau f}(t)=\sum_g v{\tau g}\cdot(\partial\theta_f/\partial a_g)$ along the plane-wave path, with $v$ the tet edge velocities.
The first-derivative structure at flat is already proved in the derivative gate and is reused here, never re-proved. Good amplitudes require positive edge values and nondegenerate tets with interior cosines.
proof idea
Pure definition by cases. Evaluate the optional canonical edge–slot lookup of $e$ against the cell and tet index of $\tau$. On some f, return the already-defined closed-form slot angle derivative at $(E,k,\tau,f,t)$. On none, return the constant $0$. No tactics and no lemmas beyond that lookup and the slot derivative.
why it matters
This is the incidence-filtered atom of every deficit derivative in the module. The deficit derivative is defined as $\delta'e(t)=-\sum\tau$ (this contribution), so the match/none split is exactly which tets hit edge $e$. Downstream, hasDerivAt_contrib and hasDerivAt_deficit justify differentiating under that sum at good amplitudes.
The pathwise Schläfli kill (sum_sqrt_deficitDeriv_eq_zero) rewrites $\sum_e\sqrt{l_e},\delta'_e$ as a sum of per-tet Schläfli contractions and shows it vanishes identically on the good neighborhood of flat; that identity is what deletes every arccos second derivative from the second variation. The flat regrouping sum_edgeSqrtDeriv_deficitDeriv_flat and Gates A2(a)–(b) (first variation zero at flat; Schläfli-reduced second variation) all thread through this contribution. In the QG campaign this is scaffolding for Crux-1(c), not a T0–T8 landmark, but it is the local incidence step that makes the Schläfli reduction machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.