det_cmMinor34Matrix
plain-language theorem explainer
The determinant of the explicit 4×4 minor for Cayley-Menger cofactor indices (3,4) equals the negative of the named cofactor polynomial in the six squared edge lengths. Anyone matching abstract CM cofactors to closed-form edge polynomials 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$ of six squared edge lengths of a tetrahedron, $\det M_{3,4}(a) = -P_{3,4}(a)$, where $M_{3,4}(a)$ is the explicit $4\times 4$ minor normal form for cofactor indices $(3,4)$ and $P_{3,4}$ is the corresponding explicit cofactor polynomial.
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 enter dihedral-angle formulas and edge derivatives.
This module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edges $a:\mathrm{Fin},6\to\mathbb{R}$. The minor for cofactor $(3,4)$ is the concrete matrix $$\begin{pmatrix}0&1&1&1\1&0&a_0&a_1\1&a_0&0&a_3\1&a_2&a_4&a_5\end{pmatrix}.$$ The matching polynomial entry is the closed-form expansion of that cofactor (up to the conventional sign factor handled downstream).
proof idea
Unfold the minor-matrix definition and the cofactor-polynomial definition. Expand the $4\times 4$ determinant by the first-row Laplace formula (Matrix.det_succ_row_zero), reducing the sum with Fin.sum_univ_succ and Fin.succAbove. The resulting multivariate polynomial identity is discharged by ring_nf. No external geometric lemmas are required; the equality is pure matrix algebra against the hard-coded normal form.
why it matters
The immediate consumer is the cofactor-polynomial agreement theorem for indices $(3,4)$, which rewrites the abstract Cayley-Menger cofactor as this polynomial: it identifies the submatrix with the normal form, applies this determinant identity, and inserts the cofactor sign. That agreement is the module's purpose: downstream dihedral-angle calculus can differentiate named polynomials in the six squared edges instead of opaque Fréchet derivatives (the cofactor analogue of the Cayley-Menger derivative development). In the Recognition geometry stack these polynomials feed hinge-aware Regge analysis on the tetrahedral lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.