det_cmMinor42Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 Cayley–Menger minor for cofactor indices (4,2) equals the named degree-4 polynomial in the six squared edge lengths. Cite this when equating geometric CM cofactors to closed-form polynomials for tetrahedral dihedral calculus. Proof: unfold both sides, expand the det along the first row, then ring-normalize.
Claim. Let $a:\{0,\ldots,5\}\to\mathbb{R}$ be squared edge lengths of a tetrahedron. The determinant of the $4\times 4$ minor matrix $$\begin{pmatrix}0&1&1&1\\1&0&a_1&a_2\\1&a_0&a_3&a_4\\1&a_1&0&a_5\end{pmatrix}$$ equals the explicit cofactor polynomial at row–column indices $(4,2)$ in those six coordinates.
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 differentiate named polynomials rather than opaque Fréchet derivatives.
SqEdges is simply $\mathrm{Fin},6\to\mathbb{R}$: the six squared edge lengths of a tetrahedron. The target polynomial cmCofactor3Poly r c is the normal-form expression for the $(r,c)$ cofactor of the bordered Cayley–Menger matrix, given by a large case split on the five-by-five index pair. The left-hand matrix cmMinor42Matrix a is the concrete $4\times 4$ submatrix obtained by deleting the appropriate row and column for the $(4,2)$ cofactor slot; its entries are $0$, $1$, or selected $a_i$.
This lemma is the pure linear-algebra identity that the determinant of that written matrix equals the corresponding polynomial case.
proof idea
Term/tactic hybrid, four lines. Unfold the matrix constructor and the polynomial definition so both sides are concrete expressions in the $a_i$. Expand Matrix.det along the zero-th row via Matrix.det_succ_row_zero, pushing the sum through Fin.sum_univ_succ and the succAbove reindexing of the complementary columns. The resulting multilinear expression is then identical to the polynomial after ring_nf. No external geometric lemmas are required; it is pure $4\times 4$ determinant algebra.
why it matters
Immediate parent is cmCofactor3_42_eq_poly, which rewrites the geometric cofactor cmCofactor3 a 4 2 (built from the abstract minor and a sign) into the explicit polynomial by composing the submatrix identification, this determinant identity, and the even-parity sign for index sum $6$. That equality is one cell of the full cofactor-polynomial table the module generates.
In the broader Recognition geometry stack these named polynomials feed dihedral-angle derivatives and volume/cofactor calculus on the tetrahedron, the discrete geometric substrate underlying eight-tick and $D=3$ forcing. Without the det-equals-poly bridge, later partials would remain stuck on opaque matrix minors rather than ring expressions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.