cmCofactor3_40_eq_poly
plain-language theorem explainer
For any six squared edge lengths of a tetrahedron, the (4,0)-cofactor of the 5×5 Cayley-Menger matrix equals its named explicit polynomial normal form. Anyone replacing opaque CM minors by closed-form polynomials in dihedral or volume calculus cites this identity. The proof unfolds the cofactor, identifies the deleted submatrix with a concrete matrix, inserts that matrix's determinant expansion, and simplifies the sign.
Claim. For every assignment $a$ of six squared edge lengths, the Cayley-Menger cofactor $C_{4,0}(a)$ equals the explicit polynomial normal form $P_{4,0}(a)$ in those six coordinates.
background
The module supplies explicit polynomial expansions of every cofactor of the tetrahedral Cayley-Menger matrix, so downstream dihedral-angle calculus can quote named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges (maps Fin 6 → ℝ). The matrix 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 definition cmCofactor3Poly is a match on the index pair that writes each of those determinants as a fixed multilinear polynomial in the six squared lengths.
Upstream, cmMinor40_submatrix_eq identifies the concrete $4\times4$ block after deleting row 4 and column 0 with a named matrix whose determinant has already been expanded by det_cmMinor40Matrix.
proof idea
Unfold the cofactor into sign times minor determinant. Rewrite the deleted submatrix via cmMinor40_submatrix_eq, then replace its determinant by the closed form det_cmMinor40Matrix. Finish with simp on the cofactor sign: $4+0$ is even, so the sign is $+1$.
why it matters
This is one cell in the exhaustive case split that proves cmCofactor3_eq_poly: every determinant cofactor of the tetrahedral Cayley-Menger matrix agrees with the explicit polynomial normal form. That global agreement is the cofactor analogue of the Cayley-Menger derivative module; it lets Recognition geometry treat dihedral angles and related partials as ordinary polynomial calculus on the six edge squares rather than as abstract matrix derivatives. The parent theorem simply fin_cases on the five-by-five index pair and dispatches each cell to a lemma of this shape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.