regularUnitDiagMinorMatrix
plain-language theorem explainer
The constant 4×4 matrix with zeros on the diagonal and ones off-diagonal is the diagonal-vertex principal minor of the Cayley–Menger matrix for the regular unit tetrahedron. Anyone computing CM determinants, cofactors, or dihedral cosines for that regular case cites it as the normal form of those minors. It is an explicit matrix literal, not a derived construction.
Claim. Let $M$ be the $4\times 4$ real matrix with $M_{ii}=0$ and $M_{ij}=1$ for $i\neq j$. This $M$ is the principal minor obtained by deleting one nonzero (vertex) index from the $5\times 5$ Cayley–Menger matrix of the regular tetrahedron with all squared edge lengths equal to $1$.
background
The module links the explicit tetrahedral Cayley–Menger polynomial cm3 to the genuine $5\times 5$ Cayley–Menger determinant and its cofactors, the layer needed for dihedral cosine formulas. Rows/columns are indexed $0..4$, with border row/column of ones (and a zero corner), and the $4\times 4$ block holding the six squared edge lengths $a_0..a_5$ for edges $(01),(02),(03),(12),(13),(23)$.
For the regular unit tetrahedron every squared edge length is $1$. Deleting the border index $0$ leaves a different minor; deleting any of the four vertex indices $1..4$ leaves a principal $4\times 4$ block. In the regular unit case that block is independent of which vertex is deleted: zeros on the diagonal (self-distances) and ones off-diagonal (unit squared edges). That constant matrix is what this definition names.
proof idea
Pure definition by matrix literal. The body is the $4\times 4$ array with $0$ on the diagonal and $1$ elsewhere, written with Mathlib’s !![·] notation. No lemmas or tactics are involved.
why it matters
Gives the normal form that later theorems identify and evaluate. Downstream, det_regularUnitDiagMinorMatrix proves its determinant equals $-3$ by unfolding the literal and expanding along the first row. regularUnit_diag_minor_eq_normalForm shows that every nonzero diagonal-vertex submatrix of cmMatrix3 regularUnitSqEdges equals this matrix (by fin_cases on the deleted index). Together they pin the regular-unit cofactor data used by the dihedral cosine layer of the tetrahedron CM calculus. In the broader Recognition geometry stack this is scaffolding for volume and angle identities on the regular cell, not a forcing-chain step (T0–T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.