cmCofactor3_00_eq_poly
plain-language theorem explainer
The (0,0) cofactor of the tetrahedral Cayley-Menger matrix equals an explicit quadratic polynomial in the six squared edge lengths. Anyone expanding dihedral angles or volume formulas from edge data via cofactors would cite this identity. The proof matches the deleted-row minor to a named 4×4 matrix, substitutes its precomputed determinant, and multiplies by the cofactor sign (+1).
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the $(0,0)$-cofactor of the $5\times 5$ Cayley-Menger matrix built from $a$ equals $(a_2)^2(a_3)^2-2a_1 a_2 a_3 a_4+(a_1)^2(a_4)^2-2a_0 a_2 a_3 a_5-2a_0 a_1 a_4 a_5+(a_0)^2(a_5)^2$.
background
The Cayley-Menger determinant recovers the squared volume of a simplex from squared pairwise distances. For a tetrahedron the ambient matrix is $5\times 5$; its cofactors appear in dihedral-angle formulas and in any calculus that differentiates volume with respect to edges.
This module expands every tetrahedral cofactor into an explicit polynomial in the six squared edge coordinates, so downstream dihedral calculus can name polynomial partials instead of opaque matrix determinants. Squared edges are an assignment $a:\mathrm{Fin},6\to\mathbb{R}$. The cofactor $C_{r,c}$ is $(-1)^{r+c}$ times the determinant of the minor that deletes row $r$ and column $c$.
The explicit normal form hard-codes the expanded expression for each index pair. Upstream, deleting row and column 0 yields a concrete $4\times 4$ matrix whose determinant has already been evaluated as a polynomial; a separate lemma identifies that matrix with the corresponding submatrix of the Cayley-Menger array.
proof idea
Unfold the cofactor into sign times minor determinant. Rewrite the submatrix after deleting row 0 and column 0 as the named $4\times 4$ matrix via the submatrix-equality lemma, then replace its determinant by the precomputed polynomial identity for that matrix. The sign factor is $(-1)^{0+0}=+1$ (even parity), discharged by simplification with a trivial evenness check on $0$. The result matches the $(0,0)$ clause of the explicit polynomial table.
why it matters
This lemma is one cell of the full agreement theorem that every determinant cofactor of the tetrahedral Cayley-Menger matrix equals its explicit polynomial normal form. That parent cases on all pairs $(r,c)\in\mathrm{Fin},5\times\mathrm{Fin},5$ and dispatches the $(0,0)$ branch here. The global equality is what lets dihedral-angle calculus replace every cofactor by a named polynomial, the cofactor analogue of the volume-polynomial derivative module.
In the Recognition geometry stack, explicit cofactor polynomials support simplex and rigid constraints in the forced $D=3$ spatial setting (forcing step T8). The claim is fully proved; no scaffolding remains on this cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.