dihedralDenom3PolyClosedDerivValue
plain-language theorem explainer
Closed-form partial of the polynomial dihedral denominator (square root of the product of the two opposite diagonal Cayley-Menger cofactors) in one squared-edge coordinate. Anyone differentiating cofactor-ratio cosines or Schläfli edge summands on a tetrahedron cites it. The body is the elementary chain-rule formula for d(sqrt(uv)), written entirely in explicit cofactor polynomials and their partials.
Claim. Given squared edge lengths $a$, an edge index $e\in\{0,\ldots,5\}$, and a coordinate $k\in\{0,\ldots,5\}$, let $p,q$ be the two Cayley-Menger vertices opposite $e$. Write $C_{ij}(a)$ for the explicit polynomial cofactor and $\partial_k C_{ij}(a)$ for its partial in the $k$-th squared edge. The value is $$\frac{(\partial_k C_{pp})\,C_{qq}+C_{pp}\,(\partial_k C_{qq})}{2\sqrt{C_{pp}\,C_{qq}}}.$$
background
The module supplies calculus hooks for Cayley-Menger cofactors and the dihedral cofactor ratio on a tetrahedron. Squared edge lengths live in SqEdges (maps from six edge indices to reals). For each edge $e$, oppositeCMVertices returns the pair $(p,q)$ of Cayley-Menger matrix vertices opposite that edge.
The polynomial cofactor $C_{rc}(a)$ is the explicit normal form of every $5\times5$ Cayley-Menger minor; cmCofactorPartial is its hand-expanded partial in one squared-edge slot. The polynomial dihedral denominator is then $\sqrt{C_{pp}(a),C_{qq}(a)}$, deliberately lighter than the determinant-normalized version because it skips det scaling.
Local setting: hard symbolic simplifications of these derivatives sit downstream; this layer only makes the calculus interface explicit and polynomial.
proof idea
Definition, not a proof. Unpack opposite vertices $(p,q)$ for edge $e$, then write the classical identity $$\partial_k\sqrt{uv}=\frac{(\partial_k u),v+u,(\partial_k v)}{2\sqrt{uv}}$$ with $u=C_{pp}(a)$, $v=C_{qq}(a)$, substituting the explicit cofactor polynomials and their partials, and the already-defined polynomial denominator in the bottom.
why it matters
Feeds the closed-form derivative of the cofactor-ratio cosine (quotient rule with this denominator derivative in the numerator) and the equality theorem that identifies the determinant-style closed derivative with this polynomial version. All six Schläfli summand bridge lemmas (one per tetrahedron edge) unfold through the squared closed dihedral derivative, which bottoms out on this expression; those bridges convert radical edge factors times dihedral derivatives into normalized polynomial Schläfli summands. In the Recognition geometry stack this is the concrete calculus step that lets dihedral variation talk to Cayley-Menger volume polynomials without leaving the polynomial ring.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.