hasDerivAt_angle_directional
plain-language theorem explainer
Along any affine path in squared-edge space through a nondegenerate tetrahedron with interior dihedral cosines, the directional derivative of one dihedral angle at the base point equals the contraction of the direction with the six closed-form coordinate partials. Gravity analysts cite it when building pathwise angle derivatives for the Regge TT plane-wave profile. The proof is Fréchet differentiability of the angle map plus chain rule along the affine path, evaluated via the known single-coordinate partials.
Claim. Let $T$ be a nondegenerate tetrahedron with squared edges $a\in\mathbb{R}^6$, let $f\in\{0,\ldots,5\}$ index a dihedral, and assume the Cayley–Menger dihedral cosine satisfies $\cos\theta_f(a)\notin\{-1,1\}$. For any direction $v\in\mathbb{R}^6$, the map $t\mapsto\theta_f(a+tv)$ is differentiable at $t=0$ with derivative $\sum_{g=0}^{5} v_g\,\partial\theta_f/\partial a_g(a)$, where the partials are the closed-form arccos chain-rule expressions.
background
This module is Gate A2 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol campaign: pathwise first and second variations of the true Regge action along a plane-wave edge field, reduced by the tetrahedral Schläfli identity so that no second derivative of arccos survives in the flat second variation.
Squared edge data live in $\mathrm{SqEdges}=\mathrm{Fin},6\to\mathbb{R}$. The dihedral cosine $\mathrm{dihedralCos3Sq}$ is the Cayley–Menger cofactor ratio; the angle is $\theta_f(a)=\arccos(\mathrm{dihedralCos3Sq}(a,f))$. The closed-form coordinate derivative multiplies the cosine partial by $-1/\sqrt{1-\cos^2\theta_f}$.
Upstream, dihedralAngle3Sq_contDiffAt_nonDegenerate supplies $C^1$ (hence Fréchet differentiability) of $\theta_f$ at any nondegenerate squared-edge point with interior cosine. The six single-coordinate Fréchet applications equal the closed-form partials, and the continuous-linear-map evaluation on $\mathbb{R}^6$ expands as a finite sum of those partials.
proof idea
Obtain $C^1$ of $x\mapsto\theta_f(x)$ at the base squared edges from the nondegenerate interior-cosine lemma, then pass to differentiability and HasFDerivAt for the Fréchet derivative.
Separately, the affine path $t\mapsto a+tv$ has derivative $v$ at $0$ by componentwise hasDerivAt (identity times constant, plus constant).
Compose Fréchet derivative with the path derivative via HasFDerivAt.comp_hasDerivAt. Identify the Fréchet application on $v$ with $\sum_g v_g\cdot\partial\theta_f/\partial a_g$ by expanding the continuous linear map as a sum of single-coordinate applications and quoting the proved single-partial lemma for each coordinate. Rewrite and simplify to finish.
why it matters
Gate A2 needs explicit pathwise derivatives of every slot angle along the plane-wave amplitude so that $S'(t)$ can be written in closed form and the Schläfli kill can erase the entire $\sum_e\sqrt{\ell_e},\delta'_e$ group identically near flat. This lemma is the base-point directional engine: it generalizes the derivative gate's flat-point angle derivative to an arbitrary nondegenerate tetrahedron with interior cosine, still using only $C^1$ plus the six coordinate partials.
Its sole direct consumer is hasDerivAt_slotAngle, which re-bases the same affine path at amplitude $t_0$ and feeds slotAngleDeriv into the profile derivative and the flat second-variation formula
$\mathrm{iteratedDeriv},2,S(0)=-\sum_\tau\sum_f L'{\tau f}(0),\theta'{\tau f}(0)$.
Without this directional step, Gate A2(b) cannot contract the flat angle Jacobian against the plane-wave edge velocities while staying free of arccos second derivatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.