cmCofactor3_31_eq_poly
plain-language theorem explainer
The (3,1)-cofactor of the tetrahedral Cayley-Menger matrix equals a fixed explicit polynomial in the six squared edge lengths. Anyone reducing dihedral-angle or volume formulas to edge coordinates would cite it. The proof unfolds the cofactor, matches the deleted-row submatrix to a named 4×4 matrix, substitutes a precomputed determinant polynomial, and fixes the sign by parity of 3+1.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the Cayley-Menger cofactor $C_{3,1}(a)$ (signed minor deleting row 3 and column 1 of the $5\times 5$ Cayley-Menger matrix) equals the explicit polynomial normal form tabulated for indices $(3,1)$ in those six coordinates.
background
The module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates. It is the cofactor analogue of the derivative module: downstream dihedral-angle calculus can quote named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data are maps $a:\mathrm{Fin},6\to\mathbb{R}$. The matrix cofactor is $C_{r,c}=(-1)^{r+c}\det M^{(r|c)}$, where $M^{(r|c)}$ is the Cayley-Menger matrix with row $r$ and column $c$ deleted. The sign is the real number $+1$ or $-1$ according as $r+c$ is even or odd. The target normal form is a match on the pair $(r,c)$ that returns a concrete multilinear polynomial in the six edge squares.
Two upstream facts pin the $(3,1)$ case: the submatrix after deleting row 3 and column 1 equals a named $4\times 4$ matrix of edge squares, and the determinant of that named matrix has already been expanded to a polynomial.
proof idea
Unfold the cofactor and minor definitions so the goal is a signed determinant of a submatrix. Rewrite that submatrix via the equality that identifies it with the named $(3,1)$-minor matrix, then replace the determinant by the precomputed polynomial identity for that matrix. Finish by simplifying the cofactor sign: $3+1=4$ is even, so the sign factor is $+1$, and the two sides match.
why it matters
This is one cell in the exhaustive case split that proves every tetrahedral Cayley-Menger cofactor agrees with the explicit polynomial table. The parent theorem cases on all pairs $(r,c)\in\mathrm{Fin},5\times\mathrm{Fin},5$ and dispatches each cell to a sibling of this form; once that parent is closed, dihedral-angle and volume calculus can differentiate named polynomials rather than opaque matrix minors.
In the broader Recognition geometry stack the Cayley-Menger apparatus sits under the $D=3$ forcing step: tetrahedra are the elementary 3-simplices whose edge data feed continuum limits. Explicit cofactor polynomials are the algebraic substrate for those continuum identities. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.