cmCofactor3
plain-language theorem explainer
Defines the $(r,c)$ cofactor of the $5\times5$ Cayley-Menger matrix of a tetrahedron as the signed minor of the squared-edge matrix. Anyone deriving dihedral cosines or volume formulas from edge data cites this. The body is the standard product of the parity sign $(-1)^{r+c}$ and the deleted-row/column determinant.
Claim. For squared edge lengths $a\in\mathbb{R}^6$ of a tetrahedron and indices $r,c\in\{0,1,2,3,4\}$, the Cayley-Menger cofactor is $C_{r,c}(a):=(-1)^{r+c}\,M_{r,c}(a)$, where $M_{r,c}(a)$ is the determinant of the $4\times4$ submatrix obtained by deleting row $r$ and column $c$ from the bordered Cayley-Menger matrix built from $a$.
background
The module links the explicit tetrahedral Cayley-Menger polynomial cm3 to the genuine $5\times5$ determinant. Rows and columns are ordered so that the border is the usual $0/1$ pattern and the interior $4\times4$ block holds the six squared edge lengths $(01),(02),(03),(12),(13),(23)$.
Squared edges are packaged as a map $a:\mathrm{Fin},6\to\mathbb{R}$. The minor deletes one row and one column via Fin.succAbove and takes the ordinary matrix determinant. The cofactor sign is the real number $+1$ or $-1$ according as $r+c$ is even or odd. Their product is the classical cofactor $C_{r,c}$ needed by Cramer's rule and by the dihedral-cosine identities.
proof idea
Pure definitional abbreviation: multiply the already-defined cofactor sign by the already-defined minor. No tactics, no lemmas beyond the two constituent definitions.
why it matters
Cofactors are the algebraic engine of the dihedral cosine formula that the module is built to support. Downstream, every regular-unit normalization theorem (cofactors $C_{12},C_{13},C_{14},C_{23},C_{24},C_{34}$ and the vertex-diagonal family) evaluates this definition on the unit regular tetrahedron and obtains the constant $1$. Smoothness of each cofactor is proved by a one-line product rule from smoothness of the minor. In the broader Recognition geometry layer these signed minors feed volume and angle extractions that sit under the $D=3$ forcing step (T8) once edge data are realized on the recognition lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.