det_cmMinor00Matrix
plain-language theorem explainer
The determinant of the principal 4×4 minor obtained by deleting the first row and column of the tetrahedral Cayley–Menger matrix equals a fixed quadratic polynomial in the six squared edge lengths. Anyone reducing dihedral-angle or volume formulae to edge data via cofactors would cite this identity. The proof unfolds both sides, expands the 4×4 determinant along the first row, and finishes by ring normalization.
Claim. For any assignment $a:\{0,\ldots,5\}\to\mathbb{R}$ of squared edge lengths of a tetrahedron, the determinant of the $4\times 4$ matrix $\begin{pmatrix}0&a_0&a_1&a_2\\a_0&0&a_3&a_4\\a_1&a_3&0&a_5\\a_2&a_4&a_5&0\end{pmatrix}$ equals the explicit polynomial $(a_2)^2(a_3)^2-2a_1 a_2 a_3 a_4+(a_1)^2(a_4)^2-2a_0 a_2 a_3 a_5-2a_0 a_1 a_4 a_5+(a_0)^2(a_5)^2$.
background
The ambient module expands every cofactor of the $5\times 5$ Cayley–Menger matrix of a tetrahedron into an explicit polynomial in the six squared edge lengths. Downstream dihedral-angle calculus can then differentiate named polynomials rather than opaque Fréchet derivatives.
Squared edge data are packaged as a map $a:\mathrm{Fin},6\to\mathbb{R}$. The matrix whose determinant is taken here is the principal minor obtained by deleting row 0 and column 0 of the bordered Cayley–Menger matrix; its entries are $0$ on the diagonal and the six squared lengths off-diagonal in the standard edge ordering. The target polynomial is the $(0,0)$ clause of the global cofactor normal form: a homogeneous degree-4 expression built only from those six coordinates.
The identity is the computational bridge between the abstract minor (defined by submatrix extraction) and that closed-form polynomial.
proof idea
Both sides are unfolded to their concrete definitions. The left-hand side is a $4\times 4$ determinant; Matrix.det_succ_row_zero expands it along the first row, while Fin.sum_univ_succ and Fin.succAbove unwind the finite sums and index shifts that appear in the Laplace expansion. After the expansion the two sides are identical as polynomials in the six edge variables, which ring_nf confirms.
why it matters
The immediate consumer is the equality that identifies the geometric $(0,0)$ Cayley–Menger cofactor with this polynomial: that theorem rewrites the abstract cofactor through the submatrix relation and then applies the present determinant identity, adjusting only by the cofactor sign (even, hence $+1$).
Together with the sibling identities for the other index pairs, this supplies the full table of explicit cofactor polynomials. That table is the cofactor analogue of the Cayley–Menger derivative module: once every cofactor is a named polynomial, partial derivatives needed for dihedral-angle gradients become ordinary polynomial calculus rather than symbolic fderiv terms. In the broader Recognition geometry stack these polynomials feed volume and angle formulae that ultimately constrain discrete curvature and edge-length dynamics on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.