sum_sqrt_slotAngleDeriv_eq_zero
plain-language theorem explainer
On any nondegenerate tetrahedron along a plane-wave edge path, the weighted sum of slot angle derivatives vanishes: Σ_f √a_f(t)·θ'_τf(t) = 0. Anyone proving the pathwise Schläfli kill or Gate A2 second-variation reduction cites this. The proof expands each angle derivative in edge velocities, swaps sums, and applies the closed-form tetrahedral Schläfli identity in every coordinate direction.
Claim. Fix a plane-wave edge field with amplitude matrix $E$ and wavevector $k$, a periodic tetrahedron $\tau$, and a time $t$. If all six squared edge lengths $a_f(t)$ of $\tau$ are positive and the Cayley–Menger determinant is positive, then $\sum_{f=1}^{6} \sqrt{a_f(t)}\,\partial_t\theta_{\tau f}(t)=0$, where $\theta_{\tau f}$ is the dihedral angle opposite slot $f$.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program. The action profile along a plane-wave edge deformation has first derivative $S'(t)=\sum_e\bigl[(l'_e/(2\sqrt{l_e}))\delta_e+\sqrt{l_e},\delta'_e\bigr]$ at every good amplitude (positive edges, nondegenerate tets with interior cosines). The second group is the obstacle: it appears to bring second derivatives of arccos through the angle jets.
Per tetrahedron the six squared edge lengths $a=\mathrm{tetSqEdgesOfField}$ determine the closed-form dihedral angles. The slot angle derivative $\theta'_{\tau f}(t)$ is the chain-rule contraction of the plane-wave tet edge velocities against the Jacobian of those angles. The classical Schläfli identity for a tetrahedron asserts $\sum_f\sqrt{a_f},\partial\theta_f/\partial a_g=0$ in every edge-coordinate direction $g$; that identity is already proved as tetraSchlaefliSixEdgeClosedForm and is invoked here pointwise on the path, not only at flat.
proof idea
Set $a$ to the six squared edges of $\tau$ at time $t$. The closed-form Schläfli lemma gives, for each coordinate $g$, $\sum_f\sqrt{a_f},\partial\theta_f/\partial a_g=0$. Unfold the definition of the slot angle derivative: it is $\sum_g v_g,\partial\theta_f/\partial a_g$ with $v$ the plane-wave tet velocity. Substitute, distribute $\sqrt{a_f}$, swap the finite double sum over slots $f$ and coordinates $g$, and factor. Each inner $f$-sum is zero by Schläfli, so the outer sum collapses by mul_zero. The argument is pure finite-sum algebra once Schläfli is in hand; no calculus beyond the already-established angle Jacobian is used.
why it matters
This is the per-tetrahedron engine of the pathwise Schläfli kill. Downstream, sum_sqrt_deficitDeriv_eq_zero regroups the global edge sum $\sum_e\sqrt{l_e},\delta'_e$ into a sum of these per-tet contractions and concludes the whole second group vanishes identically on the good neighborhood of flat. That deletion is what removes every arccos second derivative from the second variation of the true Regge action.
Gate A2(a) (first variation at flat equals zero) and Gate A2(b) (second variation reduces to $-\sum_\tau\sum_f L'{\tau f}(0),\theta'{\tau f}(0)$ with only first angle jets) both depend on this kill. In the broader QG campaign it is the algebraic reason the continuum TT symbol can be read off from the flat angle Jacobian alone, without residual curvature-of-angle terms. It sits downstream of the derivative gate and local symbol existence, and does not itself touch the forcing chain T0–T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.