det_cmMinor23Matrix
plain-language theorem explainer
The determinant of the 4×4 Cayley–Menger minor for index pair (2,3) equals the negative of the explicit cofactor polynomial at those indices. Anyone matching geometric cofactors to named polynomials in the six squared edge lengths would cite this identity. 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_{2,3}(a) = -P_{2,3}(a)$, where $M_{2,3}(a)$ is the normal-form $4\times 4$ minor matrix for cofactor indices $(2,3)$ and $P_{r,c}$ is the explicit Cayley–Menger cofactor polynomial in those squared lengths.
background
This 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 live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The bordered Cayley–Menger matrix of a tetrahedron is $5\times 5$; its $(r,c)$-cofactor is $(\pm)$ the determinant of the complementary $4\times 4$ minor. Here the minor for indices $(2,3)$ is fixed in normal form
$$M_{2,3}(a)=\begin{pmatrix}0&1&1&1\1&0&a_0&a_2\1&a_1&a_3&a_5\1&a_2&a_4&0\end{pmatrix}.$$
The matching explicit polynomial $P_{2,3}$ is one branch of the case-split normal form for every cofactor; this theorem is the pure determinant identity linking that matrix to that polynomial.
proof idea
Term-mode proof by direct expansion. Unfold the minor matrix and the cofactor polynomial definitions. Simplify with the first-row Laplace expansion (Matrix.det_succ_row_zero) together with the standard Fin sum and succAbove identities that enumerate the $4\times 4$ cofactors. The resulting multivariate polynomial identity is discharged by ring_nf. No external geometric lemmas are required; the equality is purely algebraic.
why it matters
Immediate parent is cmCofactor3_23_eq_poly, which rewrites the abstract Cayley–Menger cofactor at $(2,3)$ as the named polynomial by composing the submatrix identification, this determinant identity, and the cofactor sign. That agreement is the cofactor analogue of the derivative expansions elsewhere in the geometry stack: once every cofactor is a concrete polynomial in the six squared edges, partial derivatives and dihedral-angle formulae become ordinary polynomial calculus rather than opaque fderiv terms. The result is local linear algebra inside the tetrahedral Cayley–Menger apparatus; it does not itself invoke the Recognition forcing chain (T0–T8), but it supplies the algebraic substrate those geometric identities need when angles and volumes are expressed on the edge ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.