dihedralCos3SqDerivValue
plain-language theorem explainer
Explicit quotient-rule value for the derivative of the squared dihedral cosine, written as a Cayley–Menger cofactor ratio along a path γ of squared-edge data. Geometers working Schläfli identities or Hessian closure cite it as the concrete scalar that HasDerivAt statements target. The body is a pure definition: numerator and denominator derivatives plugged into (n'd − n d')/d².
Claim. Given a path $\gamma:\mathbb{R}\to\mathrm{SqEdges}$, a point $x\in\mathbb{R}$, scalars $n',d'\in\mathbb{R}$, and an edge index $e\in\{0,\ldots,5\}$, let $p,q$ be the Cayley–Menger vertices opposite $e$, write $N=C_3(\gamma(x);p,q)$ and $D=D_3(\gamma(x);e)$ for the off-diagonal cofactor and the dihedral denominator. The declared value is $(n'D - N\,d')/D^2$, i.e. the classical quotient-rule derivative of $N/D$ when $n'$ and $d'$ are the derivatives of numerator and denominator.
background
The module supplies calculus hooks for Cayley–Menger cofactors on six squared edge lengths of a tetrahedron (type SqEdges). The squared cosine of a dihedral angle is realized as a ratio of CM cofactors: the numerator is the off-diagonal $3\times3$ cofactor $C_3(a;p,q)$ for the pair of vertices opposite edge $e$, and the denominator $D_3(a;e)$ is built from the two diagonal cofactors on those vertices.
Along a smooth path $\gamma$ of edge-squared configurations one therefore differentiates a quotient $N/D$. The present definition packages the scalar that the quotient rule predicts once the path derivatives of $N$ and $D$ are known. Sibling definitions supply the analogous denominator derivative value and the closed-form partials coming from the cofactor polynomial module.
Local setting (module doc): hard symbolic simplifications remain downstream; this layer only makes the calculus interface explicit so later HasDerivAt theorems can name their target values.
proof idea
Pure definition, no proof obligations. Unpack opposite Cayley–Menger vertices $(p,q)$ for edge $e$, evaluate the off-diagonal cofactor $C_3(\gamma(x);p,q)$ and the dihedral denominator $D_3(\gamma(x);e)$, then return the quotient-rule combination $(n' D - C_3, d')/D^2$. The inputs $n'$ and $d'$ are treated as already-computed derivative scalars; this def does not itself differentiate.
why it matters
Names the concrete real that every dihedral-cosine derivative theorem in the geometry stack aims at. Downstream, dihedralCos3SqClosedFormDeriv_eq_generic proves the closed-form coordinate partial equals this generic value after substituting explicit cofactor polynomials; hasDerivAt_dihedralCos3Sq_from_cofactors and hasDerivAt_dihedralCos3Sq_explicit certify path and coordinate derivatives against it; hasDerivAt_dihedralAngle3Sq_from_cofactors lifts the same scalar into the angle (arccos) chain rule.
In the Recognition geometry program these hooks feed Schläfli-type identities and Hessian closure on the realisability cone. They sit under the $D=3$ spatial forcing (T8) where tetrahedral dihedral data are the natural curvature carriers. The definition closes the gap between abstract quotient calculus and the explicit cofactor polynomials needed for those targets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.