det_cmMinor40Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor that drops row 4 and column 0 equals the named degree-4 polynomial in the six squared edge lengths for that cofactor slot. Anyone expanding tetrahedral cofactors for dihedral-angle calculus cites this identity. The proof unfolds both sides and reduces the Laplace expansion along the first row by ring normalization.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the determinant of the $4\times 4$ matrix obtained by deleting row $4$ and column $0$ of the bordered Cayley–Menger matrix equals the explicit cofactor polynomial $P_{4,0}(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 name polynomial partials instead of opaque Fréchet derivatives.
SqEdges is simply $\mathrm{Fin},6\to\mathbb{R}$: the six squared edge lengths of a tetrahedron. The bordered Cayley–Menger matrix is the usual $5\times 5$ array built from a constant border row/column of ones and the squared distances. The minor matrix for indices $(4,0)$ is the concrete $4\times 4$ block
$$\begin{pmatrix}1&1&1&1\0&a_0&a_1&a_2\a_0&0&a_3&a_4\a_1&a_3&0&a_5\end{pmatrix}.$$
cmCofactor3Poly is the match-defined normal form that lists, for every pair of indices, the expanded multilinear polynomial that the corresponding cofactor is claimed to equal.
proof idea
Pure algebraic identity, no geometry. Unfold the minor-matrix definition and the target polynomial clause for indices $(4,0)$. Expand the $4\times 4$ determinant along the first row via Matrix.det_succ_row_zero, push the finite sums with Fin.sum_univ_succ and Fin.succAbove, then finish by ring_nf, which matches the expanded expression to the hard-coded polynomial.
why it matters
Feeds directly into cmCofactor3_40_eq_poly, which equates the abstract cofactor (signed determinant of the submatrix extracted from the live Cayley–Menger matrix) with this polynomial normal form. That agreement theorem is one cell of the module-wide CofactorPolynomialAgreement pattern: every cofactor becomes a named polynomial so partial derivatives needed for dihedral angles are ordinary polynomial calculus rather than opaque fderiv terms. The module is the cofactor analogue of CayleyMengerDerivatives. In the broader Recognition geometry stack these explicit cofactors support volume and angle identities on the tetrahedron that sit under the $D=3$ forcing (T8) and the eight-tick discrete geometry, though this single determinant identity itself is pure linear algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.