cmCofactorPartialClosedForm
plain-language theorem explainer
Closed-form name for the partial derivative of a tetrahedral Cayley–Menger cofactor with respect to one squared edge length. Geometry and dihedral-angle work cites this when it needs the polynomial expression rather than an opaque derivative. The body is a one-line alias of the explicit match-based partial already defined in the same module.
Claim. For matrix indices $r,c\in\{0,\ldots,4\}$, edge index $k\in\{0,\ldots,5\}$, and squared-edge coordinates $a:\{0,\ldots,5\}\to\mathbb{R}$, the closed-form cofactor partial equals the explicit polynomial partial of the $(r,c)$-cofactor of the $5\times5$ Cayley–Menger matrix in the coordinate $a_k$.
background
The module expands every tetrahedral Cayley–Menger cofactor as an explicit polynomial in the six squared edge lengths. Downstream dihedral-angle calculus can then name polynomial partials instead of opaque Fréchet derivatives.
Squared edge data are packaged as SqEdges: a map from Fin 6 into $\mathbb{R}$. The sibling partial cmCofactorPartial is the concrete match on $(r,c,k)$ that returns the corresponding multilinear monomial expression (e.g. for $(0,0,0)$ the cubic form $-2a_2 a_3 a_5-2a_1 a_4 a_5+2a_0 a_5^2$).
The doc-comment states the design split: derivative theorems stay separate from the polynomial normal form; one-variable HasDerivAt proofs live in the quotient-derivative layer once cofactors are specialized.
proof idea
Definitional one-line wrapper. The right-hand side is exactly the explicit partial cmCofactorPartial r c k a; no further algebraic reduction or tactic proof is performed here. All case-by-case polynomial content lives in that match definition.
why it matters
Gives a stable closed-form handle on Cayley–Menger cofactor partials so dihedral-angle and volume calculus can quote named polynomials rather than fderiv terms. It is the cofactor-side counterpart of the Cayley–Menger derivative module. No downstream consumers are wired in this graph snapshot; the intended landing zone is the quotient-derivative layer that discharges HasDerivAt after cofactors are specialized. Within Recognition geometry this supports rigid tetrahedral edge calculus that feeds higher structure (octave/tick geometry, spatial $D=3$ forcing) once angles and volumes are expressed in $\phi$-native units. It does not itself touch the T0–T8 chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.