det_cmMinor02Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 (0,2)-minor matrix built from six squared tetrahedron edge lengths equals the named degree-4 cofactor polynomial at indices (0,2). Anyone equating abstract Cayley-Menger cofactors to polynomial normal forms cites this identity. The proof unfolds both sides, expands the determinant along the first row, and finishes by ring normalization.
Claim. For any assignment $a:\{0,\ldots,5\}\to\mathbb{R}$ of squared edge lengths of a tetrahedron, the determinant of the matrix $$\begin{pmatrix}1&0&a_1&a_2\\1&a_0&a_3&a_4\\1&a_1&0&a_5\\1&a_2&a_5&0\end{pmatrix}$$ equals the explicit cofactor polynomial at row $0$ and column $2$ in those six squared lengths.
background
The ambient 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 data are packaged as SqEdges, an abbreviation for maps $\mathrm{Fin},6\to\mathbb{R}$. The target polynomial is the $(0,2)$-clause of the match that defines the global cofactor normal form: a homogeneous degree-4 expression in $a_0,\ldots,a_5$. The left-hand side is the determinant of the concrete $4\times 4$ matrix obtained by deleting row $0$ and column $2$ from the bordered Cayley-Menger array and writing the surviving entries in terms of those same squared lengths.
This identity is the computational bridge between the matrix minor and that closed-form polynomial.
proof idea
Both sides are unfolded to their defining expressions. The $4\times 4$ determinant is expanded along the first row via Matrix.det_succ_row_zero, with the resulting finite sums rewritten by Fin.sum_univ_succ and Fin.succAbove. The resulting multivariate polynomial identity is discharged by ring_nf. No external geometric lemmas are required; the argument is pure matrix algebra plus ring arithmetic.
why it matters
The immediate consumer is cmCofactor3_02_eq_poly, which rewrites the geometric Cayley-Menger cofactor at indices $(0,2)$ as this polynomial by composing the submatrix identification with the present determinant identity and a parity check on the cofactor sign. That equality is one cell in the full table of cofactor-polynomial agreements that the module supplies as the cofactor analogue of the Cayley-Menger derivative package. Explicit polynomial forms let later dihedral-angle and volume calculus differentiate under a named algebraic expression rather than an opaque matrix determinant, keeping the Recognition geometry stack fully computational.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.