det_cmMinor41Matrix
plain-language theorem explainer
The determinant of the Cayley–Menger (4,1)-minor matrix equals the negative of the explicit cofactor polynomial at row 4, column 1, on six squared edge lengths. Anyone wiring geometric cofactors to named polynomials for dihedral-angle calculus cites this identity. The proof unfolds both sides, expands the 4×4 determinant along the leading zero row, and finishes by ring normalization.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, $\det M_{4,1}(a) = -P_{4,1}(a)$, where $M_{4,1}(a)$ is the $4\times 4$ Cayley–Menger minor matrix obtained by deleting row index 4 and column index 1, and $P_{4,1}$ is the explicit polynomial normal form of that cofactor.
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.
Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The bordered Cayley–Menger matrix of a tetrahedron is $5\times 5$; deleting one row and one column yields a $4\times 4$ minor whose determinant (with the usual cofactor sign) is the geometric cofactor. Here the concrete minor matrix for indices $(4,1)$ is
$$\begin{pmatrix}0&1&1&1\1&a_0&a_1&a_2\1&0&a_3&a_4\1&a_3&0&a_5\end{pmatrix}.$$
The target polynomial $P_{r,c}$ is the match-defined normal form cmCofactor3Poly, which lists a cubic expression in the six edge squares for every pair $(r,c)\in\mathrm{Fin},5\times\mathrm{Fin},5$. This lemma equates the raw matrix determinant of the $(4,1)$ minor to $-P_{4,1}$.
proof idea
Term-mode proof by direct expansion. Unfold the minor-matrix constructor and the match clause of the cofactor polynomial. Simplify with the Laplace expansion of a $4\times 4$ determinant along the first (zero-border) row (Matrix.det_succ_row_zero), together with the standard Fin sum and succAbove reindexing lemmas that turn the cofactor sum into four explicit $3\times 3$ terms. The resulting multivariate polynomial identity is discharged by ring_nf.
why it matters
This is one tile in the cofactor-polynomial agreement layer: the immediate parent cmCofactor3_41_eq_poly rewrites the geometric cofactor (submatrix determinant times cofactor sign) into the named polynomial $P_{4,1}$ by composing the submatrix-equality lemma with this determinant identity and a parity check on the sign. Parallel siblings do the same for the other index pairs ($(3,4)$, $(2,4)$, …).
Once every cofactor is a named polynomial, partial derivatives needed for dihedral-angle gradients become ordinary polynomial calculus rather than abstract fderiv terms. That is exactly the module’s stated purpose: the cofactor analogue of the Cayley–Menger derivative expansions. No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here; the result is pure classical geometry scaffolding inside the RS geometry stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.