det_cmMinor30Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor from deleting row 3 and column 0 equals the negative of the matching cofactor polynomial in the six squared edge lengths. Anyone equating abstract CM cofactors to polynomial normal forms cites this identity. The proof unfolds both sides, expands the determinant along the first row, and finishes by ring normalization.
Claim. For any assignment $a:\{0,\ldots,5\}\to\mathbb{R}$ of squared tetrahedron edge lengths, $\det M_{3,0}(a)=-P_{3,0}(a)$, where $M_{3,0}(a)$ is the $4\times 4$ matrix with first row $(1,1,1,1)$ and remaining entries the indicated edge squares, and $P_{3,0}$ is the explicit degree-4 cofactor polynomial at indices $(3,0)$.
background
The module expands every tetrahedral Cayley–Menger cofactor into an explicit polynomial in the six squared edge coordinates. Downstream dihedral-angle calculus can then cite named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The family cmCofactor3Poly r c is the closed-form normal form for each cofactor of the bordered Cayley–Menger matrix; the $(3,0)$ case is one concrete quartic monomial combination. The companion matrix cmMinor30Matrix a is the concrete $4\times 4$ real matrix obtained by deleting that row/column pattern from the CM border structure:
$$\begin{pmatrix}1&1&1&1\0&a_0&a_1&a_2\a_0&0&a_3&a_4\a_2&a_4&a_5&0\end{pmatrix}.$$
This lemma equates its determinant to the signed polynomial, so later theorems can replace abstract minors by algebra.
proof idea
Term-mode proof by direct expansion. Unfold the matrix constructor and the $(3,0)$ polynomial clause. Apply the first-row Laplace expansion (Matrix.det_succ_row_zero) together with the finite-sum rewrites Fin.sum_univ_succ and Fin.succAbove to reduce the $4\times 4$ determinant to an explicit multilinear combination of the six edge squares. Finish with ring_nf, which matches that combination to the negated polynomial normal form.
why it matters
Immediate parent is cmCofactor3_30_eq_poly, which proves the abstract Cayley–Menger cofactor at indices $(3,0)$ equals the named polynomial: it rewrites the minor via the submatrix identity, applies this determinant lemma, and adjusts the cofactor sign (odd index sum). That equality is one cell of the full cofactor-polynomial agreement table used throughout the geometry stack.
In the broader Recognition geometry layer, explicit cofactor polynomials let dihedral-angle derivatives and volume sensitivities be manipulated as ordinary polynomials on the edge-square coordinates rather than as black-box automatic derivatives. The module is the cofactor analogue of CayleyMengerDerivatives; closing each minor-to-poly identity (including this one) removes scaffolding between the classical CM determinant and the computable phi-ladder geometry that sits above it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.