dihedralLeftDiagClosedDeriv
plain-language theorem explainer
Gives the explicit partial of the left diagonal Cayley–Menger cofactor (the (p,p) entry for the first vertex opposite a chosen tetrahedral edge) with respect to any squared-edge coordinate. Anyone differentiating dihedral cosines or the square-root cofactor denominator cites it. The body is a one-line selection: opposite vertex index, then the matching cofactor partial.
Claim. For squared edge lengths $a\colon\{0,\ldots,5\}\to\mathbb{R}$, edge index $e$, and coordinate $k$, if $p$ is the first Cayley–Menger vertex opposite $e$, the left diagonal closed derivative is the explicit partial $\partial_{a_k}C_{pp}(a)$ of the $(p,p)$ cofactor polynomial.
background
The module supplies calculus hooks for Cayley–Menger cofactors and the dihedral cofactor ratio on a tetrahedron. Squared edge lengths live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The classical $5\times5$ Cayley–Menger matrix has cofactors $C_{rc}$; their coordinate partials are packaged as an explicit polynomial table cmCofactorPartial.
For each of the six edges $e$, oppositeCMVertices returns the pair $(p,q)$ of CM vertex indices opposite that edge. The left diagonal denominator cofactor is the entry $C_{pp}$. Differentiating dihedral data (cosines built from cofactor ratios, and the geometric mean $\sqrt{C_{pp}C_{qq}}$) therefore needs $\partial_{a_k}C_{pp}$ in closed form.
Upstream, cmCofactorPartial r c k a is the fully expanded multilinear expression for $\partial_{a_k}C_{rc}$; this definition simply specialises to the diagonal $(p,p)$ with $p$ the first opposite vertex of $e$.
proof idea
Definitional, not a proof. Bind $p:=(\mathrm{oppositeCMVertices},e)_1$, then return cmCofactorPartial p p k a. No tactics, no lemmas beyond that lookup and the partial table.
why it matters
Feeds the closed derivative of the square-root cofactor denominator: dihedralDenom3ClosedDerivValue applies the product/quotient rule
$(\partial C_{pp},C_{qq}+C_{pp},\partial C_{qq})/(2\sqrt{C_{pp}C_{qq}})$
using this left term and its right twin. That value is identified with a pure polynomial form in dihedralDenom3ClosedDerivValue_eq_poly, and both sit under the explicit coordinate derivative theorem hasDerivAt_dihedralCos3Sq_explicit for the Cayley–Menger cofactor cosine.
In the Recognition geometry stack this is infrastructure for hinge-aware Regge/TT analysis: dihedral angles and their edge derivatives must be algebraic in the six squared lengths, not opaque calculus. The module doc states the hard symbolic simplifications remain downstream; this hook makes the left-diagonal piece of that calculus layer explicit and reusable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.