dihedralCos3SqClosedFormDeriv
plain-language theorem explainer
Closed-form partial of the tetrahedral dihedral cosine (Cayley–Menger cofactor ratio) with respect to any squared-edge coordinate. Anyone differentiating dihedral angles or building the flat-angle Jacobian in Regge analysis cites this value. The body is the ordinary quotient rule evaluated on the closed-form numerator and square-root denominator cofactors.
Claim. For squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$, edge index $e$, and coordinate index $k$, let $p,q$ be the Cayley–Menger vertex pair opposite $e$, $N=C_{pq}(a)$ the off-diagonal cofactor, $D$ the square-root cofactor denominator along $e$, and $N_k$, $D_k$ their closed-form partials in coordinate $k$. The closed-form cosine derivative is $(N_k\,D-N\,D_k)/D^2$.
background
The module supplies derivative hooks for Cayley–Menger cofactors and the dihedral cofactor-ratio cosine, so the calculus layer is explicit rather than implicit. Squared edge lengths of a tetrahedron are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The Cayley–Menger cofactor $C_{r,c}$ is the signed $3\times 3$ minor of the bordered CM matrix.
Opposite an edge $e$, two CM vertices $(p,q)$ determine the dihedral cosine as the ratio of the off-diagonal cofactor $C_{pq}$ to a square-root denominator built from the diagonal cofactors $C_{pp}$ and $C_{qq}$. Upstream, the numerator partial is the corresponding cofactor partial in coordinate $k$, and the denominator partial is the closed-form derivative of that square-root expression (product rule under the outer square root).
The local goal is a coordinate-wise real value that can be fed to HasDerivAt statements and to chain-ruled angle derivatives without re-deriving the quotient each time.
proof idea
Pure definition: no proof obligations. Unpack the opposite CM vertex pair $(p,q)$ for edge $e$, then instantiate the classical quotient rule $$\partial_k(N/D)=(N_k D-N D_k)/D^2$$ with $N=\mathrm{cmCofactor3},a,p,q$, $N_k$ the closed numerator partial, $D$ the dihedral square-root denominator, and $D_k$ its closed-form derivative value. The expression is definitionally the value that later equality lemmas match to the generic quotient derivative and to the polynomial-cofactor form.
why it matters
This value is the algebraic payload behind explicit differentiability of the cofactor cosine and, via the arccos chain rule, of the tetrahedral dihedral angle itself. Downstream, dihedralCos3SqClosedFormDeriv_eq_generic and _eq_poly certify that the formula agrees with both the generic quotient derivative and the lighter polynomial-denominator form; hasDerivAt_dihedralCos3Sq_explicit turns it into a calculus fact.
In DihedralDerivatives, the angle derivative is exactly $-(1/\sqrt{1-\cos^2})\cdot$ this quantity. That feeds the Regge TT gate: flatAngleJacobian_cofactor_form states every flat-angle Jacobian entry is pure cofactor algebra times the evaluated arccos factor, with this closed-form cosine derivative at the Freudenthal tetrahedron and no arccos value on the right-hand side. It is the concrete bridge from CM cofactor calculus to the gravity-side derivative gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.