det_cmMinor11Matrix
plain-language theorem explainer
The determinant of the normal-form 4×4 Cayley-Menger minor for cofactor (1,1) equals the explicit polynomial in the six squared tetrahedron edges. Cited by anyone equating abstract CM cofactors to named polynomials for dihedral-angle calculus. Proof unfolds both sides, expands the det along the leading zero row, and finishes by ring normalization.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, $\det M_{11}(a)$ equals the explicit polynomial normal form of the Cayley-Menger cofactor at index pair $(1,1)$ evaluated on $a$, where $M_{11}(a)$ is the $4\times 4$ matrix with first row/column $(0,1,1,1)$ and edge block filled by $a_3,a_4,a_5$.
background
The Cayley-Menger determinant recovers the squared volume of a simplex from squared edge lengths. For a tetrahedron the ambient matrix is $5\times 5$; its cofactors appear in classical formulas for dihedral cosines and related angle derivatives.
This module expands every tetrahedral CM cofactor as an explicit polynomial in the six squared edges $a:\mathrm{Fin},6\to\mathbb{R}$. The minor used by cofactor $(1,1)$ is the concrete $4\times 4$ matrix $$\begin{pmatrix}0&1&1&1\1&0&a_3&a_4\1&a_3&0&a_5\1&a_4&a_5&0\end{pmatrix}.$$ The right-hand side is the matching case of the global cofactor normal-form family, which lists a multivariate polynomial for each index pair $(r,c)\in\mathrm{Fin},5\times\mathrm{Fin},5$.
Local setting (module doc): cofactor analogue of the Cayley-Menger derivative expansions, so downstream dihedral calculus can name polynomial partials instead of opaque fderiv terms.
proof idea
Short term-mode proof. Unfold the minor-matrix definition and the $(1,1)$ case of the cofactor polynomial. Simplify with Laplace expansion along the leading row that begins with zero (Matrix.det_succ_row_zero), together with the standard Fin sum/succAbove bookkeeping that turns the $4\times 4$ det into an explicit multilinear combination of the edge entries. The resulting polynomial identity is discharged by ring_nf.
why it matters
Immediate parent is the agreement theorem equating the abstract CM cofactor at $(1,1)$ to this polynomial: that proof rewrites through the submatrix identification, applies this determinant identity, and clears the even cofactor sign. Together those lemmas discharge one diagonal entry of the cofactor-polynomial agreement family.
That family is the cofactor twin of the Cayley-Menger derivative module: once every cofactor is a named polynomial in the six squared edges, partial derivatives needed for dihedral-angle variation become ordinary polynomial calculus rather than abstract Fréchet derivatives. Pure classical 3-simplex algebra; it supplies the rigid geometric substrate used elsewhere in the Recognition stack whenever tetrahedral edge data must be differentiated or constrained, without itself invoking the forcing chain or RS unit conventions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.