det_cmMinor44Matrix
plain-language theorem explainer
The determinant of the fixed 4×4 Cayley–Menger minor for cofactor (4,4) equals the explicit polynomial normal form of that cofactor in the six squared edge lengths. Anyone equating geometric CM cofactors to named polynomials cites this. The proof unfolds both sides, expands the determinant along the first row, and finishes by ring normalization.
Claim. Let $a:\{0,\ldots,5\}\to\mathbb{R}$ be squared edge lengths of a tetrahedron. Then $\det M_{44}(a)$ equals the explicit cofactor polynomial at indices $(4,4)$, where $M_{44}(a)=\begin{pmatrix}0&1&1&1\\1&0&a_0&a_1\\1&a_0&0&a_3\\1&a_1&a_3&0\end{pmatrix}$.
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 use named polynomial partials instead of opaque Fréchet derivatives.
Squared edge data are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The target polynomial family cmCofactor3Poly is a match on row/column indices giving a fixed multilinear expression in those six coordinates. The matrix cmMinor44Matrix is the concrete $4\times 4$ normal form of the diagonal minor that appears in cofactor $(4,4)$ of the bordered Cayley–Menger matrix: first row/column is the usual $(0,1,1,1)$ border, and the remaining $3\times 3$ block carries $a_0,a_1,a_3$ on the off-diagonals.
This lemma is the pure determinant identity linking that matrix to the polynomial entry at $(4,4)$.
proof idea
Term-mode proof by direct expansion. Unfold the matrix definition and the polynomial clause for indices $(4,4)$. Apply Matrix.det_succ_row_zero to expand along the leading border row, together with Fin.sum_univ_succ and Fin.succAbove to unwind the finite sum over the remaining three columns. The resulting cubic polynomial identity is discharged by ring_nf.
why it matters
Immediate parent is cmCofactor3_44_eq_poly, which rewrites the abstract cofactor cmCofactor3 a 4 4 as the polynomial by composing the submatrix identification, this determinant equality, and the even-sign factor for index pair $(4,4)$. That closes one cell of the cofactor-polynomial agreement table used throughout the geometry stack.
In the broader Recognition geometry layer, explicit CM cofactors feed dihedral-angle derivatives and volume/angle identities on the tetrahedron; having a ring-normalized polynomial (rather than an opaque minor) is what lets later calculus and forcing arguments treat edge-length dependence algebraically. No T0–T8 landmark is touched directly; this is infrastructure for the geometric side of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.