cmMinor3
plain-language theorem explainer
The (r,c)-minor of the 5×5 Cayley-Menger matrix of a tetrahedron: delete row r and column c, then take the determinant of the remaining 4×4 block in the six squared edge lengths. Anyone expanding cofactors or deriving dihedral cosines from edge data cites this. The body is a one-line composition of Mathlib submatrix (via succAbove) and det on the explicit CM matrix.
Claim. For squared edge lengths $a$ of a tetrahedron and indices $r,c\in\{0,1,2,3,4\}$, let $M_{r,c}(a)$ be the determinant of the $4\times 4$ submatrix of the Cayley-Menger matrix of $a$ obtained by deleting row $r$ and column $c$.
background
This module sits between the explicit tetrahedral Cayley-Menger polynomial and the determinant/cofactor layer used by the dihedral cosine formula. Squared edge lengths are a map $a:\mathrm{Fin},6\to\mathbb{R}$ packing the six edges $(01),(02),(03),(12),(13),(23)$. The Cayley-Menger matrix is the standard $5\times 5$ array with a zero corner, a bordering row/column of ones, zeros on the spatial diagonal, and the squared lengths off-diagonal in the usual order.
A minor is the determinant after deleting one row and one column. Index deletion uses $\mathrm{succAbove}$, so the remaining indices stay ordered. Upstream, the matrix itself is defined entrywise by case on the pair of $\mathrm{Fin},5$ indices; the determinant is Mathlib's real matrix determinant.
proof idea
Pure definition, not a proved statement. It applies Mathlib Matrix.det to the submatrix of cmMatrix3 a whose row and column maps are Fin.succAbove r and Fin.succAbove c. No algebraic reduction or case split lives here; smoothness and numerical evaluations are proved downstream by unfolding this def.
why it matters
Cofactors are defined as signed minors, so every cofactor identity and every regular-unit cofactor evaluation (values 1 on the off-diagonal spatial pairs) unfolds through this minor. Smoothness of each minor in the six squared lengths is proved by unfolding and fun_prop, which feeds contDiff of the full determinant and of the dihedral cosine expressions.
In the Recognition geometry stack this is the determinant layer that turns the CM polynomial into a matrix calculus usable for volume, orientation, and angle formulas on tetrahedra. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is classical Euclidean scaffolding those continuum bridges sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.