det_regularUnitOffDiagMinorMatrix
plain-language theorem explainer
The 4×4 off-diagonal vertex minor of the regular unit Cayley–Menger matrix has determinant −1. Anyone computing regular-tetrahedron cofactors or dihedral cosines from the 5×5 CM determinant cites this evaluation. The proof expands the determinant along the first row and reduces the resulting 3×3 blocks by direct arithmetic.
Claim. Let $M$ be the $4\times 4$ real matrix whose first three diagonal entries are $0$, whose $(4,4)$ entry is $1$, and whose off-diagonal entries are all $1$. Then $\det M = -1$.
background
This module links the explicit tetrahedral Cayley–Menger polynomial cm3 to the genuine $5\times 5$ Cayley–Menger determinant, supplying the determinant and cofactor layer used by the dihedral-cosine formula. Rows and columns are indexed $0..4$, with the border of ones and the six squared edge lengths $a_0..a_5$ in the usual CM layout.
The object here is the off-diagonal vertex minor of the regular unit Cayley–Menger matrix: all six squared edges equal to $1$. Concretely it is the $4\times 4$ matrix with zeros on the first three diagonal positions, a one in the bottom-right corner, and ones everywhere off the diagonal. Its determinant is the raw minor that later becomes a signed cofactor.
proof idea
Unfold the matrix definition, then expand the determinant along row zero via Matrix.det_succ_row_zero. The resulting sum over the four cofactors is rewritten with Fin.sum_univ_succ and each $3\times 3$ block is evaluated by Matrix.det_fin_three (with Fin.succAbove handling the deleted-column indexing). A final norm_num closes the arithmetic to $-1$.
why it matters
Feeds directly into regularUnit_cofactor_34, which asserts that the $(3,4)$ cofactor of the regular-unit CM matrix equals $+1$. That cofactor is the first off-diagonal regular-unit cofactor needed when the dihedral-cosine formula is specialized to the regular tetrahedron. In the broader Recognition geometry stack this is pure linear-algebra scaffolding: once the regular-unit minors and cofactors are known numbers, the cosine of the regular dihedral angle drops out of the CM determinant without further casework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.