det_cmMinor03Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 (0,3)-minor of the tetrahedral Cayley–Menger matrix equals the negative of the named cubic cofactor polynomial in the six squared edge lengths. Anyone matching symbolic CM cofactors to closed-form polynomials for dihedral calculus would cite it. The proof unfolds both sides, expands the determinant along the first row, and finishes by ring normalization.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, $\det M_{0,3}(a) = -P_{0,3}(a)$, where $M_{0,3}(a)$ is the explicit $4\times 4$ minor matrix with entries built from $a$, and $P_{0,3}$ is the cubic polynomial normal form of the Cayley–Menger cofactor at indices $(0,3)$.
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 refer to named polynomial partials instead of opaque derivative terms.
Squared edge lengths live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The target cofactor polynomial $P_{0,3}$ is the $(0,3)$ branch of the match that defines the full family of CM cofactor normal forms; it is a homogeneous cubic in the six edge squares. The companion matrix $M_{0,3}(a)$ is the concrete $4\times 4$ array
$$\begin{pmatrix}1&0&a_0&a_2\1&a_0&0&a_4\1&a_1&a_3&a_5\1&a_2&a_4&0\end{pmatrix},$$
obtained by deleting the indicated row and column from the bordered Cayley–Menger matrix and writing the remaining entries in edge-square coordinates.
proof idea
Pure algebraic identity, no geometry. Unfold the matrix definition and the $(0,3)$ branch of the cofactor polynomial. Expand the $4\times 4$ determinant along the first row via Matrix.det_succ_row_zero, unwind the finite sums with Fin.sum_univ_succ and Fin.succAbove, then close by ring_nf. Both sides become the same cubic polynomial in the six edge squares.
why it matters
This is one tile in the explicit cofactor-polynomial table that makes tetrahedral CM calculus fully symbolic. Its sole downstream consumer is cmCofactor3_03_eq_poly, which rewrites the abstract cofactor cmCofactor3 a 0 3 as $P_{0,3}(a)$ by identifying the minor submatrix, applying this determinant identity, and inserting the cofactor sign (odd, hence a minus). That equality lets later dihedral-angle and volume derivatives work with named polynomials rather than fderiv black boxes, the cofactor analogue of the Cayley–Menger derivative module. No Recognition forcing-chain landmark is touched directly; the result is pure Euclidean geometry scaffolding for later RS geometric claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.