cmCofactor3_03_eq_poly
plain-language theorem explainer
For any six squared edge lengths of a tetrahedron, the (0,3) Cayley–Menger cofactor equals a fixed explicit polynomial in those edges. Anyone computing tetrahedral volumes, dihedral angles, or CM partials cites this equality. The proof unfolds the cofactor, replaces the deleted submatrix by a named 4×4 matrix, inserts its closed-form determinant, and fixes the sign (−1)^{0+3} = −1.
Claim. Let $a:\{0,\ldots,5\}\to\mathbb{R}$ be the six squared edge lengths of a tetrahedron. The Cayley–Menger cofactor $C_{0,3}(a)$ obtained by deleting row $0$ and column $3$ of the $5\times 5$ Cayley–Menger matrix equals the explicit polynomial $P_{0,3}(a)$ in those six coordinates.
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates, so downstream dihedral-angle calculus can use named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The ambient object is the $5\times 5$ Cayley–Menger matrix built from those edges. The minor that deletes row $r$ and column $c$ is its determinant after the corresponding succAbove submatrix; the cofactor multiplies that minor by the sign $(-1)^{r+c}$.
For the pair $(0,3)$ the module supplies a concrete $4\times 4$ matrix equal to that submatrix, together with a closed-form evaluation of its determinant. The target polynomial $P_{0,3}$ is the matching arm of the global cofactor normal form.
proof idea
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 the identity equating it to the named $(0,3)$-minor matrix, then replace the determinant by the precomputed closed form of that matrix. Finally simplify the cofactor sign: $0+3$ is odd, so the sign is $-1$, matching the leading sign built into the polynomial arm.
why it matters
This is one of the twenty-five case lemmas that assemble the master agreement theorem: every determinant cofactor of the tetrahedral Cayley–Menger matrix equals its explicit polynomial normal form. That master statement is the cofactor analogue of the earlier Cayley–Menger derivative expansions; together they let Recognition geometry treat volume and dihedral-angle formulae as ordinary polynomials on the edge ladder rather than as black-box matrix calculus. The result is pure classical geometry scaffolding inside the RS geometry layer; it does not itself invoke the forcing chain or the Recognition Composition Law, but it supplies the algebraic substrate those later geometric claims need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.