flatSlotAngleDeriv
plain-language theorem explainer
Packages the first variation of a local dihedral angle at the flat Freudenthal configuration as a six-edge contraction of plane-wave tet velocities against the shared flat angle Jacobian. Anyone writing the Schläfli-reduced second variation of the Regge TT action (Gate A2) cites this quantity as the θ' factor. Pure definitional sum: no proof obligations.
Claim. For a polarization $E$, wavevector $k$, periodic tetrahedron $\tau$, and local edge slot $f\in\{0,\ldots,5\}$, the flat slot angle derivative is $\theta'_{\tau f}(0)=\sum_{g=0}^{5} v_{\tau g}\, J_{fg}$, where $v_{\tau g}$ is the plane-wave tetrahedron edge velocity at amplitude zero and $J_{fg}=\partial\theta_f/\partial a_g$ is the flat angle Jacobian at the Freudenthal squared-edge tuple.
background
Gate A2 of the Regge TT continuum-symbol program computes the second variation of the plane-wave Regge action at the flat background. The first-derivative stencil is already locked in the derivative gate: the shared Jacobian $J_{fg}=\partial\theta_f/\partial a_g$ at the flat Freudenthal six-edge lengths is the closed-form directional derivative of the $f$-th local dihedral angle in the action's local six-edge ordering.
A periodic Freudenthal tetrahedron $\tau$ is one of the six tetrahedra inside each cubic cell of the $N\times N\times N$ torus. The plane-wave tet velocity $v_{\tau g}$ is the directional derivative of the $g$-th local squared edge length along the TT plane-wave path at amplitude zero. The module works pathwise near the flat point and uses the tetrahedral Schläfli identity to delete every arccos second derivative from the second variation, leaving only first-jet contractions of the form $L'\cdot\theta'$.
proof idea
Definitional one-liner. Sum over the six local slots $g$ of the product of the plane-wave tet velocity and the shared flat angle Jacobian from the derivative gate. No tactics, no lemmas applied: the name freezes the Gate A2(b) contraction $\theta'{\tau f}(0)=\sum_g v{\tau g} J_{fg}$ for reuse in the reduced second-variation formula.
why it matters
Gate A2(b) writes the flat second variation as $-\sum_\tau\sum_f L'{\tau f}(0)\cdot\theta'{\tau f}(0)$; this definition is exactly the $\theta'$ factor, paired with the flat slot sqrt-derivative for $L'$. Downstream, the zero-amplitude identification equates the pathwise slot angle derivative at $t=0$ with this quantity; the true Regge second-variation theorem and the combined TT Bloch symbol corollary feed it into the reduced finite value $(2/N^3)$ times the Schläfli contraction. The Bloch interface audit then equates that reduced value to the raw triple cell stencil by distributing the inner sum over $g$. Algebraic hinge between the derivative gate and the Normalization-Gated Schläfli Two-Jet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.