slotAngleDeriv_zero
plain-language theorem explainer
At vanishing plane-wave amplitude the slot dihedral-angle derivative equals the flat angle-Jacobian contraction of the tetrahedron edge velocities. Gate A2(b) of the Regge TT second-variation analysis cites this identification when rewriting the deficit-group first variation in slot form. The proof unfolds both sides and rewrites by vanishing of the squared-edge perturbation at t=0.
Claim. For polarization $E$, wavevector $k$, periodic tetrahedron $\tau$, and local edge slot $f\in\{0,\ldots,5\}$, the directional derivative of the dihedral angle at slot $f$ along the plane-wave edge-length path, evaluated at amplitude $t=0$, equals $\sum_{g=0}^{5} v_{\tau g}\, J_{fg}$, where $J$ is the shared flat angle Jacobian and $v_{\tau g}$ are the plane-wave edge velocities on $\tau$.
background
This module carries Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program. The ambient object is the plane-wave action profile $S(t)$ on a periodic Freudenthal triangulation: edge lengths are deformed by a monochromatic polarization $E$ and wavevector $k$, and $S$ is the usual Regge sum of $\sqrt{\ell_e},\delta_e$.
A slot angle is the dihedral angle at one of the six local edges of a periodic tetrahedron $\tau$. Its $t$-derivative along the path is slotAngleDeriv; at a general amplitude it depends on the instantaneous squared edge lengths. The flat specialization flatSlotAngleDeriv replaces that dependence by the closed contraction $\theta'{\tau f}(0)=\sum_g v{\tau g} J_{fg}$, where $J$ is the flat angle Jacobian already fixed in the derivative gate and $v$ are the plane-wave edge velocities.
Upstream, planeWaveTetSqEdges_zero records that the squared-edge perturbation vanishes identically at $t=0$, so the general path formula collapses to the flat Jacobian formula.
proof idea
Term-mode one-liner. Unfold the definitions of the general slot-angle derivative and of the flat Jacobian contraction; both become the same explicit sum once the squared-edge lengths are specialized. Rewrite by planeWaveTetSqEdges_zero (squared edges equal their flat values at amplitude zero) and finish by rfl.
why it matters
The immediate consumer is sum_edgeSqrtDeriv_deficitDeriv_flat, which rewrites the deficit-group first variation at flat as $-\sum_\tau\sum_f L'{\tau f}(0),\theta'{\tau f}(0)$. That identity is the algebraic engine of Gate A2(b): the second variation of the true Regge action at the flat background equals exactly the indicated double sum of flat slot sqrt-derivatives against flat slot angle derivatives, with no second derivative of $\arccos$ remaining.
In the broader campaign this closes the first-derivative bookkeeping needed before the Schläfli kill deletes the entire $\sqrt{\ell},\delta'$ block near $t=0$. It sits downstream of the derivative gate (flat Jacobian) and of local symbol existence, and upstream of the continuum TT symbol extraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.