hasDerivAt_slotAngle
plain-language theorem explainer
Along a plane-wave edge-length path, the dihedral angle at a fixed tetrahedron slot is differentiable at every amplitude where the tet is nondegenerate with interior cosine. The derivative equals the closed-form slot-angle Jacobian contracted against the plane-wave velocity. Cited by anyone assembling the first variation of the Regge action profile. Proof rebases the directional angle-derivative lemma onto the affine path through the squared edges at t₀.
Claim. Fix polarization amplitudes $E$, wavevector $k$, a periodic tetrahedron $\tau$, and a local slot $f\in\{0,\ldots,5\}$. At any amplitude $t_0$ such that all six squared edge lengths of $\tau$ are positive, the Cayley–Menger determinant is positive, and the squared cosine of the dihedral angle at slot $f$ is neither $-1$ nor $1$, the map $t\mapsto\theta_f(a_\tau(\text{plane-wave field at }t))$ is differentiable at $t_0$, with derivative equal to the closed-form slot-angle derivative at that base point.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program. The ambient object is a plane-wave edge field on a periodic lattice triangulation: each tetrahedron $\tau$ carries six squared edge lengths pulled from that field at amplitude $t$.
Nondegeneracy is encoded by positive squared edges together with a positive Cayley–Menger polynomial $\mathrm{cm}_3$ (the explicit degree-3 polynomial in the six squared lengths that measures oriented volume squared). Dihedral angles are recovered from squared cosines via the Cayley–Menger dihedral formula; the endpoint conditions exclude $\cos^2=\pm 1$ so the arccos branch stays smooth.
Upstream, a directional derivative lemma already gives differentiability of a dihedral angle along any affine path of squared edges through a fixed nondegenerate tet. The plane-wave path is affine in squared-edge coordinates once the base point is fixed, so the present result is a pure re-basing of that lemma at $a_\tau(t_0)$.
proof idea
Package the squared edges at $t_0$ with the positivity and $\mathrm{cm}_3$ hypotheses into a nondegenerate tetrahedron. Apply the directional angle-derivative lemma at that tet, in the direction of the plane-wave tet velocity, under the interior-cosine endpoint hypothesis.
Compose with the affine shift $t\mapsto t-t_0$ (derivative $1$ at $t_0$). By unfolding the plane-wave squared-edge formulas and a ring identity, the directional path $a_j(t_0)+(t-t_0)v_j$ coincides with the squared edges of the plane-wave field at time $t$. Transport the derivative across that functional equality and unfold the definition of the closed-form slot-angle derivative.
why it matters
Direct parent is the contribution derivative: differentiability of one edge-tet angle contribution at a good amplitude. That feeds the full plane-wave action-profile derivative, which supplies Gate A2(a) (first variation vanishes at flat) and Gate A2(b) (Schläfli-reduced second variation at flat, with no arccos second derivatives).
The pathwise Schläfli identity kills the entire $\sum_e\sqrt{\ell_e},\delta'_e$ group identically near zero; the angle first derivatives supplied here are exactly what survives after that kill, contracted against flat slot length derivatives. The module reuses the first-derivative structure from the derivative gate and never re-proves it. This is Crux-1(c) of the QG full-theory campaign on the continuum TT symbol.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.