det_cmMinor31Matrix
plain-language theorem explainer
The determinant of the explicit 4x4 (3,1)-minor of the bordered Cayley-Menger matrix equals the hand-expanded cofactor polynomial at indices (3,1), for any six squared tetrahedron edge lengths. Cite when converting abstract CM cofactors into ordinary polynomials for dihedral or volume calculus. 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_{3,1}(a)$ equals the explicit polynomial normal form of the Cayley-Menger cofactor at row 3 and column 1, where $M_{3,1}(a)$ is the $4\times 4$ matrix $\begin{pmatrix}0&1&1&1\\1&a(0)&a(1)&a(2)\\1&0&a(3)&a(4)\\1&a(4)&a(5)&0\end{pmatrix}$.
background
This 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 Fréchet derivatives.
Squared edge lengths are maps $a:{0,\ldots,5}\to\mathbb{R}$. The bordered Cayley-Menger matrix encodes Euclidean embeddability of a 3-simplex from those lengths; its $4\times 4$ minors (after deleting one border row and one border column) are the classical cofactors that enter volume and dihedral formulae. The matrix appearing here is exactly that minor for deletion indices $(3,1)$. The right-hand side is the matching clause of the global cofactor polynomial table, which lists a cubic form in the six edge squares for every index pair.
proof idea
Unfold the concrete minor matrix and the target polynomial clause. Expand the $4\times 4$ determinant along its first row (the border row of zeros and ones) via the successor-row determinant formula, summing the three nonzero contributions with the signs induced by column deletion. The resulting expression in the six edge squares is identical, after commutative ring normalization, to the precomputed polynomial at indices $(3,1)$.
why it matters
The immediate consumer is the identification theorem that equates the abstract Cayley-Menger cofactor (determinant of the submatrix cut from the full CM matrix, including the conventional sign) with this explicit polynomial. Once that bridge is in place, every subsequent partial derivative needed for dihedral-angle gradients becomes ordinary polynomial calculus rather than symbolic differentiation of an opaque matrix determinant.
The lemma sits in the cofactor analogue of the Cayley-Menger derivative expansions. Within the broader Recognition geometry stack it supplies the algebraic substrate for volume and angle identities on edge lengths drawn from the phi-ladder, though the statement itself is pure classical simplex algebra and does not invoke RS constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.