det_cmMinor04Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor that drops row 0 and column 4 equals the named degree-4 cofactor polynomial at indices (0,4), for any six squared edge lengths. Anyone equating abstract CM cofactors to polynomial normal forms cites this. The proof unfolds both sides, expands the determinant along the first row, and finishes by ring normalization.
Claim. For every assignment $a:\{0,\ldots,5\}\to\mathbb{R}$ of squared edge lengths of a tetrahedron, $\det M_{0,4}(a)=P_{0,4}(a)$, where $M_{0,4}(a)$ is the $4\times 4$ matrix $\begin{pmatrix}1&0&a_0&a_1\\1&a_0&0&a_3\\1&a_1&a_3&0\\1&a_2&a_4&a_5\end{pmatrix}$ and $P_{0,4}$ is the explicit Cayley–Menger cofactor polynomial at row–column indices $(0,4)$.
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 quote named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The family of target polynomials is the match-defined map that, for each pair of indices $(r,c)\in\mathrm{Fin},5\times\mathrm{Fin},5$, returns a fixed multilinear expression in the six edge squares. The matrix whose determinant is taken here is the concrete $4\times 4$ array obtained by deleting the indicated row and column from the bordered Cayley–Menger layout and writing the remaining entries in terms of those six coordinates.
This identity is the computational half of the bridge from the abstract minor (built by submatrix extraction) to the closed-form polynomial; the companion equality that inserts the sign and identifies the geometric cofactor sits immediately downstream.
proof idea
Term-mode proof by direct expansion. Unfold the matrix constructor and the target polynomial clause so both sides are concrete expressions in the six edge squares. Apply the first-row Laplace expansion (Matrix.det_succ_row_zero) together with the finite-sum and succAbove simplifiers to reduce the $4\times 4$ determinant to a polynomial. Finish with ring_nf, which matches the expanded determinant against the pre-written normal form for indices $(0,4)$.
why it matters
Feeds the parent theorem that equates the geometric Cayley–Menger cofactor at $(0,4)$ to the explicit polynomial: that parent rewrites the cofactor via the minor-submatrix identity, invokes this determinant equality, and adjusts the cofactor sign (even index 4). The module’s purpose is precisely this cofactor-to-polynomial dictionary, the cofactor analogue of the earlier derivative expansions, so that dihedral-angle formulae can differentiate named polynomials rather than abstract determinants. Within the broader geometry stack it supplies one of the six edge-indexed cofactor identities needed for fully expanded tetrahedral volume and angle calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.