regularUnit_cofactor_14
plain-language theorem explainer
For the unit regular tetrahedron (all squared edges equal to 1), the Cayley-Menger cofactor at matrix indices (1,4) equals 1. Anyone checking the regular-unit base case of the dihedral cosine formula via CM cofactors will cite this. The proof unfolds the cofactor definition, identifies the odd-parity sign, rewrites the minor as an explicit off-diagonal matrix, and multiplies the known determinant -1 by -1.
Claim. Let $C_{r,c}$ be the Cayley-Menger cofactor of the $5\times 5$ tetrahedral CM matrix built from squared edge lengths. For the unit regular tetrahedron (every squared edge length equal to $1$), one has $C_{1,4}=1$.
background
The module links the explicit tetrahedral Cayley-Menger polynomial cm3 to the genuine $5\times 5$ CM determinant and its cofactors, the layer required by the dihedral cosine formula. Rows and columns are indexed $0..4$, with the border of ones in row/column 0 and squared edge lengths $a_0..a_5$ filling the $4\times 4$ interior in the standard order $(01),(02),(03),(12),(13),(23)$.
A cofactor is $C_{r,c}=(-1)^{r+c}$ times the determinant of the matrix with row $r$ and column $c$ deleted. The unit regular tetrahedron is the edge assignment with every squared length equal to $1$. Upstream, the $(1,4)$-minor of that matrix is identified with an explicit off-diagonal $4\times 4$ matrix whose determinant equals $-1$.
proof idea
Unfold the cofactor into sign times minor. The index sum $1+4=5$ is odd, so the sign is $-1$ (discharged by a decide on parity). Rewrite the deleted-row/column submatrix via the equality that identifies it with the named regular-unit off-diagonal minor matrix, then substitute the already-proved fact that that matrix has determinant $-1$. A final norm_num multiplies $(-1)\cdot(-1)$ to obtain $1$.
why it matters
This is one of the six regular-unit cofactor evaluations that discharge regularUnitCofactorCheck in the dihedral CM module. That check was previously an assumption; the downstream theorem now proves it by case-splitting on opposite-edge pairs and invoking this identity (together with the sibling cofactor facts for indices $(1,2)$, $(1,3)$, $(2,3)$, $(2,4)$, $(3,4)$). The cofactor layer is exactly what feeds the dihedral cosine formula from CM data, so the regular tetrahedron becomes a fully proved calibration point rather than a hypothesis. In the broader Recognition geometry stack this anchors the unit regular base case before any deformation or continuum arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.