cmCofactor3Poly
plain-language theorem explainer
Explicit closed-form polynomials for every entry of the 5×5 Cayley–Menger cofactor array of a tetrahedron, as a function of the six squared edge lengths. Anyone deriving dihedral cosines or their edge derivatives from cofactors cites this normal form. The body is a pure case split on the (row, column) pair with fully expanded multilinear expressions.
Claim. For indices $r,c \in \{0,1,2,3,4\}$ and squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$, the map $(r,c,a)\mapsto C_{r,c}(a)$ returns the explicit polynomial (in the six $a_i$) equal to the $(r,c)$-cofactor of the $5\times 5$ Cayley–Menger matrix of a tetrahedron; for any other index pair the value is $0$.
background
A tetrahedron is determined (up to congruence) by six edge lengths. The Cayley–Menger matrix is the standard $5\times 5$ bordered matrix of squared distances whose determinant encodes $288V^2$. Cofactors of that matrix enter classical formulas for face areas and dihedral cosines.
This module supplies the cofactor analogue of the expanded Cayley–Menger polynomial: every cofactor is written as an ordinary polynomial in the six squared-edge coordinates SqEdges ($\mathrm{Fin},6\to\mathbb{R}$), so later calculus never has to differentiate through an opaque matrix determinant.
The local setting is pure Euclidean 3-geometry of one tetrahedron; no Recognition-specific constants appear at this layer.
proof idea
Definition by exhaustive match on the pair of natural values $(r.val,c.val)$. Each of the twenty-five on-range cases is a hard-coded multilinear polynomial in $a_0,\ldots,a_5$; the catch-all returns $0$. No lemmas are invoked; the polynomials are the content.
why it matters
This is the named normal form that the whole cofactor-derivative stack hangs on. Downstream, the dihedral numerator is exactly $C_{p,q}(a)$ for the opposite Cayley–Menger vertex pair of an edge; the denominator is $\sqrt{C_{p,p}C_{q,q}}$; the discriminant identity $C_{p,p}C_{q,q}-C_{p,q}^2=2,\mathrm{CM}_3(a),a_e$ is stated directly in these polynomials; and the closed-form edge derivatives of the cofactor-ratio cosine are quotients of the corresponding partials. Without the expanded form, those objects would remain fderiv terms rather than algebraic expressions. It is scaffolding for the geometry side of Recognition’s rigid-body and packing arguments, not a forcing-chain step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.