cmCofactor3_24_eq_poly
plain-language theorem explainer
The (2,4) cofactor of the tetrahedral Cayley-Menger matrix equals the named explicit polynomial in the six squared edge lengths. Geometers and anyone differentiating dihedral cosines cite it when they need a closed algebraic form instead of an opaque determinant. The proof unfolds the cofactor, replaces the minor by its 4×4 submatrix identity, evaluates that determinant, and fixes the sign (+1) because 2+4 is even.
Claim. For every assignment $a$ of the six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{2,4}(a)$ equals the explicit polynomial $\mathrm{Poly}_{2,4}(a)$ in those six coordinates.
background
The module expands every cofactor of the 5×5 tetrahedral Cayley-Menger matrix into a named polynomial in the six squared edge coordinates (SqEdges). Downstream dihedral-angle calculus can then differentiate those polynomials instead of opaque fderiv terms.
A cofactor is $C_{r,c} = (-1)^{r+c},M_{r,c}$, where $M_{r,c}$ is the determinant of the matrix obtained by deleting row $r$ and column $c$. The sign is $+1$ when $r+c$ is even and $-1$ otherwise. The companion definition cmCofactor3Poly is the closed-form expansion of that determinant as a multilinear polynomial in the edge squares.
This lemma is the $(r,c)=(2,4)$ case. Sibling lemmas treat the other index pairs; together they feed the uniform statement that every cofactor agrees with its polynomial normal form.
proof idea
Term-mode, four steps. Unfold the cofactor and minor definitions so the goal is a signed determinant of a submatrix of the Cayley-Menger matrix. Rewrite that submatrix via cmMinor24_submatrix_eq and replace its determinant by the precomputed closed form det_cmMinor24Matrix. Finally simp on the sign definition: $2+4=6$ is even, so the sign factor is $+1$ and the two sides match.
why it matters
Parent theorems are cmCofactor3_eq_poly (full agreement of every determinant cofactor with its polynomial) and cmCofactor3_opposite_eq_poly (agreement on the six numerator cofactors that appear in tetrahedral dihedral cosines). The opposite-cofactor theorem dispatches edge index 1 by calling this lemma directly.
In the Recognition geometry stack these polynomials are the algebraic substrate for dihedral-angle derivatives used in rigidity and forcing arguments. Explicit cofactors let later calculus stay inside the ring of polynomials on edge squares rather than symbolic matrix determinants, which is what the module advertises as the cofactor analogue of CayleyMengerDerivatives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.