fderiv_dihedralAngle3Sq_apply_single
plain-language theorem explainer
At a nondegenerate tetrahedron, the Fréchet derivative of the squared dihedral angle (as a map on the six squared edge lengths), evaluated on the k-th coordinate basis vector, equals the closed-form coordinate partial. First-variation and Regge TT-gate arguments cite this to assemble directional derivatives from six partials. The proof matches the Fréchet derivative along a single-edge update path against the explicit one-variable derivative by uniqueness.
Claim. Let $T$ be a nondegenerate tetrahedron with squared edge lengths $a\in\mathbb{R}^{6}$, and fix indices $f,k\in\{0,\ldots,5\}$. Assume the cosine of the $f$-th dihedral angle at $a$ is not $\pm 1$. Then the Fr\'echet derivative of $a\mapsto \theta_f(a)^{2}$ at $a$ applied to the standard basis vector $e_k$ equals the closed-form partial $\partial_{a_k}\theta_f^{2}$ at $T$.
background
This module records the analytic first variation of the full nonlinear Regge action at the flat conformal potential. The geometric target is Schläfli cancellation plus zero deficit; until the global derivative is expanded from closed-form local Schläfli identities, the module supplies exact local derivative statements.
Squared edge lengths of a tetrahedron are an element $a:\mathrm{Fin},6\to\mathbb{R}$. Dihedral data are extracted from Cayley–Menger cofactors $C_{r,c}$ of the $5\times 5$ bordered matrix built from those lengths. The squared dihedral angle $\theta_f^{2}$ is a smooth function of $a$ on the nondegenerate locus provided the cosine is interior ($\cos\theta_f\neq\pm 1$), so the denominator built from opposite-vertex cofactors stays nonzero.
Upstream smoothness (dihedralAngle3Sq_contDiffAt_nonDegenerate) and the explicit one-variable derivative along a single edge update supply the two sides that this theorem identifies.
proof idea
Obtain $C^{1}$ of $a\mapsto\theta_f(a)^{2}$ at $T$ from the nondegenerate interior-cosine lemma, then pass to DifferentiableAt and HasFDerivAt for the Fréchet derivative.
Rewrite the base point as Function.update T.sqEdge k (T.sqEdge k) and compose with the affine single-coordinate path $t\mapsto\mathrm{update}(T.sqEdge,k,t)$, whose derivative is the standard basis vector (via functionUpdate_hasDerivAt_single). Chain rule yields a one-variable HasDerivAt for the composition.
Separately invoke the closed-form coordinate derivative hasDerivAt_dihedralAngle3Sq_explicit, after checking the product of opposite cofactors and the dihedral denominator are nonzero (via dihedralDenom3_eq_poly and nondegeneracy). Uniqueness of derivatives equates the two slopes; simp identifies the Fréchet evaluation on $\mathrm{Pi.single},k,1$ with dihedralClosedDerivSq.
why it matters
Coordinate partials of squared dihedral angles are the atomic input to every first- and second-variation identity for the nonlinear Regge action in this codebase. Downstream, localAngleSqEdgeChainRulePackage_of_flat packages them into a triangulation-level chain-rule record at flat configurations; the nonlinear Hessian proof lifts the same data to a neighborhood of the flat conformal potential.
In the gravity analysis layer, hasDerivAt_flatAngle_directional (Regge TT derivative gate) and its non-flat generalization hasDerivAt_angle_directional assemble the directional derivative along $t\mapsto a+tv$ as $\sum_k v_k\cdot(\text{partial}_k)$ precisely by feeding this Fréchet-on-basis evaluation. That gate is the analytic step that turns Schläfli cancellation into a vanishing first variation at flat space, the geometric content of the module target.
Within Recognition geometry this is pure classical Regge calculus (no phi-ladder or T0–T8 forcing), but it is the local differential engine behind discrete curvature identities used later in the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.