det_cmMinor12Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor for cofactor indices (1,2) equals the negative of the named cofactor polynomial in the six squared edge lengths. Anyone equating abstract CM cofactors to polynomial normal forms for tetrahedral 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_{12}(a) = -P_{1,2}(a)$, where $M_{12}(a)$ is the explicit $4\times 4$ minor matrix used by cofactor $(1,2)$ and $P_{1,2}(a)$ 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 lengths live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The cofactor polynomial cmCofactor3Poly r c is a match on row/column indices giving a concrete multilinear expression in those six coordinates. The companion matrix cmMinor12Matrix a is the fixed $4\times 4$ pattern
$$\begin{pmatrix}0&1&1&1\1&a_0&a_3&a_4\1&a_1&0&a_5\1&a_2&a_5&0\end{pmatrix}$$
used as the minor for cofactor $(1,2)$.
The abstract Cayley–Menger cofactor is defined via a signed determinant of a submatrix; this lemma identifies that determinant, for the $(1,2)$ slot, with the already-expanded polynomial (up to sign).
proof idea
Pure algebraic identification. Unfold the matrix constructor and the polynomial clause for indices $(1,2)$. Expand Matrix.det along the leading zero-row via Matrix.det_succ_row_zero, pushing the sum over Fin 4 with Fin.sum_univ_succ and Fin.succAbove. The resulting cubic expression in the six edge squares is identical (after a global minus) to the body of cmCofactor3Poly 1 2; ring_nf closes the equality.
why it matters
Immediate parent is cmCofactor3_12_eq_poly, which rewrites the abstract cofactor cmCofactor3 a 1 2 as the polynomial by composing the submatrix identity, this determinant identity, and the odd-parity cofactor sign. That equality is one tile in the module-wide program of replacing every tetrahedral CM cofactor by a named polynomial, the cofactor analogue of CayleyMengerDerivatives. Once all six (or fifteen) such identities are in place, dihedral-angle formulas become ordinary polynomial calculus on edge squares, with no residual matrix determinants in the derivative pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.