regularUnit_diag_minor_eq_normalForm
plain-language theorem explainer
For the unit regular tetrahedron, every principal 4×4 minor of the 5×5 Cayley-Menger matrix obtained by deleting a vertex row and column (any index other than the border) equals one fixed normal-form matrix: zeros on the diagonal and ones off it in the standard border pattern. Cofactor and dihedral-cosine calculations for that tetrahedron cite this reduction. The proof is exhaustive case analysis on the deleted index, then entrywise simplification.
Claim. Let $C$ be the $5\times 5$ Cayley-Menger matrix of the unit regular tetrahedron (all six squared edge lengths equal to $1$). For every index $p\in\{1,2,3,4\}$, the principal submatrix of $C$ obtained by deleting row $p$ and column $p$ equals the fixed $4\times 4$ matrix $\begin{pmatrix}0&1&1&1\\1&0&1&1\\1&1&0&1\\1&1&1&0\end{pmatrix}$.
background
This module links the explicit tetrahedral Cayley-Menger polynomial to the concrete $5\times 5$ determinant and its cofactors, the layer needed by the dihedral cosine formula. Rows and columns are indexed $0..4$, with border row/column $0$ holding the classical $0$ and $1$ pattern, and the remaining $4\times 4$ block carrying the six squared edge lengths $(01),(02),(03),(12),(13),(23)$.
The unit regular tetrahedron is the edge assignment in which every squared length equals $1$. Its Cayley-Menger matrix is therefore completely numerical. The target normal form is the fixed $4\times 4$ matrix with $0$ on the diagonal and $1$ off-diagonal in the same border convention; it is exactly what one expects after deleting any single vertex row/column from that numerical matrix.
Upstream, the matrix constructor fills entries from the six squared lengths, and the unit-regular edge data is the constant-$1$ assignment. The claim is only about principal minors that delete a nonzero index (a geometric vertex), not the border.
proof idea
Term-mode proof by exhaustive case split on the deleted index $p\in\mathrm{Fin},5$. The $p=0$ branch is immediate contradiction with the hypothesis $p\neq 0$. For each of the four surviving indices, both sides are $4\times 4$ matrices, so equality is reduced to entrywise identity via ext. Nested case splits on the two remaining $\mathrm{Fin},4$ indices, followed by simp against the definitions of the normal-form matrix, the Cayley-Menger matrix constructor, the constant-$1$ edge data, and the succAbove reindexing, discharge every entry.
why it matters
The immediate consumer is the diagonal vertex-cofactor theorem for the same unit regular tetrahedron, which unfolds the cofactor as a signed minor and obtains the constant value $-3$. That constant is the numerical input needed when the dihedral cosine formula is specialized to the regular unit case.
In the broader Recognition geometry stack this sits in the determinant/cofactor layer that turns the Cayley-Menger polynomial into concrete $5\times 5$ linear algebra. Regular-unit specializations are the baseline against which deformed edge data (and later continuum or Regge-type limits) are compared; having every vertex minor collapse to one normal form removes casework from those downstream cofactor identities.
No forcing-chain landmark (T5–T8) is touched directly; the result is pure classical tetrahedral linear algebra inside the geometry module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.