det_regularUnitDiagMinorMatrix
plain-language theorem explainer
The 4×4 diagonal vertex minor of the regular unit tetrahedron Cayley-Menger matrix has determinant −3. Cofactor and dihedral-angle calculations for that tetrahedron cite this constant. The proof expands along the first row, reduces the 3×3 blocks with the finite determinant formula, and finishes by arithmetic.
Claim. Let $M$ be the $4\times 4$ real matrix with zeros on the diagonal and ones off the diagonal (the diagonal vertex minor of the regular unit Cayley-Menger matrix). Then $\det M = -3$.
background
The 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 a border of ones and squared edge lengths $a_0..a_5$ in the interior.
For the regular unit tetrahedron every squared edge length equals $1$. The diagonal vertex minor is the $4\times 4$ principal submatrix obtained by deleting the border row/column that corresponds to a spatial vertex; explicitly it is the matrix with $0$ on the diagonal and $1$ elsewhere. Upstream, that matrix is packaged as a named constant so that its determinant can be evaluated once and reused.
proof idea
Term-mode proof. Unfold the named $4\times 4$ matrix, expand the determinant along the first row via Matrix.det_succ_row_zero, then simplify with the finite-sum decomposition over Fin, the closed $3\times 3$ determinant formula, and the succAbove indexing of the complementary minors. The resulting rational expression is discharged by norm_num.
why it matters
Feeds the theorem that every diagonal vertex cofactor of the regular unit tetrahedron equals $-3$. That constant is the numerical input to the dihedral cosine formula in the regular case, and therefore sits on the path from the Cayley-Menger polynomial to concrete geometric angles. The surrounding module is the determinant/cofactor layer that makes the $5\times 5$ matrix usable; this evaluation closes the regular-unit special case of the vertex minors. In the broader Recognition geometry stack the result is pure Euclidean infrastructure in $D=3$ (the forced spatial dimension), not a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.