det_cmMinor24Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor for index pair (2,4) equals the named cofactor polynomial in the six squared edge lengths. Anyone computing tetrahedral cofactors or dihedral-angle partials in closed form will cite this identity. The proof unfolds both sides and reduces the 4×4 determinant by row expansion and ring normalization.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the determinant of the explicit $4\times 4$ minor matrix associated to cofactor indices $(2,4)$ equals the value of the explicit Cayley–Menger cofactor polynomial at those same indices and edge data.
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 target polynomial cmCofactor3Poly is a match on row/column indices giving a fixed multilinear expression in those six coordinates; the $(2,4)$ branch is one of those normal forms. The matrix cmMinor24Matrix a is the concrete $4\times 4$ real matrix
$$\begin{pmatrix}0&1&1&1\1&0&a_0&a_1\1&a_1&a_3&0\1&a_2&a_4&a_5\end{pmatrix}$$
used as the minor for cofactor $(2,4)$.
This lemma equates the ordinary matrix determinant of that minor with the polynomial normal form, closing the gap between the combinatorial minor and the expanded expression.
proof idea
Term-style tactic proof. Unfold the minor matrix and the cofactor polynomial definitions so both sides are concrete expressions in the six edge coordinates. Expand the $4\times 4$ determinant along the first row via Matrix.det_succ_row_zero, together with the finite-sum and succAbove simplifiers that discharge the Fin 4 indexing. The resulting multilinear polynomial identity is finished by ring_nf.
why it matters
Feeds directly into cmCofactor3_24_eq_poly, which proves that the abstract Cayley–Menger cofactor at indices $(2,4)$ equals the explicit polynomial: that parent rewrites the cofactor through the minor-submatrix equality, applies this determinant identity, and adjusts the cofactor sign (even parity of $6$).
In the broader geometry stack this is one tile of the cofactor-polynomial catalogue that lets dihedral-angle derivatives be written as ordinary partials of named polynomials rather than symbolic fderiv terms. It is pure classical multilinear algebra supporting the Recognition geometry layer; it does not itself invoke the forcing chain (T0–T8), RCL, or $\varphi$-ladder constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.