cmCofactor3_04_eq_poly
plain-language theorem explainer
The (0,4) cofactor of the tetrahedral Cayley-Menger matrix equals its named explicit polynomial in the six squared edge lengths. Anyone differentiating dihedral angles from edge data cites this for a closed form instead of a determinant minor. The proof unfolds the cofactor, swaps in the explicit 4×4 minor matrix, evaluates its determinant, and simplifies the even sign.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{0,4}(a)$ (signed minor deleting row $0$ and column $4$ of the $5\times 5$ bordered matrix) equals the corresponding explicit multivariate polynomial in those six edge-square coordinates.
background
The Cayley-Menger matrix of a tetrahedron is a $5\times 5$ bordered matrix whose off-border entries are the six squared edge lengths. A cofactor $C_{r,c}$ is $(-1)^{r+c}$ times the determinant of the minor after deleting row $r$ and column $c$. Squared edges are packaged as a map $a:{0,\ldots,5}\to\mathbb{R}$.
This module expands every such cofactor into an explicit polynomial normal form so that dihedral-angle calculus can cite named polynomial partials rather than opaque Fréchet derivatives (the cofactor analogue of the Cayley-Menger derivative module).
Upstream, the deleted $(0,4)$ submatrix is identified with a concrete matrix, and that matrix's determinant is already reduced to a polynomial identity. The sign factor is the standard parity rule $(-1)^{r+c}$.
proof idea
Unfold the cofactor and minor definitions. Rewrite the deleted submatrix via the equality that matches it to the named $(0,4)$ minor matrix, then replace the determinant by the precomputed polynomial evaluation of that matrix. What remains is the cofactor sign $(-1)^{0+4}$; since $4$ is even the sign is $+1$, discharged by simplification with a decide proof of evenness.
why it matters
This is one arm of the exhaustive case split that proves every tetrahedral Cayley-Menger cofactor agrees with its polynomial normal form. That global agreement is the parent theorem this feeds: once all twenty-five cofactors match, downstream dihedral-angle work can differentiate named polynomials instead of determinants. In the Recognition geometry stack those cofactors supply the algebraic backbone for volume and angle identities that connect discrete edge data to continuum geometry, parallel to the derivative expansions already available for the Cayley-Menger determinant itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.