cmCofactor3_14_eq_poly
plain-language theorem explainer
For any six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor at indices (1,4) equals a named explicit polynomial in those coordinates. Geometers and RS geometry proofs cite it to replace opaque 4×4 determinants by polynomial algebra when computing dihedral numerators. The proof unfolds the cofactor, substitutes a precomputed minor determinant, and evaluates the odd sign (−1)^{1+4}.
Claim. For any assignment $a$ of the six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{1,4}(a)$ equals the explicit polynomial normal form $\mathrm{Poly}_{1,4}(a)$ in those squared edges.
background
The tetrahedral Cayley-Menger matrix is the standard $5\times 5$ bordered matrix built from squared edge lengths; its determinant encodes $288V^2$. Cofactors of that matrix enter closed formulas for dihedral cosines and related metric quantities.
In this module every such cofactor is expanded into an explicit polynomial in the six squared-edge coordinates, so downstream dihedral calculus can differentiate named polynomials instead of opaque Fréchet derivatives. The cofactor $C_{r,c}$ is defined as the sign $(-1)^{r+c}$ times the determinant of the submatrix obtained by deleting row $r$ and column $c$.
The companion polynomial map supplies a closed-form expression for each index pair. The present lemma is the agreement identity for the single pair $(1,4)$.
proof idea
Unfold the cofactor and minor definitions. Rewrite the deleted submatrix via the specialized identity that matches it to an explicit $4\times 4$ matrix in the edge coordinates, then replace that determinant by the precomputed polynomial evaluation for the matrix. Finish by simplifying the cofactor sign: $1+4=5$ is odd, so the sign is $-1$, matching the polynomial normal form.
why it matters
This is one arm of the exhaustive case split that proves every tetrahedral Cayley-Menger cofactor equals its polynomial normal form. That global agreement theorem is what lets every numerator cofactor used by tetrahedral dihedral cosines be treated as a polynomial, which is the cofactor-side analogue of the Cayley-Menger derivative calculus described in the module header.
In the Recognition geometry stack, explicit cofactor polynomials keep tetrahedral constraints inside ordinary algebra rather than opaque determinants. That is the setting needed for later closed-form work on spatial structure tied to the $D=3$ landmark (T8) and to discrete geometric measurement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.