cmCofactorPartial
plain-language theorem explainer
Explicit closed-form partial derivative of each tetrahedral Cayley-Menger cofactor with respect to one squared-edge coordinate. Dihedral-angle calculus cites it in place of opaque automatic derivatives. The body is a generated match table: every (row, column, edge) triple maps to a concrete multilinear polynomial in the six squared edges.
Claim. For row $r\in\{0,\ldots,4\}$, column $c\in\{0,\ldots,4\}$, edge index $k\in\{0,\ldots,5\}$, and squared-edge vector $a=(a_0,\ldots,a_5)$, return the explicit partial $\partial_{a_k}$ of the $(r,c)$ Cayley-Menger cofactor polynomial, as a real polynomial in the six squared edge lengths.
background
The module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates. It is the cofactor analogue of the Cayley-Menger derivative module: downstream dihedral-angle work can name polynomial partials instead of opaque Fréchet derivatives.
Squared edges are the type $\mathrm{SqEdges}:=\mathrm{Fin},6\to\mathbb{R}$, the six independent $d_{ij}^2$ of a tetrahedron. Cofactors of the bordered Cayley-Menger matrix enter the classical cosine formulas for dihedral angles (numerator cofactor over a product of diagonal cofactors under a square root).
Sibling definitions supply the cofactor polynomials themselves and the $3\times3$ minor matrices; this declaration is only the coordinate-wise partial table for those polynomials.
proof idea
Pure definition by exhaustive pattern match on $(r.val, c.val, k.val)$. Each arm is a hand-expanded (generated) multilinear expression in $a_0,\ldots,a_5$; unmatched index triples fall through the elided default. No lemmas are applied: the content is the closed-form table itself, later certified by agreement and Taylor-update theorems in the same module.
why it matters
Parent consumers in CofactorDerivatives build every closed dihedral derivative from this table: numerator partial, left and right diagonal partials, square-root denominator derivative, and the quotient rule for the squared-cosine polynomial. Same-module Taylor forms (e.g. the $(3,4)$ cofactor update) quote it as the linear coefficient in $t$.
In the Recognition geometry stack this replaces symbolic fderiv with named polynomials, so hinge-aware Regge and discrete-curvature arguments can differentiate dihedral data algebraically. It does not itself touch the T0-T8 forcing chain; it is infrastructure for the geometric layer that feeds discrete gravity and eight-tick spatial structure ($D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.