cmCofactor3_01_eq_poly
plain-language theorem explainer
The (0,1)-cofactor of the tetrahedral Cayley-Menger matrix equals a fixed explicit polynomial in the six squared edge lengths. Geometers computing dihedral-angle derivatives cite it when they need a closed form instead of an opaque determinant minor. The proof unfolds the cofactor, replaces the deleted submatrix by its named matrix, inserts the precomputed determinant, and simplifies the odd-parity sign.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{0,1}(a)$ equals the explicit polynomial $-2 a_3 a_4 a_5 + a_2 a_3 a_5 + a_2 a_3 a_4 - a_2 a_3^2 + a_1 a_4 a_5 - a_1 a_4^2 + a_1 a_3 a_4 - a_0 a_5^2 + a_0 a_4 a_5 + a_0 a_3 a_5$.
background
This module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates. Downstream dihedral-angle calculus can then differentiate named polynomials rather than opaque fderiv terms.
A tetrahedron carries six edges; squared lengths are packaged as a map $a:\mathrm{Fin},6\to\mathbb{R}$. The Cayley-Menger matrix is the standard $5\times 5$ bordered matrix built from those lengths. Deleting row $r$ and column $c$ and taking the determinant yields the minor; the cofactor multiplies by the sign $(-1)^{r+c}$.
The target polynomial table supplies a fully expanded normal form for each index pair. An upstream equality identifies the concrete submatrix after deleting row 0 and column 1 with a named $4\times 4$ matrix whose determinant has already been evaluated in closed form.
proof idea
Unfold the cofactor and minor definitions to expose the signed determinant of the deleted submatrix. Rewrite that submatrix via the sibling equality that matches it to the named $(0,1)$-minor matrix, then substitute the precomputed determinant of that matrix. A final simplification applies the cofactor sign at $(0,1)$: $0+1$ is odd, so the sign is $-1$, which already appears as the leading minus in the polynomial branch for those indices.
why it matters
This lemma is one cell of the exhaustive fin_cases split that proves global agreement: every determinant cofactor of the tetrahedral Cayley-Menger matrix equals its explicit polynomial normal form. That parent theorem is the cofactor analogue of the Cayley-Menger derivative expansions; it lets dihedral-angle identities differentiate named polynomials instead of determinants.
In the Recognition geometry stack these closed forms support volume and angle identities that relate edge data to three-dimensional spatial structure. The result is fully proved; it closes no open scaffold and introduces none.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.